base of #12810

[FR-vdash-bot]

---

[FR-vdash-bot]

!bench

[mergify]

⚠️ The sha of the head commit of this PR conflicts with #12782. Mergify cannot evaluate rules on this PR. ⚠️

[leanprover-bot]

Here are the benchmark results for commit c8ba1f8.
There were significant changes against commit 51625e9:

  Benchmark                                                   Metric         Change
  =================================================================================
+ build                                                       elaboration     -8.9%
+ ~Batteries.Data.Array.Lemmas                                instructions   -87.8%
+ ~Batteries.Data.List.Lemmas                                 instructions   -39.6%
+ ~Mathlib.Algebra.DirectLimit                                instructions   -15.7%
+ ~Mathlib.Algebra.Lie.Quotient                               instructions   -72.4%
- ~Mathlib.Algebra.Module.PID                                 instructions     7.3%
+ ~Mathlib.Algebra.Module.Submodule.Localization              instructions   -51.7%
+ ~Mathlib.Analysis.Normed.Group.Quotient                     instructions   -75.2%
+ ~Mathlib.CategoryTheory.Generator                           instructions   -42.2%
+ ~Mathlib.Combinatorics.Additive.PluenneckeRuzsa             instructions   -69.1%
+ ~Mathlib.FieldTheory.AbelRuffini                            instructions   -35.2%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure           instructions   -43.9%
+ ~Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits   instructions    -6.8%
+ ~Mathlib.GroupTheory.Coset                                  instructions   -78.8%
+ ~Mathlib.GroupTheory.GroupAction.Quotient                   instructions   -76.8%
+ ~Mathlib.GroupTheory.QuotientGroup                          instructions   -34.3%
+ ~Mathlib.LinearAlgebra.Isomorphisms                         instructions   -58.1%
+ ~Mathlib.LinearAlgebra.Quotient                             instructions   -28.7%
+ ~Mathlib.LinearAlgebra.QuotientPi                           instructions   -68.3%
+ ~Mathlib.LinearAlgebra.SModEq                               instructions   -89.4%
+ ~Mathlib.MeasureTheory.Measure.Haar.Quotient                instructions   -54.5%
+ ~Mathlib.RingTheory.Smooth.Basic                            instructions   -42.6%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring              instructions   -22.4%
+ ~Mathlib.Topology.Algebra.InfiniteSum.Module                instructions   -60.3%
+ ~Mathlib.Topology.Instances.AddCircle                       instructions   -58.4%