chore: testing leanprover/lean4#4085 against nightly-testing

[kim-em]

This is the lean-pr-testing-4085 branch, turned into a PR so we can run !bench.

[kim-em]

!bench

[leanprover-bot]

Here are the benchmark results for commit 7293754.
The entire run failed.
Found no significant differences.

[kim-em]

!bench

[leanprover-bot]

Here are the benchmark results for commit e7526e3.
There were significant changes against commit d297310:

  Benchmark                                                   Metric         Change
  =================================================================================
+ build                                                       elaboration     -6.5%
+ ~Mathlib.Algebra.Category.AlgebraCat.Monoidal               instructions   -11.1%
- ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings           instructions     3.2%
- ~Mathlib.Algebra.Category.ModuleCat.Presheaf                instructions    13.4%
+ ~Mathlib.Algebra.DirectLimit                                instructions   -15.8%
+ ~Mathlib.Algebra.Lie.Quotient                               instructions   -72.3%
- ~Mathlib.Algebra.Module.PID                                 instructions     7.5%
+ ~Mathlib.Algebra.Module.Submodule.Localization              instructions   -52.0%
- ~Mathlib.AlgebraicGeometry.AffineScheme                     instructions     5.5%
- ~Mathlib.AlgebraicGeometry.GammaSpecAdjunction              instructions     4.8%
- ~Mathlib.AlgebraicGeometry.OpenImmersion                    instructions    41.2%
- ~Mathlib.AlgebraicGeometry.Restrict                         instructions   294.2%
- ~Mathlib.AlgebraicGeometry.Scheme                           instructions   169.2%
+ ~Mathlib.Analysis.Normed.Group.Quotient                     instructions   -75.0%
+ ~Mathlib.CategoryTheory.Generator                           instructions   -48.0%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure           instructions   -44.0%
- ~Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions        instructions    52.3%
- ~Mathlib.Geometry.RingedSpace.LocallyRingedSpace            instructions   134.2%
- ~Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing        instructions     4.7%
+ ~Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits   instructions   -10.7%
+ ~Mathlib.GroupTheory.Coset                                  instructions   -79.2%
+ ~Mathlib.GroupTheory.GroupAction.Quotient                   instructions   -76.8%
+ ~Mathlib.GroupTheory.QuotientGroup                          instructions   -34.4%
+ ~Mathlib.LinearAlgebra.Isomorphisms                         instructions   -55.7%
+ ~Mathlib.LinearAlgebra.Quotient                             instructions   -28.5%
+ ~Mathlib.LinearAlgebra.QuotientPi                           instructions   -68.1%
+ ~Mathlib.LinearAlgebra.SModEq                               instructions   -89.4%
+ ~Mathlib.MeasureTheory.Measure.Haar.Quotient                instructions   -55.0%
- ~Mathlib.RepresentationTheory.GroupCohomology.Resolution    instructions     3.6%
- ~Mathlib.RepresentationTheory.Rep                           instructions    20.3%
- ~Mathlib.RingTheory.SimpleModule                            instructions    21.1%
+ ~Mathlib.RingTheory.Smooth.Basic                            instructions   -42.0%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring              instructions   -22.8%
+ ~Mathlib.Topology.Algebra.InfiniteSum.Module                instructions   -60.3%
+ ~Mathlib.Topology.Instances.AddCircle                       instructions   -59.4%