Benchmark                                              Metric         Change
  ============================================================================
+ ~Mathlib.Algebra.Algebra.Subalgebra.Unitization        instructions   -17.2%
+ ~Mathlib.Algebra.Category.Ring.Limits                  instructions   -18.6%
+ ~Mathlib.Algebra.Lie.Killing                           instructions   -19.9%
- ~Mathlib.Algebra.Order.Ring.InjSurj                    instructions   183.3%
- ~Mathlib.Algebra.Ring.InjSurj                          instructions    79.1%
+ ~Mathlib.Algebra.Star.NonUnitalSubalgebra              instructions    -4.5%
+ ~Mathlib.AlgebraicGeometry.FunctionField               instructions   -20.2%
+ ~Mathlib.AlgebraicGeometry.GammaSpecAdjunction         instructions   -18.3%
+ ~Mathlib.AlgebraicGeometry.Properties                  instructions   -25.6%
+ ~Mathlib.AlgebraicGeometry.Spec                        instructions   -20.7%
+ ~Mathlib.FieldTheory.AbelRuffini                       instructions   -11.1%
+ ~Mathlib.FieldTheory.Adjoin                            instructions   -23.8%
+ ~Mathlib.FieldTheory.Galois                            instructions   -15.6%
+ ~Mathlib.FieldTheory.IntermediateField                 instructions   -17.2%
+ ~Mathlib.FieldTheory.PurelyInseparable                 instructions    -9.4%
+ ~Mathlib.FieldTheory.SeparableClosure                  instructions   -21.2%
+ ~Mathlib.FieldTheory.SeparableDegree                   instructions   -21.5%
+ ~Mathlib.FieldTheory.Subfield                          instructions   -46.1%
- ~Mathlib.GroupTheory.Transfer                          instructions    51.1%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv       instructions   -10.4%
+ ~Mathlib.LinearAlgebra.Dual                            instructions    -3.3%
+ ~Mathlib.LinearAlgebra.FiniteDimensional               instructions   -12.3%
+ ~Mathlib.LinearAlgebra.Isomorphisms                    instructions   -15.7%
+ ~Mathlib.LinearAlgebra.TensorProduct.Graded.Internal   instructions   -16.1%
+ ~Mathlib.MeasureTheory.Integral.SetToL1                instructions    -4.9%
+ ~Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots        instructions   -23.2%
+ ~Mathlib.NumberTheory.Cyclotomic.Rat                   instructions   -19.4%
+ ~Mathlib.NumberTheory.NumberField.Basic                instructions   -32.0%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding   instructions   -21.0%
+ ~Mathlib.NumberTheory.NumberField.ClassNumber          instructions   -40.5%
+ ~Mathlib.NumberTheory.NumberField.Discriminant         instructions   -10.3%
+ ~Mathlib.NumberTheory.NumberField.FractionalIdeal      instructions   -51.7%
+ ~Mathlib.NumberTheory.NumberField.Units                instructions   -17.9%
+ ~Mathlib.NumberTheory.RamificationInertia              instructions    -4.8%
+ ~Mathlib.RingTheory.IntegralClosure                    instructions   -12.9%
+ ~Mathlib.RingTheory.IntegralRestrict                   instructions   -10.3%
+ ~Mathlib.RingTheory.NonUnitalSubring.Basic             instructions   -25.3%
+ ~Mathlib.RingTheory.Norm                               instructions   -17.4%
+ ~Mathlib.RingTheory.Subring.Basic                      instructions   -37.5%
+ ~Mathlib.RingTheory.Subsemiring.Basic                  instructions   -52.3%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring         instructions   -18.9%