changes

[mattrobball]

---

[mattrobball]

!bench

[leanprover-bot]

Here are the benchmark results for commit 2aab5f5.
There were significant changes against commit 21b3a48:

  Benchmark                                                   Metric         Change
  =================================================================================
+ build                                                       elaboration     -8.9%
+ ~Mathlib.Algebra.Category.AlgebraCat.Monoidal               instructions   -11.0%
- ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings           instructions     3.0%
- ~Mathlib.Algebra.Category.ModuleCat.Presheaf                instructions    12.4%
+ ~Mathlib.Algebra.DirectLimit                                instructions   -15.4%
+ ~Mathlib.Algebra.Lie.Quotient                               instructions   -72.4%
+ ~Mathlib.Algebra.Module.Submodule.Localization              instructions   -52.1%
- ~Mathlib.AlgebraicGeometry.AffineScheme                     instructions     9.1%
- ~Mathlib.AlgebraicGeometry.GammaSpecAdjunction              instructions    10.0%
- ~Mathlib.AlgebraicGeometry.OpenImmersion                    instructions    40.6%
- ~Mathlib.AlgebraicGeometry.Restrict                         instructions   290.0%
- ~Mathlib.AlgebraicGeometry.Scheme                           instructions   210.7%
+ ~Mathlib.Analysis.Normed.Group.Quotient                     instructions   -75.2%
+ ~Mathlib.CategoryTheory.Generator                           instructions   -48.0%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure           instructions   -43.9%
- ~Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions        instructions    52.2%
- ~Mathlib.Geometry.RingedSpace.LocallyRingedSpace            instructions   134.0%
- ~Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing        instructions     6.0%
+ ~Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits   instructions   -10.6%
+ ~Mathlib.GroupTheory.Coset                                  instructions   -79.1%
+ ~Mathlib.GroupTheory.GroupAction.Quotient                   instructions   -76.8%
+ ~Mathlib.GroupTheory.QuotientGroup                          instructions   -34.4%
+ ~Mathlib.LinearAlgebra.Isomorphisms                         instructions   -58.1%
+ ~Mathlib.LinearAlgebra.Quotient                             instructions   -28.5%
+ ~Mathlib.LinearAlgebra.QuotientPi                           instructions   -68.3%
+ ~Mathlib.LinearAlgebra.SModEq                               instructions   -89.4%
+ ~Mathlib.MeasureTheory.Measure.Haar.Quotient                instructions   -54.9%
- ~Mathlib.RepresentationTheory.Rep                           instructions    20.2%
- ~Mathlib.RingTheory.SimpleModule                            instructions    21.6%
+ ~Mathlib.RingTheory.Smooth.Basic                            instructions   -42.7%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring              instructions   -22.5%
+ ~Mathlib.Topology.Algebra.InfiniteSum.Module                instructions   -60.3%
+ ~Mathlib.Topology.Instances.AddCircle                       instructions   -59.4%

[mattrobball]

!bench

[leanprover-bot]

Here are the benchmark results for commit 00c6501.
There were significant changes against commit 21b3a48:

  Benchmark                                                   Metric         Change
  =================================================================================
+ build                                                       elaboration     -9.5%
+ ~Mathlib.Algebra.Category.AlgebraCat.Monoidal               instructions   -11.0%
- ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings           instructions     3.0%
- ~Mathlib.Algebra.Category.ModuleCat.Presheaf                instructions    12.4%
+ ~Mathlib.Algebra.DirectLimit                                instructions   -15.4%
+ ~Mathlib.Algebra.Lie.Quotient                               instructions   -72.4%
+ ~Mathlib.Algebra.Module.Submodule.Localization              instructions   -52.1%
- ~Mathlib.AlgebraicGeometry.AffineScheme                     instructions     9.7%
- ~Mathlib.AlgebraicGeometry.GammaSpecAdjunction              instructions     6.1%
+ ~Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties      instructions    -4.6%
- ~Mathlib.AlgebraicGeometry.OpenImmersion                    instructions    39.9%
- ~Mathlib.AlgebraicGeometry.Restrict                         instructions   287.5%
- ~Mathlib.AlgebraicGeometry.Scheme                           instructions   209.6%
+ ~Mathlib.Analysis.Normed.Group.Quotient                     instructions   -75.2%
+ ~Mathlib.CategoryTheory.Generator                           instructions   -48.0%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure           instructions   -43.9%
- ~Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions        instructions    52.2%
- ~Mathlib.Geometry.RingedSpace.LocallyRingedSpace            instructions   133.8%
- ~Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing        instructions     2.7%
+ ~Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits   instructions   -13.1%
+ ~Mathlib.GroupTheory.Coset                                  instructions   -79.1%
+ ~Mathlib.GroupTheory.GroupAction.Quotient                   instructions   -76.8%
+ ~Mathlib.GroupTheory.QuotientGroup                          instructions   -34.4%
+ ~Mathlib.LinearAlgebra.Isomorphisms                         instructions   -58.1%
+ ~Mathlib.LinearAlgebra.Quotient                             instructions   -28.5%
+ ~Mathlib.LinearAlgebra.QuotientPi                           instructions   -68.3%
+ ~Mathlib.LinearAlgebra.SModEq                               instructions   -89.4%
+ ~Mathlib.MeasureTheory.Measure.Haar.Quotient                instructions   -54.9%
- ~Mathlib.RepresentationTheory.Rep                           instructions    20.3%
- ~Mathlib.RingTheory.SimpleModule                            instructions    21.6%
+ ~Mathlib.RingTheory.Smooth.Basic                            instructions   -42.7%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring              instructions   -22.5%
+ ~Mathlib.Topology.Algebra.InfiniteSum.Module                instructions   -60.3%
+ ~Mathlib.Topology.Instances.AddCircle                       instructions   -59.4%

[mattrobball]

Helped a bit

[mattrobball]

!bench

[leanprover-bot]

Here are the benchmark results for commit a1924c6.
There were significant changes against commit 21b3a48:

  Benchmark                                                   Metric         Change
  =================================================================================
+ build                                                       elaboration     -9.1%
+ ~Mathlib.Algebra.Category.AlgebraCat.Monoidal               instructions   -11.0%
- ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings           instructions     3.0%
- ~Mathlib.Algebra.Category.ModuleCat.Presheaf                instructions    12.4%
+ ~Mathlib.Algebra.DirectLimit                                instructions   -15.4%
+ ~Mathlib.Algebra.Lie.Quotient                               instructions   -72.4%
+ ~Mathlib.Algebra.Module.Submodule.Localization              instructions   -52.1%
- ~Mathlib.AlgebraicGeometry.AffineScheme                     instructions     9.7%
- ~Mathlib.AlgebraicGeometry.GammaSpecAdjunction              instructions     6.1%
- ~Mathlib.AlgebraicGeometry.OpenImmersion                    instructions    39.9%
- ~Mathlib.AlgebraicGeometry.Restrict                         instructions     8.6%
- ~Mathlib.AlgebraicGeometry.Scheme                           instructions   209.6%
+ ~Mathlib.Analysis.Normed.Group.Quotient                     instructions   -75.2%
+ ~Mathlib.CategoryTheory.Generator                           instructions   -48.0%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure           instructions   -43.9%
- ~Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions        instructions    52.2%
- ~Mathlib.Geometry.RingedSpace.LocallyRingedSpace            instructions   133.8%
- ~Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing        instructions     3.0%
+ ~Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits   instructions   -13.2%
+ ~Mathlib.GroupTheory.Coset                                  instructions   -79.1%
+ ~Mathlib.GroupTheory.GroupAction.Quotient                   instructions   -76.8%
+ ~Mathlib.GroupTheory.QuotientGroup                          instructions   -34.4%
+ ~Mathlib.LinearAlgebra.Isomorphisms                         instructions   -58.1%
+ ~Mathlib.LinearAlgebra.Quotient                             instructions   -28.5%
+ ~Mathlib.LinearAlgebra.QuotientPi                           instructions   -68.3%
+ ~Mathlib.LinearAlgebra.SModEq                               instructions   -89.4%
+ ~Mathlib.MeasureTheory.Measure.Haar.Quotient                instructions   -54.9%
- ~Mathlib.RepresentationTheory.Rep                           instructions    20.3%
- ~Mathlib.RingTheory.SimpleModule                            instructions    21.6%
+ ~Mathlib.RingTheory.Smooth.Basic                            instructions   -42.7%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring              instructions   -22.5%
+ ~Mathlib.Topology.Algebra.InfiniteSum.Module                instructions   -60.3%
+ ~Mathlib.Topology.Instances.AddCircle                       instructions   -59.4%