Skip to content

[Merged by Bors] - chore: reenable eta, bump to nightly 2023-05-16#3414

Closed
gebner wants to merge 68 commits intomasterfrom
reenableeta
Closed

[Merged by Bors] - chore: reenable eta, bump to nightly 2023-05-16#3414
gebner wants to merge 68 commits intomasterfrom
reenableeta

Conversation

@gebner
Copy link
Copy Markdown
Member

@gebner gebner commented Apr 12, 2023 •
edited by Ruben-VandeVelde
Loading

Now that leanprover/lean4#2210 has been merged, this PR:

Open in Gitpod

@gebner gebner added the WIP Work in progress label Apr 12, 2023
@gebner gebner marked this pull request as draft April 12, 2023 17:23
@gebner
Copy link
Copy Markdown
Member Author

gebner commented Apr 12, 2023

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Apr 12, 2023

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

@gebner
Copy link
Copy Markdown
Member Author

gebner commented Apr 12, 2023

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Apr 12, 2023

Here are the benchmark results for commit f648c85.
There were significant changes against commit c5372bb:

  Benchmark                                                     Metric                Change
  ==========================================================================================
+ build                                                         branch-misses         -13.9%
+ build                                                         branches              -21.4%
+ build                                                         elaboration           -36.3%
+ build                                                         instructions          -20.3%
+ build                                                         linting                -5.9%
- build                                                         maxrss                 11.6%
+ build                                                         simp                  -29.3%
+ build                                                         tactic execution      -54.1%
+ build                                                         task-clock            -18.4%
+ build                                                         typeclass inference   -13.7%
+ build                                                         wall-clock            -23.0%
+ lint                                                          instructions          -30.0%
+ lint                                                          wall-clock            -32.7%
+ ~Mathlib.Algebra.Algebra.Basic                                instructions          -35.7%
+ ~Mathlib.Algebra.Algebra.Bilinear                             instructions          -16.5%
+ ~Mathlib.Algebra.Algebra.Equiv                                instructions          -31.9%
+ ~Mathlib.Algebra.Algebra.Hom                                  instructions          -14.4%
+ ~Mathlib.Algebra.Algebra.Operations                           instructions          -42.2%
+ ~Mathlib.Algebra.Algebra.Pi                                   instructions          -33.5%
+ ~Mathlib.Algebra.Algebra.Prod                                 instructions          -19.9%
+ ~Mathlib.Algebra.Algebra.RestrictScalars                      instructions          -30.1%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Basic                     instructions          -26.5%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Pointwise                 instructions          -11.0%
+ ~Mathlib.Algebra.Algebra.Tower                                instructions           -5.8%
+ ~Mathlib.Algebra.Algebra.Unitization                          instructions          -15.6%
+ ~Mathlib.Algebra.BigOperators.Associated                      instructions          -47.9%
+ ~Mathlib.Algebra.BigOperators.Finsupp                         instructions          -12.6%
+ ~Mathlib.Algebra.BigOperators.Order                           instructions           -7.5%
+ ~Mathlib.Algebra.BigOperators.Pi                              instructions          -11.4%
+ ~Mathlib.Algebra.Category.GroupCat.Basic                      instructions          -21.6%
+ ~Mathlib.Algebra.Category.GroupCat.Preadditive                instructions           -5.6%
+ ~Mathlib.Algebra.Category.MonCat.Basic                        instructions          -10.2%
+ ~Mathlib.Algebra.CharP.Algebra                                instructions          -24.8%
+ ~Mathlib.Algebra.CharP.Quotient                               instructions          -19.6%
+ ~Mathlib.Algebra.CharZero.Quotient                            instructions          -26.3%
+ ~Mathlib.Algebra.CubicDiscriminant                            instructions          -61.6%
+ ~Mathlib.Algebra.DirectSum.Basic                              instructions          -22.5%
+ ~Mathlib.Algebra.DirectSum.Finsupp                            instructions          -27.8%
+ ~Mathlib.Algebra.DirectSum.Module                             instructions          -39.4%
+ ~Mathlib.Algebra.DualNumber                                   instructions          -23.2%
+ ~Mathlib.Algebra.EuclideanDomain.Basic                        instructions           -5.8%
+ ~Mathlib.Algebra.Field.Power                                  instructions           -5.5%
+ ~Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra                 instructions          -27.9%
+ ~Mathlib.Algebra.GCDMonoid.Div                                instructions          -61.2%
+ ~Mathlib.Algebra.GeomSum                                      instructions          -35.2%
+ ~Mathlib.Algebra.Group.Conj                                   instructions          -12.3%
+ ~Mathlib.Algebra.Group.Opposite                               instructions          -10.4%
+ ~Mathlib.Algebra.Group.WithOne.Units                          instructions           -7.5%
+ ~Mathlib.Algebra.GroupPower.Identities                        instructions           -7.9%
+ ~Mathlib.Algebra.GroupRingAction.Invariant                    instructions          -49.4%
+ ~Mathlib.Algebra.Hom.Centroid                                 instructions          -19.6%
+ ~Mathlib.Algebra.Hom.GroupInstances                           instructions          -12.7%
+ ~Mathlib.Algebra.Lie.Basic                                    instructions          -25.6%
+ ~Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra                 instructions           -6.2%
+ ~Mathlib.Algebra.Lie.Subalgebra                               instructions          -34.9%
+ ~Mathlib.Algebra.Module.Algebra                               instructions          -14.7%
+ ~Mathlib.Algebra.Module.Equiv                                 instructions           -7.2%
+ ~Mathlib.Algebra.Module.LinearMap                             instructions           -7.8%
+ ~Mathlib.Algebra.Module.Pi                                    instructions          -11.4%
+ ~Mathlib.Algebra.Module.Projective                            instructions          -36.2%
+ ~Mathlib.Algebra.Module.Submodule.Pointwise                   instructions           -5.6%
+ ~Mathlib.Algebra.Module.ULift                                 instructions          -16.8%
+ ~Mathlib.Algebra.MonoidAlgebra.Basic                          instructions          -43.9%
+ ~Mathlib.Algebra.MonoidAlgebra.Division                       instructions          -49.2%
+ ~Mathlib.Algebra.MonoidAlgebra.Support                        instructions          -24.4%
+ ~Mathlib.Algebra.Order.AbsoluteValue                          instructions          -16.4%
+ ~Mathlib.Algebra.Order.Archimedean                            instructions          -16.3%
+ ~Mathlib.Algebra.Order.Field.Basic                            instructions           -6.3%
+ ~Mathlib.Algebra.Order.Field.Power                            instructions           -6.2%
+ ~Mathlib.Algebra.Order.Floor                                  instructions          -11.8%
+ ~Mathlib.Algebra.Order.Group.Defs                             instructions          -11.8%
+ ~Mathlib.Algebra.Order.Group.OrderIso                         instructions           -7.0%
- ~Mathlib.Algebra.Order.Hom.Basic                              instructions            5.2%
+ ~Mathlib.Algebra.Order.Hom.Ring                               instructions           -5.2%
+ ~Mathlib.Algebra.Order.Module                                 instructions          -17.7%
+ ~Mathlib.Algebra.Order.Monoid.ToMulBot                        instructions           -6.6%
+ ~Mathlib.Algebra.Order.Nonneg.Field                           instructions          -24.1%
+ ~Mathlib.Algebra.Order.Nonneg.Ring                            instructions           -6.7%
+ ~Mathlib.Algebra.Order.Positive.Field                         instructions           -5.7%
+ ~Mathlib.Algebra.Order.Rearrangement                          instructions          -20.3%
+ ~Mathlib.Algebra.Order.Ring.Abs                               instructions           -9.4%
+ ~Mathlib.Algebra.Order.Ring.Cone                              instructions           -6.1%
+ ~Mathlib.Algebra.Order.Ring.Defs                              instructions          -14.1%
+ ~Mathlib.Algebra.Order.Ring.WithTop                           instructions           -9.2%
+ ~Mathlib.Algebra.Order.SMul                                   instructions           -8.5%
- ~Mathlib.Algebra.Order.Sub.Basic                              instructions            5.1%
+ ~Mathlib.Algebra.Order.WithZero                               instructions          -17.0%
+ ~Mathlib.Algebra.Periodic                                     instructions           -5.2%
+ ~Mathlib.Algebra.Polynomial.BigOperators                      instructions          -16.9%
+ ~Mathlib.Algebra.Polynomial.GroupRingAction                   instructions          -27.9%
+ ~Mathlib.Algebra.QuadraticDiscriminant                        instructions          -39.8%
+ ~Mathlib.Algebra.Quandle                                      instructions          -40.6%
+ ~Mathlib.Algebra.Ring.AddAut                                  instructions          -10.6%
+ ~Mathlib.Algebra.Ring.Aut                                     instructions          -12.9%
+ ~Mathlib.Algebra.Ring.CompTypeclasses                         instructions           -8.6%
+ ~Mathlib.Algebra.Ring.Equiv                                   instructions           -8.1%
+ ~Mathlib.Algebra.Ring.Opposite                                instructions          -15.6%
+ ~Mathlib.Algebra.Ring.Prod                                    instructions          -10.4%
+ ~Mathlib.Algebra.Star.Basic                                   instructions           -6.5%
+ ~Mathlib.Algebra.Star.CHSH                                    instructions          -67.3%
+ ~Mathlib.Algebra.Star.Free                                    instructions           -7.1%
+ ~Mathlib.Algebra.Star.Module                                  instructions          -34.4%
+ ~Mathlib.Algebra.Star.SelfAdjoint                             instructions          -20.1%
+ ~Mathlib.Algebra.Star.StarAlgHom                              instructions          -10.2%
+ ~Mathlib.Algebra.Star.Subalgebra                              instructions           -7.5%
+ ~Mathlib.Algebra.TrivSqZeroExt                                instructions          -30.1%
- ~Mathlib.Algebra.Tropical.Basic                               instructions            5.0%
+ ~Mathlib.Algebra.Tropical.Lattice                             instructions           -6.8%
+ ~Mathlib.AlgebraicTopology.DoldKan.Compatibility              instructions          -43.8%
+ ~Mathlib.Analysis.Convex.Function                             instructions          -10.2%
+ ~Mathlib.Analysis.Convex.Segment                              instructions           -8.7%
+ ~Mathlib.Analysis.Convex.Strict                               instructions           -5.3%
+ ~Mathlib.Analysis.Hofer                                       instructions           -7.1%
+ ~Mathlib.Analysis.LocallyConvex.Polar                         instructions          -73.3%
+ ~Mathlib.Analysis.Normed.Field.Basic                          instructions          -12.5%
+ ~Mathlib.Analysis.Normed.Field.InfiniteSum                    instructions          -17.4%
+ ~Mathlib.Analysis.Normed.Group.Basic                          instructions           -6.1%
+ ~Mathlib.Analysis.Normed.Group.Hom                            instructions          -11.7%
+ ~Mathlib.Analysis.Normed.Group.HomCompletion                  instructions          -49.9%
+ ~Mathlib.Analysis.Normed.Group.InfiniteSum                    instructions           -5.5%
+ ~Mathlib.Analysis.SpecificLimits.Basic                        instructions          -19.4%
+ ~Mathlib.CategoryTheory.Abelian.Basic                         instructions          -10.4%
+ ~Mathlib.CategoryTheory.Abelian.FunctorCategory               instructions          -40.5%
+ ~Mathlib.CategoryTheory.Adjunction.FullyFaithful              instructions          -14.1%
+ ~Mathlib.CategoryTheory.Adjunction.Limits                     instructions          -31.7%
+ ~Mathlib.CategoryTheory.Adjunction.Whiskering                 instructions          -62.7%
+ ~Mathlib.CategoryTheory.Arrow                                 instructions           -8.3%
+ ~Mathlib.CategoryTheory.Category.Bipointed                    instructions          -13.6%
+ ~Mathlib.CategoryTheory.Category.Cat                          instructions          -51.5%
+ ~Mathlib.CategoryTheory.Category.QuivCat                      instructions           -7.0%
+ ~Mathlib.CategoryTheory.Category.TwoP                         instructions          -29.7%
+ ~Mathlib.CategoryTheory.Elements                              instructions          -47.4%
+ ~Mathlib.CategoryTheory.Equivalence                           instructions           -6.2%
+ ~Mathlib.CategoryTheory.EssentialImage                        instructions           -7.1%
+ ~Mathlib.CategoryTheory.FinCategory                           instructions          -29.0%
+ ~Mathlib.CategoryTheory.FintypeCat                            instructions           -9.1%
+ ~Mathlib.CategoryTheory.Functor.Currying                      instructions          -17.4%
+ ~Mathlib.CategoryTheory.Functor.InvIsos                       instructions           -6.5%
+ ~Mathlib.CategoryTheory.Grothendieck                          instructions          -34.4%
+ ~Mathlib.CategoryTheory.Idempotents.FunctorCategories         instructions          -11.2%
+ ~Mathlib.CategoryTheory.Idempotents.FunctorExtension          instructions          -75.4%
+ ~Mathlib.CategoryTheory.Idempotents.Karoubi                   instructions           -7.3%
+ ~Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi            instructions          -25.2%
+ ~Mathlib.CategoryTheory.Limits.ColimitLimit                   instructions          -42.2%
+ ~Mathlib.CategoryTheory.Limits.Comma                          instructions          -34.8%
+ ~Mathlib.CategoryTheory.Limits.Cones                          instructions          -10.4%
+ ~Mathlib.CategoryTheory.Limits.Constructions.Over.Connected   instructions           -7.2%
+ ~Mathlib.CategoryTheory.Limits.Creates                        instructions           -5.2%
+ ~Mathlib.CategoryTheory.Limits.ExactFunctor                   instructions          -11.7%
+ ~Mathlib.CategoryTheory.Limits.FunctorCategory                instructions          -19.0%
+ ~Mathlib.CategoryTheory.Limits.HasLimits                      instructions          -13.8%
+ ~Mathlib.CategoryTheory.Limits.KanExtension                   instructions          -35.0%
+ ~Mathlib.CategoryTheory.Limits.Opposites                      instructions          -16.0%
+ ~Mathlib.CategoryTheory.Limits.Preserves.Basic                instructions          -19.6%
+ ~Mathlib.CategoryTheory.Limits.Preserves.Limits               instructions           -7.9%
+ ~Mathlib.CategoryTheory.Limits.Preserves.Opposites            instructions          -27.1%
+ ~Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer          instructions           -6.0%
+ ~Mathlib.CategoryTheory.Limits.Shapes.Products                instructions           -6.7%
+ ~Mathlib.CategoryTheory.Limits.Shapes.Types                   instructions           -5.6%
+ ~Mathlib.CategoryTheory.Linear.Basic                          instructions          -75.3%
+ ~Mathlib.CategoryTheory.Localization.Construction             instructions          -50.9%
+ ~Mathlib.CategoryTheory.Localization.Opposite                 instructions          -40.5%
+ ~Mathlib.CategoryTheory.Localization.Predicate                instructions          -25.3%
+ ~Mathlib.CategoryTheory.Monoidal.Functor                      instructions           -7.3%
+ ~Mathlib.CategoryTheory.Monoidal.NaturalTransformation        instructions           -8.1%
+ ~Mathlib.CategoryTheory.Monoidal.Transport                    instructions          -12.7%
+ ~Mathlib.CategoryTheory.Opposites                             instructions          -19.5%
+ ~Mathlib.CategoryTheory.Over                                  instructions           -6.8%
+ ~Mathlib.CategoryTheory.PEmpty                                instructions           -5.5%
+ ~Mathlib.CategoryTheory.Preadditive.AdditiveFunctor           instructions           -8.5%
+ ~Mathlib.CategoryTheory.Products.Basic                        instructions           -9.3%
+ ~Mathlib.CategoryTheory.Shift.Basic                           instructions           -5.8%
+ ~Mathlib.CategoryTheory.Sigma.Basic                           instructions          -16.0%
+ ~Mathlib.CategoryTheory.SingleObj                             instructions          -23.3%
+ ~Mathlib.CategoryTheory.Sites.Plus                            instructions          -44.0%
+ ~Mathlib.CategoryTheory.Sites.Sheaf                           instructions           -7.3%
+ ~Mathlib.CategoryTheory.Skeletal                              instructions           -6.2%
+ ~Mathlib.CategoryTheory.StructuredArrow                       instructions           -7.3%
+ ~Mathlib.CategoryTheory.Whiskering                            instructions          -24.2%
+ ~Mathlib.CategoryTheory.Yoneda                                instructions          -34.5%
+ ~Mathlib.Combinatorics.Additive.Energy                        instructions           -5.2%
+ ~Mathlib.Combinatorics.Additive.PluenneckeRuzsa               instructions          -12.9%
+ ~Mathlib.Combinatorics.Catalan                                instructions          -54.9%
+ ~Mathlib.Combinatorics.Composition                            instructions           -5.7%
+ ~Mathlib.Combinatorics.SetFamily.Compression.UV               instructions           -7.2%
+ ~Mathlib.Combinatorics.SetFamily.Kleitman                     instructions          -17.3%
+ ~Mathlib.Combinatorics.SetFamily.LYM                          instructions           -8.5%
+ ~Mathlib.Combinatorics.SimpleGraph.Density                    instructions          -13.4%
+ ~Mathlib.Combinatorics.SimpleGraph.Matching                   instructions          -15.1%
+ ~Mathlib.Combinatorics.SimpleGraph.Prod                       instructions           -7.1%
+ ~Mathlib.Combinatorics.SimpleGraph.Regularity.Energy          instructions           -6.5%
+ ~Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform         instructions           -5.9%
- ~Mathlib.Computability.Language                               instructions            5.1%
- ~Mathlib.Computability.RegularExpressions                     instructions            5.8%
+ ~Mathlib.Control.LawfulFix                                    instructions          -30.1%
+ ~Mathlib.Data.Complex.Basic                                   instructions          -61.9%
+ ~Mathlib.Data.Complex.Exponential                             instructions          -36.9%
+ ~Mathlib.Data.Dfinsupp.Basic                                  instructions          -16.5%
+ ~Mathlib.Data.Dfinsupp.Multiset                               instructions           -5.3%
+ ~Mathlib.Data.Dfinsupp.NeLocus                                instructions          -12.5%
- ~Mathlib.Data.Fin.Basic                                       instructions           14.4%
+ ~Mathlib.Data.Fin.Tuple.BubbleSortInduction                   instructions          -17.6%
+ ~Mathlib.Data.Fin.Tuple.Sort                                  instructions          -10.0%
+ ~Mathlib.Data.Finset.Pi                                       instructions          -19.5%
+ ~Mathlib.Data.Finset.Sym                                      instructions           -7.3%
+ ~Mathlib.Data.Finsupp.Antidiagonal                            instructions          -42.0%
+ ~Mathlib.Data.Finsupp.Basic                                   instructions          -13.5%
+ ~Mathlib.Data.Finsupp.Multiset                                instructions          -62.0%
+ ~Mathlib.Data.Finsupp.NeLocus                                 instructions          -14.8%
+ ~Mathlib.Data.Finsupp.ToDfinsupp                              instructions          -17.3%
+ ~Mathlib.Data.Fintype.Basic                                   instructions           -7.7%
+ ~Mathlib.Data.Fintype.Powerset                                instructions          -22.4%
+ ~Mathlib.Data.Int.AbsoluteValue                               instructions          -44.6%
+ ~Mathlib.Data.Int.Associated                                  instructions           -6.0%
+ ~Mathlib.Data.Int.Cast.Lemmas                                 instructions           -5.5%
+ ~Mathlib.Data.Int.Cast.Prod                                   instructions           -6.7%
- ~Mathlib.Data.Int.ConditionallyCompleteOrder                  instructions           15.9%
+ ~Mathlib.Data.Int.Log                                         instructions          -39.2%
+ ~Mathlib.Data.List.Cycle                                      instructions          -16.7%
+ ~Mathlib.Data.Matrix.Basic                                    instructions          -19.2%
+ ~Mathlib.Data.Matrix.DualNumber                               instructions          -22.0%
+ ~Mathlib.Data.MvPolynomial.Basic                              instructions          -17.9%
+ ~Mathlib.Data.MvPolynomial.CommRing                           instructions          -51.0%
- ~Mathlib.Data.MvPolynomial.Division                           instructions            5.7%
+ ~Mathlib.Data.MvPolynomial.Equiv                              instructions          -58.1%
+ ~Mathlib.Data.MvPolynomial.Expand                             instructions          -33.7%
+ ~Mathlib.Data.MvPolynomial.Monad                              instructions          -28.8%
+ ~Mathlib.Data.MvPolynomial.Rename                             instructions          -27.8%
+ ~Mathlib.Data.MvPolynomial.Supported                          instructions          -47.1%
+ ~Mathlib.Data.MvPolynomial.Variables                          instructions           -7.4%
- ~Mathlib.Data.Nat.Bitwise                                     instructions            5.6%
+ ~Mathlib.Data.Nat.Cast.Field                                  instructions           -5.5%
+ ~Mathlib.Data.Nat.Choose.Bounds                               instructions           -6.0%
+ ~Mathlib.Data.Nat.Factorization.Basic                         instructions          -20.1%
+ ~Mathlib.Data.Nat.Order.Basic                                 instructions          -10.5%
+ ~Mathlib.Data.Nat.PSub                                        instructions           -7.1%
+ ~Mathlib.Data.Nat.Prime                                       instructions           -5.2%
+ ~Mathlib.Data.Nat.Totient                                     instructions          -10.0%
+ ~Mathlib.Data.PFunctor.Multivariate.M                         instructions           -6.5%
+ ~Mathlib.Data.PNat.Interval                                   instructions           -7.5%
+ ~Mathlib.Data.Pi.Interval                                     instructions           -9.9%
+ ~Mathlib.Data.Polynomial.Basic                                instructions           -9.7%
+ ~Mathlib.Data.Polynomial.Coeff                                instructions           -5.2%
+ ~Mathlib.Data.Polynomial.Degree.CardPowDegree                 instructions          -52.2%
+ ~Mathlib.Data.Polynomial.Degree.Definitions                   instructions           -9.5%
+ ~Mathlib.Data.Polynomial.Degree.Lemmas                        instructions           -6.0%
+ ~Mathlib.Data.Polynomial.DenomsClearable                      instructions          -56.1%
+ ~Mathlib.Data.Polynomial.Derivative                           instructions          -29.7%
+ ~Mathlib.Data.Polynomial.Div                                  instructions          -18.4%
+ ~Mathlib.Data.Polynomial.EraseLead                            instructions           -6.5%
+ ~Mathlib.Data.Polynomial.Eval                                 instructions          -24.6%
+ ~Mathlib.Data.Polynomial.FieldDivision                        instructions          -78.5%
+ ~Mathlib.Data.Polynomial.HasseDeriv                           instructions          -42.2%
+ ~Mathlib.Data.Polynomial.IntegralNormalization                instructions           -6.5%
+ ~Mathlib.Data.Polynomial.Lifts                                instructions          -39.8%
+ ~Mathlib.Data.Polynomial.Monic                                instructions           -6.5%
+ ~Mathlib.Data.Polynomial.Monomial                             instructions          -64.5%
+ ~Mathlib.Data.Polynomial.PartialFractions                     instructions          -72.1%
+ ~Mathlib.Data.Polynomial.Reverse                              instructions           -6.1%
+ ~Mathlib.Data.Polynomial.RingDivision                         instructions          -22.0%
+ ~Mathlib.Data.Polynomial.Splits                               instructions          -83.4%
+ ~Mathlib.Data.Polynomial.Taylor                               instructions          -12.1%
+ ~Mathlib.Data.Rat.BigOperators                                instructions           -6.1%
+ ~Mathlib.Data.Rat.Cast                                        instructions          -17.1%
+ ~Mathlib.Data.Rat.Floor                                       instructions          -22.4%
+ ~Mathlib.Data.Rat.Lemmas                                      instructions           -6.3%
+ ~Mathlib.Data.Rat.NNRat                                       instructions          -25.4%
+ ~Mathlib.Data.Rat.Order                                       instructions           -8.4%
+ ~Mathlib.Data.Real.Basic                                      instructions          -62.6%
+ ~Mathlib.Data.Real.CauSeq                                     instructions          -44.9%
+ ~Mathlib.Data.Real.CauSeqCompletion                           instructions          -39.4%
+ ~Mathlib.Data.Real.ConjugateExponents                         instructions           -6.4%
+ ~Mathlib.Data.Real.ENNReal                                    instructions          -35.2%
+ ~Mathlib.Data.Real.ENatENNReal                                instructions          -49.6%
+ ~Mathlib.Data.Real.EReal                                      instructions           -9.3%
+ ~Mathlib.Data.Real.NNReal                                     instructions          -32.4%
+ ~Mathlib.Data.Real.Pointwise                                  instructions          -12.4%
+ ~Mathlib.Data.Real.Sqrt                                       instructions          -11.6%
+ ~Mathlib.Data.Set.Intervals.Disjoint                          instructions           -5.6%
+ ~Mathlib.Data.Set.Intervals.IsoIoo                            instructions          -16.7%
+ ~Mathlib.Data.Set.Intervals.SurjOn                            instructions           -7.7%
- ~Mathlib.Data.Set.Semiring                                    instructions            8.7%
+ ~Mathlib.Data.Vector.Basic                                    instructions          -18.3%
+ ~Mathlib.Data.ZMod.Basic                                      instructions           -6.4%
- ~Mathlib.Data.ZMod.Coprime                                    instructions            7.7%
+ ~Mathlib.Data.ZMod.Defs                                       instructions           -8.4%
+ ~Mathlib.Deprecated.Subfield                                  instructions          -12.4%
+ ~Mathlib.Deprecated.Subring                                   instructions          -11.6%
+ ~Mathlib.FieldTheory.MvPolynomial                             instructions          -55.0%
+ ~Mathlib.FieldTheory.PerfectClosure                           instructions          -10.5%
+ ~Mathlib.FieldTheory.Subfield                                 instructions          -22.4%
+ ~Mathlib.GroupTheory.Abelianization                           instructions          -22.4%
+ ~Mathlib.GroupTheory.Commutator                               instructions           -7.9%
+ ~Mathlib.GroupTheory.CommutingProbability                     instructions          -14.5%
- ~Mathlib.GroupTheory.Divisible                                instructions           10.7%
+ ~Mathlib.GroupTheory.Finiteness                               instructions           -6.8%
+ ~Mathlib.GroupTheory.FreeAbelianGroup                         instructions          -16.4%
+ ~Mathlib.GroupTheory.FreeProduct                              instructions          -36.2%
+ ~Mathlib.GroupTheory.GroupAction.ConjAct                      instructions          -26.4%
+ ~Mathlib.GroupTheory.GroupAction.FixingSubgroup               instructions           -9.3%
+ ~Mathlib.GroupTheory.Index                                    instructions           -5.9%
+ ~Mathlib.GroupTheory.IsFreeGroup                              instructions           -5.8%
+ ~Mathlib.GroupTheory.Perm.Basic                               instructions           -5.9%
+ ~Mathlib.GroupTheory.Perm.Cycle.Basic                         instructions          -19.7%
+ ~Mathlib.GroupTheory.Perm.Cycle.Type                          instructions          -22.6%
- ~Mathlib.GroupTheory.Perm.Fin                                 instructions            5.4%
+ ~Mathlib.GroupTheory.Perm.Sign                                instructions           -9.9%
+ ~Mathlib.GroupTheory.Perm.Subgroup                            instructions           -9.7%
+ ~Mathlib.GroupTheory.QuotientGroup                            instructions           -6.2%
+ ~Mathlib.GroupTheory.SemidirectProduct                        instructions           -5.0%
+ ~Mathlib.GroupTheory.Subgroup.Basic                           instructions           -6.9%
+ ~Mathlib.GroupTheory.Subgroup.Finite                          instructions          -10.4%
+ ~Mathlib.GroupTheory.Subgroup.Pointwise                       instructions           -9.9%
+ ~Mathlib.GroupTheory.Submonoid.Pointwise                      instructions          -20.4%
+ ~Mathlib.LinearAlgebra.AffineSpace.AffineEquiv                instructions          -17.4%
+ ~Mathlib.LinearAlgebra.AffineSpace.AffineMap                  instructions          -44.4%
+ ~Mathlib.LinearAlgebra.AffineSpace.AffineSubspace             instructions          -12.1%
+ ~Mathlib.LinearAlgebra.AffineSpace.Combination                instructions          -57.0%
+ ~Mathlib.LinearAlgebra.AffineSpace.MidpointZero               instructions          -17.9%
+ ~Mathlib.LinearAlgebra.AffineSpace.Ordered                    instructions          -42.0%
+ ~Mathlib.LinearAlgebra.AffineSpace.Restrict                   instructions          -60.1%
+ ~Mathlib.LinearAlgebra.AffineSpace.Slope                      instructions          -21.5%
+ ~Mathlib.LinearAlgebra.Alternating                            instructions          -44.4%
+ ~Mathlib.LinearAlgebra.Basic                                  instructions          -11.2%
+ ~Mathlib.LinearAlgebra.Basis                                  instructions          -28.1%
+ ~Mathlib.LinearAlgebra.BilinearMap                            instructions          -21.9%
+ ~Mathlib.LinearAlgebra.Dfinsupp                               instructions          -21.5%
+ ~Mathlib.LinearAlgebra.Dimension                              instructions          -63.3%
- ~Mathlib.LinearAlgebra.DirectSum.Finsupp                      instructions           29.6%
+ ~Mathlib.LinearAlgebra.DirectSum.TensorProduct                instructions          -33.4%
+ ~Mathlib.LinearAlgebra.Finsupp                                instructions          -35.3%
+ ~Mathlib.LinearAlgebra.FinsuppVectorSpace                     instructions          -12.5%
+ ~Mathlib.LinearAlgebra.FreeModule.Basic                       instructions          -19.8%
+ ~Mathlib.LinearAlgebra.FreeModule.Finite.Basic                instructions          -20.9%
+ ~Mathlib.LinearAlgebra.InvariantBasisNumber                   instructions          -51.7%
+ ~Mathlib.LinearAlgebra.Isomorphisms                           instructions          -81.7%
+ ~Mathlib.LinearAlgebra.LinearIndependent                      instructions          -26.4%
+ ~Mathlib.LinearAlgebra.LinearPMap                             instructions          -15.2%
+ ~Mathlib.LinearAlgebra.Multilinear.TensorProduct              instructions           -7.1%
+ ~Mathlib.LinearAlgebra.Prod                                   instructions          -18.4%
+ ~Mathlib.LinearAlgebra.Projection                             instructions          -43.1%
+ ~Mathlib.LinearAlgebra.Quotient                               instructions          -13.9%
+ ~Mathlib.LinearAlgebra.Ray                                    instructions          -23.9%
+ ~Mathlib.LinearAlgebra.SModEq                                 instructions           -7.8%
+ ~Mathlib.LinearAlgebra.SesquilinearForm                       instructions          -70.7%
+ ~Mathlib.LinearAlgebra.Span                                   instructions           -6.9%
+ ~Mathlib.LinearAlgebra.StdBasis                               instructions          -34.1%
+ ~Mathlib.LinearAlgebra.TensorProduct                          instructions          -14.6%
+ ~Mathlib.LinearAlgebra.TensorProductBasis                     instructions          -45.3%
+ ~Mathlib.Logic.Denumerable                                    instructions           -7.5%
+ ~Mathlib.Logic.Equiv.Defs                                     instructions          -10.3%
+ ~Mathlib.Logic.Equiv.List                                     instructions           -8.4%
+ ~Mathlib.Logic.Hydra                                          instructions           -7.4%
- ~Mathlib.MeasureTheory.MeasurableSpace                        instructions           11.4%
+ ~Mathlib.NumberTheory.ADEInequality                           instructions           -5.5%
+ ~Mathlib.NumberTheory.Basic                                   instructions          -43.6%
+ ~Mathlib.NumberTheory.ClassNumber.AdmissibleAbs               instructions          -24.4%
+ ~Mathlib.NumberTheory.Fermat4                                 instructions           -7.2%
+ ~Mathlib.NumberTheory.LucasPrimality                          instructions          -19.4%
+ ~Mathlib.NumberTheory.Padics.PadicNorm                        instructions          -13.5%
+ ~Mathlib.NumberTheory.Primorial                               instructions           -7.3%
+ ~Mathlib.NumberTheory.PythagoreanTriples                      instructions          -37.2%
+ ~Mathlib.NumberTheory.Zsqrtd.Basic                            instructions          -40.9%
- ~Mathlib.Order.Bounded                                        instructions            5.7%
+ ~Mathlib.Order.Category.LatCat                                instructions          -45.8%
+ ~Mathlib.Order.Category.LinOrdCat                             instructions          -54.5%
+ ~Mathlib.Order.Category.NonemptyFinLinOrdCat                  instructions          -13.8%
+ ~Mathlib.Order.Category.PartOrdCat                            instructions          -23.3%
+ ~Mathlib.Order.Category.PreordCat                             instructions          -20.3%
+ ~Mathlib.Order.CompleteLatticeIntervals                       instructions          -13.5%
+ ~Mathlib.Order.ConditionallyCompleteLattice.Basic             instructions           -7.1%
+ ~Mathlib.Order.Disjointed                                     instructions          -12.8%
+ ~Mathlib.Order.Filter.Archimedean                             instructions          -10.2%
+ ~Mathlib.Order.Filter.Basic                                   instructions           -6.2%
+ ~Mathlib.Order.Filter.ENNReal                                 instructions           -9.7%
+ ~Mathlib.Order.Filter.Pointwise                               instructions          -19.7%
+ ~Mathlib.Order.Filter.Ultrafilter                             instructions          -38.7%
+ ~Mathlib.Order.FixedPoints                                    instructions           -6.5%
+ ~Mathlib.Order.GaloisConnection                               instructions           -5.4%
+ ~Mathlib.Order.Heyting.Basic                                  instructions           -6.4%
+ ~Mathlib.Order.Heyting.Regular                                instructions          -13.2%
+ ~Mathlib.Order.JordanHolder                                   instructions           -6.1%
+ ~Mathlib.Order.OmegaCompletePartialOrder                      instructions           -8.0%
+ ~Mathlib.Order.RelIso.Group                                   instructions          -39.7%
+ ~Mathlib.Order.SuccPred.IntervalSucc                          instructions          -10.6%
+ ~Mathlib.RepresentationTheory.Maschke                         instructions          -74.1%
+ ~Mathlib.RingTheory.Adjoin.Basic                              instructions          -54.6%
+ ~Mathlib.RingTheory.Adjoin.Fg                                 instructions          -56.5%
+ ~Mathlib.RingTheory.Adjoin.Tower                              instructions          -67.5%
+ ~Mathlib.RingTheory.AlgebraTower                              instructions           -6.5%
+ ~Mathlib.RingTheory.Coprime.Ideal                             instructions          -19.8%
+ ~Mathlib.RingTheory.EisensteinCriterion                       instructions          -52.6%
+ ~Mathlib.RingTheory.EuclideanDomain                           instructions          -20.3%
+ ~Mathlib.RingTheory.FiniteType                                instructions          -77.9%
+ ~Mathlib.RingTheory.Finiteness                                instructions          -39.0%
+ ~Mathlib.RingTheory.Flat                                      instructions          -17.2%
+ ~Mathlib.RingTheory.FreeRing                                  instructions          -15.8%
+ ~Mathlib.RingTheory.Ideal.Basic                               instructions          -10.4%
+ ~Mathlib.RingTheory.Ideal.IdempotentFg                        instructions          -69.0%
+ ~Mathlib.RingTheory.Ideal.Operations                          instructions          -51.1%
+ ~Mathlib.RingTheory.Ideal.Prod                                instructions          -61.9%
+ ~Mathlib.RingTheory.Ideal.Quotient                            instructions          -43.6%
+ ~Mathlib.RingTheory.Ideal.QuotientOperations                  instructions          -24.6%
+ ~Mathlib.RingTheory.Localization.Basic                        instructions          -45.6%
+ ~Mathlib.RingTheory.Localization.FractionRing                 instructions          -60.2%
+ ~Mathlib.RingTheory.Localization.Integer                      instructions          -39.8%
+ ~Mathlib.RingTheory.Localization.Module                       instructions          -36.6%
+ ~Mathlib.RingTheory.Localization.NumDen                       instructions          -23.9%
+ ~Mathlib.RingTheory.MvPolynomial.Basic                        instructions          -56.3%
+ ~Mathlib.RingTheory.MvPolynomial.Symmetric                    instructions          -33.6%
+ ~Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous          instructions          -15.0%
+ ~Mathlib.RingTheory.Nilpotent                                 instructions           -6.9%
+ ~Mathlib.RingTheory.Noetherian                                instructions          -15.2%
+ ~Mathlib.RingTheory.OreLocalization.Basic                     instructions          -21.2%
+ ~Mathlib.RingTheory.Polynomial.Basic                          instructions          -61.6%
+ ~Mathlib.RingTheory.Polynomial.Chebyshev                      instructions          -26.7%
+ ~Mathlib.RingTheory.Polynomial.Content                        instructions          -26.8%
- ~Mathlib.RingTheory.Polynomial.Opposites                      instructions           10.8%
+ ~Mathlib.RingTheory.Polynomial.ScaleRoots                     instructions          -23.6%
+ ~Mathlib.RingTheory.Prime                                     instructions          -15.1%
+ ~Mathlib.RingTheory.PrincipalIdealDomain                      instructions          -51.4%
+ ~Mathlib.RingTheory.QuotientNilpotent                         instructions          -48.8%
+ ~Mathlib.RingTheory.QuotientNoetherian                        instructions          -13.2%
+ ~Mathlib.RingTheory.ReesAlgebra                               instructions          -70.6%
+ ~Mathlib.RingTheory.SimpleModule                              instructions          -89.7%
+ ~Mathlib.RingTheory.Subring.Basic                             instructions          -31.1%
+ ~Mathlib.RingTheory.Subring.Pointwise                         instructions          -11.2%
+ ~Mathlib.RingTheory.Subsemiring.Basic                         instructions           -5.8%
- ~Mathlib.RingTheory.Valuation.Basic                           instructions            6.4%
- ~Mathlib.RingTheory.Valuation.Integers                        instructions            6.4%
+ ~Mathlib.RingTheory.Valuation.Quotient                        instructions          -41.7%
- ~Mathlib.RingTheory.ZMod                                      instructions           10.6%
+ ~Mathlib.SetTheory.Cardinal.Cofinality                        instructions          -57.7%
+ ~Mathlib.SetTheory.Cardinal.Divisibility                      instructions           -5.9%
+ ~Mathlib.SetTheory.Ordinal.Arithmetic                         instructions          -45.0%
+ ~Mathlib.SetTheory.Ordinal.FixedPoint                         instructions          -44.4%
+ ~Mathlib.SetTheory.Ordinal.NaturalOps                         instructions           -7.1%
+ ~Mathlib.Topology.Algebra.Algebra                             instructions           -6.7%
+ ~Mathlib.Topology.Algebra.Field                               instructions          -39.2%
+ ~Mathlib.Topology.Algebra.Group.Basic                         instructions           -7.6%
+ ~Mathlib.Topology.Algebra.GroupCompletion                     instructions           -8.9%
+ ~Mathlib.Topology.Algebra.GroupWithZero                       instructions          -14.1%
+ ~Mathlib.Topology.Algebra.InfiniteSum.Real                    instructions           -7.0%
+ ~Mathlib.Topology.Algebra.Localization                        instructions          -15.3%
+ ~Mathlib.Topology.Algebra.Module.Basic                        instructions          -54.7%
+ ~Mathlib.Topology.Algebra.Module.LinearPMap                   instructions           -5.8%
+ ~Mathlib.Topology.Algebra.Module.Simple                       instructions          -21.9%
+ ~Mathlib.Topology.Algebra.Module.WeakDual                     instructions          -51.6%
+ ~Mathlib.Topology.Algebra.Nonarchimedean.Basic                instructions           -9.5%
+ ~Mathlib.Topology.Algebra.Order.Compact                       instructions           -5.6%
+ ~Mathlib.Topology.Algebra.Order.Field                         instructions           -7.8%
+ ~Mathlib.Topology.Algebra.Order.Floor                         instructions           -5.1%
+ ~Mathlib.Topology.Algebra.Order.IntermediateValue             instructions          -15.5%
+ ~Mathlib.Topology.Algebra.Order.LiminfLimsup                  instructions           -5.1%
+ ~Mathlib.Topology.Algebra.Polynomial                          instructions          -44.9%
+ ~Mathlib.Topology.Algebra.Ring.Basic                          instructions          -36.8%
+ ~Mathlib.Topology.Algebra.StarSubalgebra                      instructions          -57.0%
+ ~Mathlib.Topology.Algebra.UniformField                        instructions          -38.6%
+ ~Mathlib.Topology.Algebra.UniformRing                         instructions          -17.7%
+ ~Mathlib.Topology.Basic                                       instructions           -5.5%
- ~Mathlib.Topology.ContinuousFunction.T0Sierpinski             instructions            9.4%
- ~Mathlib.Topology.FiberBundle.Trivialization                  instructions            7.3%
+ ~Mathlib.Topology.Filter                                      instructions           -5.7%
+ ~Mathlib.Topology.Homotopy.Equiv                              instructions           -5.2%
+ ~Mathlib.Topology.Instances.ENNReal                           instructions          -34.4%
+ ~Mathlib.Topology.Instances.EReal                             instructions          -10.4%
+ ~Mathlib.Topology.Instances.NNReal                            instructions          -30.8%
+ ~Mathlib.Topology.Instances.Nat                               instructions          -17.8%
+ ~Mathlib.Topology.Instances.Real                              instructions          -14.6%
+ ~Mathlib.Topology.Instances.RealVectorSpace                   instructions          -15.8%
+ ~Mathlib.Topology.Instances.TrivSqZeroExt                     instructions           -6.7%
+ ~Mathlib.Topology.LocalHomeomorph                             instructions          -37.9%
+ ~Mathlib.Topology.LocallyConstant.Algebra                     instructions           -5.6%
+ ~Mathlib.Topology.MetricSpace.Algebra                         instructions          -15.3%
+ ~Mathlib.Topology.MetricSpace.CauSeqFilter                    instructions          -12.2%
+ ~Mathlib.Topology.MetricSpace.Completion                      instructions           -6.3%
+ ~Mathlib.Topology.MetricSpace.EMetricSpace                    instructions           -5.2%
+ ~Mathlib.Topology.MetricSpace.HausdorffDistance               instructions          -12.2%
+ ~Mathlib.Topology.MetricSpace.Infsep                          instructions           -7.2%
+ ~Mathlib.Topology.MetricSpace.Isometry                        instructions          -10.9%
+ ~Mathlib.Topology.MetricSpace.Lipschitz                       instructions           -7.9%
+ ~Mathlib.Topology.MetricSpace.PiNat                           instructions          -35.2%
- ~Mathlib.Topology.OmegaCompletePartialOrder                   instructions            8.9%
+ ~Mathlib.Topology.Order                                       instructions          -12.3%
+ ~Mathlib.Topology.PathConnected                               instructions           -9.4%
+ ~Mathlib.Topology.Separation                                  instructions           -8.5%
+ ~Mathlib.Topology.Sequences                                   instructions           -5.2%
+ ~Mathlib.Topology.Sets.Closeds                                instructions          -62.0%
- ~Mathlib.Topology.Sets.Compacts                               instructions           13.0%
+ ~Mathlib.Topology.Sets.Opens                                  instructions           -6.7%
+ ~Mathlib.Topology.StoneCech                                   instructions          -11.2%
+ ~Mathlib.Topology.UniformSpace.AbsoluteValue                  instructions          -13.5%
+ ~Mathlib.Topology.UniformSpace.Compact                        instructions           -5.1%
+ ~Mathlib.Topology.UniformSpace.CompareReals                   instructions          -19.9%
+ ~Mathlib.Topology.UniformSpace.Completion                     instructions          -25.2%
+ ~Mathlib.Topology.UniformSpace.Pi                             instructions           -9.1%
+ ~Mathlib.Topology.UniformSpace.Separation                     instructions           -7.0%
+ ~Mathlib.Topology.UniformSpace.UniformConvergenceTopology     instructions          -36.0%
- ~Qq.AssertInstancesCommute                                    instructions           10.7%

@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 13, 2023
@kim-em kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 6, 2023
@gebner
Copy link
Copy Markdown
Member Author

gebner commented May 8, 2023

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented May 8, 2023

Here are the benchmark results for commit 6cd73ad.
There were significant changes against commit 9ff903e:

  Benchmark                                                           Metric                Change
  ================================================================================================
+ build                                                               aesop                  -6.6%
+ build                                                               branch-misses         -19.4%
+ build                                                               branches              -26.8%
+ build                                                               elaboration           -41.1%
+ build                                                               instructions          -25.8%
+ build                                                               interpretation         -6.4%
+ build                                                               simp                  -33.0%
+ build                                                               tactic execution      -57.7%
+ build                                                               task-clock            -22.0%
+ build                                                               typeclass inference   -16.1%
+ build                                                               wall-clock            -23.6%
+ lint                                                                instructions          -39.9%
+ lint                                                                wall-clock            -42.0%
+ ~Mathlib.Algebra.Algebra.Basic                                      instructions          -29.1%
+ ~Mathlib.Algebra.Algebra.Bilinear                                   instructions          -17.9%
+ ~Mathlib.Algebra.Algebra.Equiv                                      instructions          -24.3%
+ ~Mathlib.Algebra.Algebra.Hom                                        instructions          -11.3%
+ ~Mathlib.Algebra.Algebra.Operations                                 instructions          -42.8%
+ ~Mathlib.Algebra.Algebra.Pi                                         instructions          -30.8%
+ ~Mathlib.Algebra.Algebra.Prod                                       instructions          -18.2%
+ ~Mathlib.Algebra.Algebra.RestrictScalars                            instructions          -35.1%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Basic                           instructions          -24.9%
+ ~Mathlib.Algebra.Algebra.Tower                                      instructions           -6.1%
+ ~Mathlib.Algebra.Algebra.Unitization                                instructions          -15.9%
+ ~Mathlib.Algebra.BigOperators.Associated                            instructions          -43.7%
+ ~Mathlib.Algebra.BigOperators.Finprod                               instructions           -6.4%
+ ~Mathlib.Algebra.BigOperators.Finsupp                               instructions          -16.5%
+ ~Mathlib.Algebra.BigOperators.Order                                 instructions           -8.4%
+ ~Mathlib.Algebra.BigOperators.Pi                                    instructions          -10.5%
+ ~Mathlib.Algebra.Category.GroupCat.Basic                            instructions          -23.5%
+ ~Mathlib.Algebra.Category.GroupCat.Preadditive                      instructions           -6.5%
+ ~Mathlib.Algebra.Category.GroupCat.ZModuleEquivalence               instructions           -5.0%
+ ~Mathlib.Algebra.Category.ModuleCat.Basic                           instructions          -20.8%
+ ~Mathlib.Algebra.Category.ModuleCat.EpiMono                         instructions          -62.1%
+ ~Mathlib.Algebra.Category.ModuleCat.Products                        instructions          -52.1%
+ ~Mathlib.Algebra.Category.ModuleCat.Tannaka                         instructions          -12.7%
+ ~Mathlib.Algebra.Category.MonCat.Basic                              instructions          -12.6%
+ ~Mathlib.Algebra.CharP.Algebra                                      instructions          -26.1%
+ ~Mathlib.Algebra.CharP.Quotient                                     instructions          -20.3%
+ ~Mathlib.Algebra.CharZero.Lemmas                                    instructions           -5.3%
+ ~Mathlib.Algebra.CharZero.Quotient                                  instructions          -26.2%
+ ~Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv                instructions          -15.5%
+ ~Mathlib.Algebra.CubicDiscriminant                                  instructions          -61.9%
+ ~Mathlib.Algebra.DirectSum.Basic                                    instructions          -19.6%
+ ~Mathlib.Algebra.DirectSum.Finsupp                                  instructions          -26.5%
+ ~Mathlib.Algebra.DirectSum.Module                                   instructions          -38.2%
+ ~Mathlib.Algebra.DualNumber                                         instructions          -22.7%
+ ~Mathlib.Algebra.EuclideanDomain.Basic                              instructions           -6.6%
+ ~Mathlib.Algebra.Field.Power                                        instructions           -5.4%
+ ~Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra                       instructions          -27.5%
+ ~Mathlib.Algebra.GCDMonoid.Basic                                    instructions           -5.0%
+ ~Mathlib.Algebra.GCDMonoid.Div                                      instructions          -61.1%
+ ~Mathlib.Algebra.GeomSum                                            instructions          -46.4%
+ ~Mathlib.Algebra.Group.Conj                                         instructions          -15.3%
+ ~Mathlib.Algebra.Group.Opposite                                     instructions          -15.9%
+ ~Mathlib.Algebra.Group.Prod                                         instructions           -7.2%
+ ~Mathlib.Algebra.Group.TypeTags                                     instructions           -5.3%
+ ~Mathlib.Algebra.Group.WithOne.Basic                                instructions           -9.0%
+ ~Mathlib.Algebra.Group.WithOne.Units                                instructions           -7.7%
+ ~Mathlib.Algebra.GroupPower.Identities                              instructions           -8.5%
+ ~Mathlib.Algebra.GroupRingAction.Invariant                          instructions          -49.1%
+ ~Mathlib.Algebra.Hom.Centroid                                       instructions          -20.7%
+ ~Mathlib.Algebra.Hom.Equiv.Basic                                    instructions           -6.6%
+ ~Mathlib.Algebra.Hom.Equiv.Units.Basic                              instructions           -7.2%
+ ~Mathlib.Algebra.Hom.GroupInstances                                 instructions          -20.9%
+ ~Mathlib.Algebra.Hom.NonUnitalAlg                                   instructions           -8.2%
+ ~Mathlib.Algebra.Hom.Units                                          instructions           -5.0%
+ ~Mathlib.Algebra.Homology.Additive                                  instructions          -32.7%
+ ~Mathlib.Algebra.Homology.Flip                                      instructions          -75.6%
+ ~Mathlib.Algebra.Homology.Homology                                  instructions          -30.9%
+ ~Mathlib.Algebra.Homology.Homotopy                                  instructions          -34.7%
+ ~Mathlib.Algebra.Homology.HomotopyCategory                          instructions          -57.2%
+ ~Mathlib.Algebra.Homology.Single                                    instructions          -21.4%
+ ~Mathlib.Algebra.Lie.Basic                                          instructions          -26.2%
+ ~Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra                       instructions           -6.7%
+ ~Mathlib.Algebra.Lie.Subalgebra                                     instructions          -32.7%
+ ~Mathlib.Algebra.LinearRecurrence                                   instructions          -25.1%
+ ~Mathlib.Algebra.Module.Algebra                                     instructions          -15.1%
+ ~Mathlib.Algebra.Module.Equiv                                       instructions           -9.3%
+ ~Mathlib.Algebra.Module.LinearMap                                   instructions           -9.6%
+ ~Mathlib.Algebra.Module.Pi                                          instructions          -12.0%
+ ~Mathlib.Algebra.Module.Projective                                  instructions          -35.5%
+ ~Mathlib.Algebra.Module.Submodule.Pointwise                         instructions           -6.6%
+ ~Mathlib.Algebra.Module.ULift                                       instructions          -17.4%
+ ~Mathlib.Algebra.MonoidAlgebra.Basic                                instructions          -40.1%
+ ~Mathlib.Algebra.MonoidAlgebra.Division                             instructions          -48.8%
+ ~Mathlib.Algebra.MonoidAlgebra.Ideal                                instructions          -49.6%
+ ~Mathlib.Algebra.MonoidAlgebra.Support                              instructions          -23.9%
+ ~Mathlib.Algebra.Order.AbsoluteValue                                instructions          -18.4%
+ ~Mathlib.Algebra.Order.Algebra                                      instructions           -9.3%
+ ~Mathlib.Algebra.Order.Archimedean                                  instructions          -16.7%
+ ~Mathlib.Algebra.Order.Chebyshev                                    instructions          -20.8%
+ ~Mathlib.Algebra.Order.EuclideanAbsoluteValue                       instructions           -5.0%
+ ~Mathlib.Algebra.Order.Field.Basic                                  instructions           -8.0%
+ ~Mathlib.Algebra.Order.Field.Power                                  instructions           -9.0%
+ ~Mathlib.Algebra.Order.Floor                                        instructions          -12.9%
+ ~Mathlib.Algebra.Order.Group.Defs                                   instructions          -16.1%
+ ~Mathlib.Algebra.Order.Group.OrderIso                               instructions           -7.9%
+ ~Mathlib.Algebra.Order.Hom.Monoid                                   instructions           -6.8%
+ ~Mathlib.Algebra.Order.Hom.Ring                                     instructions           -7.1%
+ ~Mathlib.Algebra.Order.Kleene                                       instructions           -5.4%
+ ~Mathlib.Algebra.Order.LatticeGroup                                 instructions           -7.4%
+ ~Mathlib.Algebra.Order.Module                                       instructions          -18.3%
+ ~Mathlib.Algebra.Order.Monoid.ToMulBot                              instructions           -7.6%
+ ~Mathlib.Algebra.Order.Nonneg.Field                                 instructions          -24.6%
+ ~Mathlib.Algebra.Order.Nonneg.Ring                                  instructions           -7.9%
+ ~Mathlib.Algebra.Order.Positive.Field                               instructions           -6.5%
+ ~Mathlib.Algebra.Order.Rearrangement                                instructions          -14.2%
+ ~Mathlib.Algebra.Order.Ring.Abs                                     instructions          -10.0%
+ ~Mathlib.Algebra.Order.Ring.Cone                                    instructions           -6.3%
+ ~Mathlib.Algebra.Order.Ring.Defs                                    instructions          -14.8%
+ ~Mathlib.Algebra.Order.Ring.WithTop                                 instructions          -11.8%
+ ~Mathlib.Algebra.Order.SMul                                         instructions           -9.3%
+ ~Mathlib.Algebra.Order.WithZero                                     instructions          -17.7%
+ ~Mathlib.Algebra.Periodic                                           instructions           -6.1%
+ ~Mathlib.Algebra.Polynomial.BigOperators                            instructions          -15.5%
+ ~Mathlib.Algebra.Polynomial.GroupRingAction                         instructions          -27.9%
+ ~Mathlib.Algebra.QuadraticDiscriminant                              instructions          -39.8%
+ ~Mathlib.Algebra.Quandle                                            instructions          -35.5%
+ ~Mathlib.Algebra.Ring.AddAut                                        instructions          -11.5%
+ ~Mathlib.Algebra.Ring.Aut                                           instructions          -13.5%
+ ~Mathlib.Algebra.Ring.CompTypeclasses                               instructions          -10.7%
+ ~Mathlib.Algebra.Ring.Equiv                                         instructions          -10.5%
+ ~Mathlib.Algebra.Ring.Opposite                                      instructions          -16.1%
+ ~Mathlib.Algebra.Ring.Prod                                          instructions          -11.6%
+ ~Mathlib.Algebra.RingQuot                                           instructions          -13.1%
+ ~Mathlib.Algebra.Star.Basic                                         instructions           -7.9%
+ ~Mathlib.Algebra.Star.CHSH                                          instructions          -56.4%
+ ~Mathlib.Algebra.Star.Free                                          instructions           -5.7%
+ ~Mathlib.Algebra.Star.Module                                        instructions          -34.7%
+ ~Mathlib.Algebra.Star.SelfAdjoint                                   instructions          -20.8%
+ ~Mathlib.Algebra.Star.StarAlgHom                                    instructions           -9.4%
+ ~Mathlib.Algebra.Star.Subalgebra                                    instructions           -9.1%
+ ~Mathlib.Algebra.TrivSqZeroExt                                      instructions          -29.2%
+ ~Mathlib.Algebra.Tropical.Lattice                                   instructions           -7.1%
+ ~Mathlib.AlgebraicTopology.AlternatingFaceMapComplex                instructions          -29.7%
+ ~Mathlib.AlgebraicTopology.CechNerve                                instructions          -12.4%
+ ~Mathlib.AlgebraicTopology.DoldKan.Compatibility                    instructions          -44.8%
+ ~Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive              instructions          -88.5%
+ ~Mathlib.AlgebraicTopology.DoldKan.FunctorN                         instructions          -70.7%
+ ~Mathlib.AlgebraicTopology.DoldKan.GammaCompN                       instructions          -86.3%
+ ~Mathlib.AlgebraicTopology.DoldKan.Homotopies                       instructions          -11.8%
+ ~Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence              instructions          -25.4%
+ ~Mathlib.AlgebraicTopology.DoldKan.NCompGamma                       instructions          -63.1%
+ ~Mathlib.AlgebraicTopology.DoldKan.NReflectsIso                     instructions          -55.5%
+ ~Mathlib.AlgebraicTopology.DoldKan.Normalized                       instructions          -68.8%
+ ~Mathlib.AlgebraicTopology.DoldKan.PInfty                           instructions          -58.8%
+ ~Mathlib.AlgebraicTopology.DoldKan.Projections                      instructions          -28.2%
+ ~Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject            instructions          -21.1%
+ ~Mathlib.AlgebraicTopology.ExtraDegeneracy                          instructions          -12.5%
+ ~Mathlib.AlgebraicTopology.MooreComplex                             instructions          -16.9%
+ ~Mathlib.AlgebraicTopology.Nerve                                    instructions          -14.9%
+ ~Mathlib.AlgebraicTopology.SimplicialObject                         instructions          -32.1%
+ ~Mathlib.AlgebraicTopology.SimplicialSet                            instructions          -14.7%
+ ~Mathlib.AlgebraicTopology.TopologicalSimplex                       instructions          -13.4%
+ ~Mathlib.Analysis.Asymptotics.AsymptoticEquivalent                  instructions          -21.7%
+ ~Mathlib.Analysis.Asymptotics.SpecificAsymptotics                   instructions          -15.8%
+ ~Mathlib.Analysis.Asymptotics.SuperpolynomialDecay                  instructions          -13.5%
+ ~Mathlib.Analysis.BoxIntegral.Box.Basic                             instructions           -8.1%
+ ~Mathlib.Analysis.BoxIntegral.Box.SubboxInduction                   instructions           -5.6%
+ ~Mathlib.Analysis.Convex.Basic                                      instructions           -5.7%
+ ~Mathlib.Analysis.Convex.Caratheodory                               instructions          -10.0%
+ ~Mathlib.Analysis.Convex.Combination                                instructions          -42.4%
+ ~Mathlib.Analysis.Convex.Complex                                    instructions          -35.6%
+ ~Mathlib.Analysis.Convex.Exposed                                    instructions          -65.5%
+ ~Mathlib.Analysis.Convex.Extrema                                    instructions          -15.4%
+ ~Mathlib.Analysis.Convex.Function                                   instructions          -11.2%
+ ~Mathlib.Analysis.Convex.Independent                                instructions          -12.9%
+ ~Mathlib.Analysis.Convex.Jensen                                     instructions          -18.1%
+ ~Mathlib.Analysis.Convex.Normed                                     instructions          -16.3%
+ ~Mathlib.Analysis.Convex.Quasiconvex                                instructions          -16.3%
+ ~Mathlib.Analysis.Convex.Segment                                    instructions           -9.4%
+ ~Mathlib.Analysis.Convex.Slope                                      instructions          -40.6%
+ ~Mathlib.Analysis.Convex.Strict                                     instructions           -5.9%
+ ~Mathlib.Analysis.Convex.Topology                                   instructions          -10.3%
+ ~Mathlib.Analysis.Hofer                                             instructions           -7.9%
+ ~Mathlib.Analysis.LocallyConvex.Bounded                             instructions          -44.9%
+ ~Mathlib.Analysis.LocallyConvex.Polar                               instructions          -71.8%
+ ~Mathlib.Analysis.Normed.Field.Basic                                instructions          -14.6%
+ ~Mathlib.Analysis.Normed.Field.InfiniteSum                          instructions          -17.4%
+ ~Mathlib.Analysis.Normed.Group.AddTorsor                            instructions          -19.2%
+ ~Mathlib.Analysis.Normed.Group.Basic                                instructions           -7.9%
+ ~Mathlib.Analysis.Normed.Group.Hom                                  instructions          -13.0%
+ ~Mathlib.Analysis.Normed.Group.HomCompletion                        instructions          -49.8%
+ ~Mathlib.Analysis.Normed.Group.InfiniteSum                          instructions           -6.0%
+ ~Mathlib.Analysis.Normed.Order.Lattice                              instructions           -5.7%
+ ~Mathlib.Analysis.Normed.Order.UpperLower                           instructions           -6.2%
+ ~Mathlib.Analysis.Normed.Ring.Seminorm                              instructions          -37.5%
+ ~Mathlib.Analysis.NormedSpace.AddTorsor                             instructions          -55.6%
+ ~Mathlib.Analysis.NormedSpace.Basic                                 instructions          -34.1%
+ ~Mathlib.Analysis.NormedSpace.ConformalLinearMap                    instructions          -68.0%
+ ~Mathlib.Analysis.NormedSpace.ContinuousLinearMap                   instructions          -80.3%
+ ~Mathlib.Analysis.NormedSpace.LinearIsometry                        instructions          -21.3%
+ ~Mathlib.Analysis.NormedSpace.Ray                                   instructions          -11.8%
+ ~Mathlib.Analysis.NormedSpace.RieszLemma                            instructions          -12.9%
+ ~Mathlib.Analysis.NormedSpace.Star.Basic                            instructions          -65.1%
+ ~Mathlib.Analysis.Seminorm                                          instructions          -30.9%
+ ~Mathlib.Analysis.SpecialFunctions.Polynomials                      instructions          -18.4%
+ ~Mathlib.Analysis.SpecificLimits.Basic                              instructions          -20.2%
+ ~Mathlib.CategoryTheory.Abelian.Basic                               instructions          -10.7%
+ ~Mathlib.CategoryTheory.Abelian.Exact                               instructions           -6.4%
+ ~Mathlib.CategoryTheory.Abelian.FunctorCategory                     instructions          -11.6%
+ ~Mathlib.CategoryTheory.Abelian.Opposite                            instructions          -16.4%
+ ~Mathlib.CategoryTheory.Abelian.Subobject                           instructions           -8.0%
+ ~Mathlib.CategoryTheory.Action                                      instructions          -17.6%
+ ~Mathlib.CategoryTheory.Adjunction.Basic                            instructions           -5.2%
+ ~Mathlib.CategoryTheory.Adjunction.FullyFaithful                    instructions          -15.1%
+ ~Mathlib.CategoryTheory.Adjunction.Limits                           instructions          -31.1%
+ ~Mathlib.CategoryTheory.Adjunction.Opposites                        instructions           -6.7%
+ ~Mathlib.CategoryTheory.Adjunction.Over                             instructions          -15.1%
+ ~Mathlib.CategoryTheory.Adjunction.Whiskering                       instructions          -63.1%
+ ~Mathlib.CategoryTheory.Arrow                                       instructions           -7.9%
+ ~Mathlib.CategoryTheory.Category.Bipointed                          instructions          -14.4%
+ ~Mathlib.CategoryTheory.Category.Cat                                instructions          -51.9%
+ ~Mathlib.CategoryTheory.Category.QuivCat                            instructions           -7.3%
+ ~Mathlib.CategoryTheory.Category.TwoP                               instructions          -29.9%
+ ~Mathlib.CategoryTheory.Conj                                        instructions           -6.9%
+ ~Mathlib.CategoryTheory.Elements                                    instructions          -50.8%
+ ~Mathlib.CategoryTheory.Equivalence                                 instructions           -6.7%
+ ~Mathlib.CategoryTheory.EssentialImage                              instructions           -7.7%
+ ~Mathlib.CategoryTheory.FinCategory                                 instructions          -28.2%
+ ~Mathlib.CategoryTheory.FintypeCat                                  instructions           -9.6%
+ ~Mathlib.CategoryTheory.Functor.Currying                            instructions          -15.0%
+ ~Mathlib.CategoryTheory.Functor.InvIsos                             instructions           -7.5%
+ ~Mathlib.CategoryTheory.Functor.LeftDerived                         instructions          -76.9%
+ ~Mathlib.CategoryTheory.GradedObject                                instructions          -37.9%
+ ~Mathlib.CategoryTheory.Grothendieck                                instructions          -34.4%
+ ~Mathlib.CategoryTheory.Idempotents.FunctorCategories               instructions          -11.7%
+ ~Mathlib.CategoryTheory.Idempotents.FunctorExtension                instructions          -71.6%
+ ~Mathlib.CategoryTheory.Idempotents.HomologicalComplex              instructions          -50.5%
+ ~Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi                  instructions          -25.1%
+ ~Mathlib.CategoryTheory.Limits.ColimitLimit                         instructions          -42.2%
+ ~Mathlib.CategoryTheory.Limits.Comma                                instructions          -35.4%
+ ~Mathlib.CategoryTheory.Limits.Cones                                instructions          -17.9%
+ ~Mathlib.CategoryTheory.Limits.Constructions.Over.Connected         instructions           -7.5%
+ ~Mathlib.CategoryTheory.Limits.Creates                              instructions           -6.1%
+ ~Mathlib.CategoryTheory.Limits.ExactFunctor                         instructions          -12.3%
+ ~Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit   instructions          -12.4%
+ ~Mathlib.CategoryTheory.Limits.FunctorCategory                      instructions          -19.9%
+ ~Mathlib.CategoryTheory.Limits.HasLimits                            instructions          -15.2%
+ ~Mathlib.CategoryTheory.Limits.KanExtension                         instructions          -35.4%
+ ~Mathlib.CategoryTheory.Limits.Opposites                            instructions           -8.9%
+ ~Mathlib.CategoryTheory.Limits.Preserves.Basic                      instructions          -29.0%
+ ~Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory            instructions          -59.0%
+ ~Mathlib.CategoryTheory.Limits.Preserves.Limits                     instructions           -7.6%
+ ~Mathlib.CategoryTheory.Limits.Preserves.Opposites                  instructions          -35.9%
+ ~Mathlib.CategoryTheory.Limits.Presheaf                             instructions          -77.0%
+ ~Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer                instructions           -6.2%
+ ~Mathlib.CategoryTheory.Limits.Shapes.Products                      instructions           -7.1%
+ ~Mathlib.CategoryTheory.Limits.Shapes.Types                         instructions           -6.3%
+ ~Mathlib.CategoryTheory.Linear.Basic                                instructions          -75.3%
+ ~Mathlib.CategoryTheory.Linear.Yoneda                               instructions          -80.8%
+ ~Mathlib.CategoryTheory.Localization.Construction                   instructions          -49.0%
+ ~Mathlib.CategoryTheory.Localization.Opposite                       instructions          -32.7%
+ ~Mathlib.CategoryTheory.Localization.Predicate                      instructions          -24.8%
+ ~Mathlib.CategoryTheory.Monad.Adjunction                            instructions          -30.8%
+ ~Mathlib.CategoryTheory.Monad.Limits                                instructions           -9.6%
+ ~Mathlib.CategoryTheory.Monad.Products                              instructions           -6.7%
+ ~Mathlib.CategoryTheory.Monoidal.Functor                            instructions           -7.9%
+ ~Mathlib.CategoryTheory.Monoidal.Linear                             instructions           -5.6%
+ ~Mathlib.CategoryTheory.Monoidal.NaturalTransformation              instructions           -8.4%
+ ~Mathlib.CategoryTheory.Monoidal.Transport                          instructions          -12.7%
+ ~Mathlib.CategoryTheory.Opposites                                   instructions          -12.1%
+ ~Mathlib.CategoryTheory.Over                                        instructions           -6.9%
+ ~Mathlib.CategoryTheory.PEmpty                                      instructions           -5.9%
+ ~Mathlib.CategoryTheory.Preadditive.AdditiveFunctor                 instructions           -8.9%
+ ~Mathlib.CategoryTheory.Preadditive.EilenbergMoore                  instructions           -6.7%
+ ~Mathlib.CategoryTheory.Preadditive.Yoneda.Basic                    instructions          -61.2%
+ ~Mathlib.CategoryTheory.Products.Basic                              instructions           -8.2%
+ ~Mathlib.CategoryTheory.Shift.Basic                                 instructions           -6.3%
+ ~Mathlib.CategoryTheory.Sigma.Basic                                 instructions          -16.4%
+ ~Mathlib.CategoryTheory.SingleObj                                   instructions          -23.6%
+ ~Mathlib.CategoryTheory.Sites.Adjunction                            instructions          -92.7%
+ ~Mathlib.CategoryTheory.Sites.LeftExact                             instructions          -71.3%
+ ~Mathlib.CategoryTheory.Sites.Limits                                instructions           -9.1%
+ ~Mathlib.CategoryTheory.Sites.Plus                                  instructions          -40.0%
+ ~Mathlib.CategoryTheory.Sites.Sheaf                                 instructions           -7.8%
+ ~Mathlib.CategoryTheory.Sites.Sheafification                        instructions          -70.0%
+ ~Mathlib.CategoryTheory.Skeletal                                    instructions           -6.5%
+ ~Mathlib.CategoryTheory.StructuredArrow                             instructions           -7.5%
+ ~Mathlib.CategoryTheory.Subobject.Basic                             instructions          -34.4%
+ ~Mathlib.CategoryTheory.Subobject.Lattice                           instructions          -25.3%
+ ~Mathlib.CategoryTheory.Subobject.MonoOver                          instructions          -12.5%
+ ~Mathlib.CategoryTheory.Whiskering                                  instructions          -20.4%
+ ~Mathlib.CategoryTheory.Yoneda                                      instructions          -31.6%
+ ~Mathlib.Combinatorics.Additive.Energy                              instructions           -7.9%
+ ~Mathlib.Combinatorics.Additive.PluenneckeRuzsa                     instructions          -13.4%
+ ~Mathlib.Combinatorics.Catalan                                      instructions          -55.4%
+ ~Mathlib.Combinatorics.Composition                                  instructions           -8.1%
+ ~Mathlib.Combinatorics.SetFamily.Compression.UV                     instructions           -8.0%
+ ~Mathlib.Combinatorics.SetFamily.Kleitman                           instructions          -17.6%
+ ~Mathlib.Combinatorics.SetFamily.LYM                                instructions           -9.2%
+ ~Mathlib.Combinatorics.SimpleGraph.Density                          instructions          -14.4%
+ ~Mathlib.Combinatorics.SimpleGraph.Matching                         instructions          -15.5%
+ ~Mathlib.Combinatorics.SimpleGraph.Prod                             instructions           -6.7%
+ ~Mathlib.Combinatorics.SimpleGraph.Regularity.Energy                instructions           -6.7%
+ ~Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform               instructions           -6.9%
+ ~Mathlib.Control.LawfulFix                                          instructions          -30.0%
+ ~Mathlib.Data.Complex.Basic                                         instructions          -54.0%
+ ~Mathlib.Data.Complex.Determinant                                   instructions          -63.7%
+ ~Mathlib.Data.Complex.Exponential                                   instructions          -32.8%
+ ~Mathlib.Data.Complex.Module                                        instructions          -38.1%
+ ~Mathlib.Data.Dfinsupp.Basic                                        instructions          -18.1%
+ ~Mathlib.Data.Dfinsupp.Interval                                     instructions           -5.5%
+ ~Mathlib.Data.Dfinsupp.NeLocus                                      instructions          -13.3%
- ~Mathlib.Data.Fin.Basic                                             instructions           12.0%
+ ~Mathlib.Data.Fin.Tuple.BubbleSortInduction                         instructions          -18.1%
+ ~Mathlib.Data.Fin.Tuple.Sort                                        instructions           -7.0%
+ ~Mathlib.Data.Finset.Pi                                             instructions          -20.2%
+ ~Mathlib.Data.Finset.Sym                                            instructions           -8.0%
+ ~Mathlib.Data.Finsupp.Antidiagonal                                  instructions          -45.2%
+ ~Mathlib.Data.Finsupp.Basic                                         instructions          -16.7%
+ ~Mathlib.Data.Finsupp.Multiset                                      instructions          -68.5%
+ ~Mathlib.Data.Finsupp.NeLocus                                       instructions          -15.6%
+ ~Mathlib.Data.Finsupp.Pointwise                                     instructions           -5.4%
+ ~Mathlib.Data.Finsupp.ToDfinsupp                                    instructions          -17.8%
+ ~Mathlib.Data.Fintype.Basic                                         instructions           -9.2%
+ ~Mathlib.Data.Fintype.Powerset                                      instructions          -22.5%
+ ~Mathlib.Data.Int.AbsoluteValue                                     instructions          -44.8%
+ ~Mathlib.Data.Int.Associated                                        instructions           -6.1%
+ ~Mathlib.Data.Int.Cast.Lemmas                                       instructions           -7.9%
+ ~Mathlib.Data.Int.Cast.Prod                                         instructions           -7.1%
- ~Mathlib.Data.Int.ConditionallyCompleteOrder                        instructions           15.0%
+ ~Mathlib.Data.Int.Log                                               instructions          -40.0%
+ ~Mathlib.Data.List.Cycle                                            instructions          -17.1%
+ ~Mathlib.Data.List.Join                                             instructions           -5.1%
+ ~Mathlib.Data.Matrix.Basic                                          instructions          -18.8%
+ ~Mathlib.Data.Matrix.Block                                          instructions           -5.4%
+ ~Mathlib.Data.Matrix.DualNumber                                     instructions          -23.0%
+ ~Mathlib.Data.Matrix.Rank                                           instructions          -81.1%
+ ~Mathlib.Data.Multiset.Basic                                        instructions           -5.2%
+ ~Mathlib.Data.Multiset.Pi                                           instructions           -5.5%
+ ~Mathlib.Data.MvPolynomial.Basic                                    instructions          -19.6%
+ ~Mathlib.Data.MvPolynomial.CommRing                                 instructions          -51.4%
+ ~Mathlib.Data.MvPolynomial.Equiv                                    instructions          -56.5%
+ ~Mathlib.Data.MvPolynomial.Expand                                   instructions          -34.8%
+ ~Mathlib.Data.MvPolynomial.Funext                                   instructions          -61.8%
+ ~Mathlib.Data.MvPolynomial.Monad                                    instructions          -30.2%
+ ~Mathlib.Data.MvPolynomial.Polynomial                               instructions           -7.7%
+ ~Mathlib.Data.MvPolynomial.Rename                                   instructions          -29.2%
+ ~Mathlib.Data.MvPolynomial.Supported                                instructions          -51.3%
+ ~Mathlib.Data.MvPolynomial.Variables                                instructions          -11.1%
+ ~Mathlib.Data.Nat.Cast.Field                                        instructions           -6.1%
+ ~Mathlib.Data.Nat.Choose.Bounds                                     instructions           -6.4%
+ ~Mathlib.Data.Nat.Factorization.Basic                               instructions          -21.4%
+ ~Mathlib.Data.Nat.Order.Basic                                       instructions          -11.6%
+ ~Mathlib.Data.Nat.PSub                                              instructions           -7.6%
+ ~Mathlib.Data.Nat.Parity                                            instructions           -5.1%
+ ~Mathlib.Data.Nat.Prime                                             instructions           -6.6%
+ ~Mathlib.Data.Nat.Totient                                           instructions          -10.7%
+ ~Mathlib.Data.PFunctor.Multivariate.M                               instructions           -5.7%
+ ~Mathlib.Data.PNat.Interval                                         instructions           -8.0%
+ ~Mathlib.Data.PNat.Xgcd                                             instructions           -5.3%
+ ~Mathlib.Data.Pi.Interval                                           instructions          -10.3%
+ ~Mathlib.Data.Polynomial.Basic                                      instructions          -12.3%
+ ~Mathlib.Data.Polynomial.Coeff                                      instructions           -5.7%
+ ~Mathlib.Data.Polynomial.Degree.CardPowDegree                       instructions          -52.2%
+ ~Mathlib.Data.Polynomial.Degree.Definitions                         instructions           -7.8%
+ ~Mathlib.Data.Polynomial.Degree.Lemmas                              instructions           -5.7%
+ ~Mathlib.Data.Polynomial.DenomsClearable                            instructions          -51.5%
+ ~Mathlib.Data.Polynomial.Derivative                                 instructions          -27.8%
+ ~Mathlib.Data.Polynomial.Div                                        instructions          -16.9%
+ ~Mathlib.Data.Polynomial.EraseLead                                  instructions           -6.8%
+ ~Mathlib.Data.Polynomial.Eval                                       instructions          -20.8%
+ ~Mathlib.Data.Polynomial.FieldDivision                              instructions          -78.6%
+ ~Mathlib.Data.Polynomial.HasseDeriv                                 instructions          -40.1%
+ ~Mathlib.Data.Polynomial.Identities                                 instructions           -5.0%
+ ~Mathlib.Data.Polynomial.Inductions                                 instructions           -5.2%
+ ~Mathlib.Data.Polynomial.IntegralNormalization                      instructions           -8.4%
+ ~Mathlib.Data.Polynomial.Lifts                                      instructions          -39.7%
+ ~Mathlib.Data.Polynomial.Module                                     instructions          -58.0%
+ ~Mathlib.Data.Polynomial.Monic                                      instructions           -6.7%
+ ~Mathlib.Data.Polynomial.Monomial                                   instructions          -58.4%
+ ~Mathlib.Data.Polynomial.PartialFractions                           instructions          -70.4%
+ ~Mathlib.Data.Polynomial.Reverse                                    instructions           -6.1%
+ ~Mathlib.Data.Polynomial.RingDivision                               instructions          -22.4%
+ ~Mathlib.Data.Polynomial.Splits                                     instructions          -83.6%
+ ~Mathlib.Data.Polynomial.Taylor                                     instructions          -14.1%
+ ~Mathlib.Data.Rat.BigOperators                                      instructions           -5.8%
+ ~Mathlib.Data.Rat.Cast                                              instructions          -18.7%
+ ~Mathlib.Data.Rat.Floor                                             instructions          -23.3%
+ ~Mathlib.Data.Rat.Lemmas                                            instructions           -6.9%
+ ~Mathlib.Data.Rat.NNRat                                             instructions          -25.2%
+ ~Mathlib.Data.Rat.Order                                             instructions           -9.0%
+ ~Mathlib.Data.Real.Basic                                            instructions          -65.9%
+ ~Mathlib.Data.Real.Cardinality                                      instructions           -7.8%
+ ~Mathlib.Data.Real.CauSeq                                           instructions          -45.1%
+ ~Mathlib.Data.Real.CauSeqCompletion                                 instructions          -39.7%
+ ~Mathlib.Data.Real.ConjugateExponents                               instructions           -6.2%
+ ~Mathlib.Data.Real.ENNReal                                          instructions          -38.6%
+ ~Mathlib.Data.Real.ENatENNReal                                      instructions          -49.4%
+ ~Mathlib.Data.Real.EReal                                            instructions           -9.8%
+ ~Mathlib.Data.Real.Hyperreal                                        instructions          -10.5%
+ ~Mathlib.Data.Real.NNReal                                           instructions          -30.3%
+ ~Mathlib.Data.Real.Pointwise                                        instructions          -12.5%
+ ~Mathlib.Data.Real.Sqrt                                             instructions          -11.6%
+ ~Mathlib.Data.Set.Intervals.Disjoint                                instructions           -6.1%
+ ~Mathlib.Data.Set.Intervals.IsoIoo                                  instructions          -17.1%
+ ~Mathlib.Data.Set.Intervals.SurjOn                                  instructions           -8.2%
- ~Mathlib.Data.Set.Semiring                                          instructions            7.5%
+ ~Mathlib.Data.Vector.Basic                                          instructions          -21.6%
+ ~Mathlib.Data.ZMod.Basic                                            instructions           -7.9%
- ~Mathlib.Data.ZMod.Coprime                                          instructions            7.3%
+ ~Mathlib.Data.ZMod.Defs                                             instructions           -8.3%
+ ~Mathlib.Deprecated.Subfield                                        instructions          -10.5%
+ ~Mathlib.Deprecated.Subgroup                                        instructions           -8.5%
+ ~Mathlib.Deprecated.Subring                                         instructions           -9.7%
+ ~Mathlib.FieldTheory.MvPolynomial                                   instructions          -51.3%
+ ~Mathlib.FieldTheory.PerfectClosure                                 instructions          -12.4%
+ ~Mathlib.FieldTheory.Subfield                                       instructions          -21.5%
+ ~Mathlib.FieldTheory.Tower                                          instructions          -82.2%
+ ~Mathlib.GroupTheory.Abelianization                                 instructions          -18.0%
+ ~Mathlib.GroupTheory.Commensurable                                  instructions           -5.6%
+ ~Mathlib.GroupTheory.Commutator                                     instructions           -8.9%
+ ~Mathlib.GroupTheory.CommutingProbability                           instructions          -14.8%
- ~Mathlib.GroupTheory.Divisible                                      instructions            6.5%
+ ~Mathlib.GroupTheory.Finiteness                                     instructions           -9.3%
+ ~Mathlib.GroupTheory.FreeAbelianGroup                               instructions          -15.2%
+ ~Mathlib.GroupTheory.FreeAbelianGroupFinsupp                        instructions          -11.4%
+ ~Mathlib.GroupTheory.FreeGroup                                      instructions           -7.7%
+ ~Mathlib.GroupTheory.FreeProduct                                    instructions          -33.9%
+ ~Mathlib.GroupTheory.GroupAction.ConjAct                            instructions          -28.3%
+ ~Mathlib.GroupTheory.GroupAction.FixingSubgroup                     instructions          -10.1%
+ ~Mathlib.GroupTheory.Index                                          instructions           -6.9%
+ ~Mathlib.GroupTheory.IsFreeGroup                                    instructions           -7.0%
+ ~Mathlib.GroupTheory.MonoidLocalization                             instructions           -7.2%
+ ~Mathlib.GroupTheory.Perm.Basic                                     instructions           -8.3%
+ ~Mathlib.GroupTheory.Perm.Cycle.Basic                               instructions          -13.9%
+ ~Mathlib.GroupTheory.Perm.Cycle.Type                                instructions          -24.5%
+ ~Mathlib.GroupTheory.Perm.Fin                                       instructions           -9.0%
+ ~Mathlib.GroupTheory.Perm.Sign                                      instructions           -8.0%
+ ~Mathlib.GroupTheory.Perm.Subgroup                                  instructions           -8.7%
+ ~Mathlib.GroupTheory.QuotientGroup                                  instructions          -13.1%
+ ~Mathlib.GroupTheory.SemidirectProduct                              instructions           -7.2%
+ ~Mathlib.GroupTheory.SpecificGroups.Alternating                     instructions          -63.7%
+ ~Mathlib.GroupTheory.Subgroup.Basic                                 instructions          -13.1%
+ ~Mathlib.GroupTheory.Subgroup.Finite                                instructions          -11.5%
+ ~Mathlib.GroupTheory.Subgroup.Pointwise                             instructions          -11.9%
+ ~Mathlib.GroupTheory.Submonoid.Inverses                             instructions          -14.2%
+ ~Mathlib.GroupTheory.Submonoid.Pointwise                            instructions          -19.9%
+ ~Mathlib.LinearAlgebra.AffineSpace.AffineEquiv                      instructions          -18.3%
+ ~Mathlib.LinearAlgebra.AffineSpace.AffineMap                        instructions          -45.5%
+ ~Mathlib.LinearAlgebra.AffineSpace.AffineSubspace                   instructions          -13.1%
+ ~Mathlib.LinearAlgebra.AffineSpace.Basis                            instructions          -32.5%
+ ~Mathlib.LinearAlgebra.AffineSpace.Combination                      instructions          -60.1%
+ ~Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional                instructions          -55.1%
+ ~Mathlib.LinearAlgebra.AffineSpace.Independent                      instructions          -37.0%
+ ~Mathlib.LinearAlgebra.AffineSpace.Matrix                           instructions          -58.6%
+ ~Mathlib.LinearAlgebra.AffineSpace.MidpointZero                     instructions          -18.4%
+ ~Mathlib.LinearAlgebra.AffineSpace.Ordered                          instructions          -42.3%
+ ~Mathlib.LinearAlgebra.AffineSpace.Restrict                         instructions          -60.1%
+ ~Mathlib.LinearAlgebra.AffineSpace.Slope                            instructions          -22.1%
+ ~Mathlib.LinearAlgebra.Alternating                                  instructions          -41.8%
+ ~Mathlib.LinearAlgebra.Basic                                        instructions          -11.7%
+ ~Mathlib.LinearAlgebra.Basis                                        instructions          -28.9%
+ ~Mathlib.LinearAlgebra.BilinearMap                                  instructions          -22.7%
+ ~Mathlib.LinearAlgebra.Determinant                                  instructions          -58.0%
+ ~Mathlib.LinearAlgebra.Dfinsupp                                     instructions          -19.8%
+ ~Mathlib.LinearAlgebra.Dimension                                    instructions          -62.7%
- ~Mathlib.LinearAlgebra.DirectSum.Finsupp                            instructions           31.1%
+ ~Mathlib.LinearAlgebra.DirectSum.TensorProduct                      instructions          -33.4%
+ ~Mathlib.LinearAlgebra.FiniteDimensional                            instructions          -69.7%
+ ~Mathlib.LinearAlgebra.Finrank                                      instructions          -54.2%
+ ~Mathlib.LinearAlgebra.Finsupp                                      instructions          -37.0%
+ ~Mathlib.LinearAlgebra.FinsuppVectorSpace                           instructions          -13.3%
+ ~Mathlib.LinearAlgebra.FreeAlgebra                                  instructions          -79.2%
+ ~Mathlib.LinearAlgebra.FreeModule.Basic                             instructions          -20.5%
+ ~Mathlib.LinearAlgebra.FreeModule.Determinant                       instructions          -22.7%
+ ~Mathlib.LinearAlgebra.FreeModule.Finite.Basic                      instructions          -20.1%
+ ~Mathlib.LinearAlgebra.FreeModule.Finite.Matrix                     instructions          -75.8%
+ ~Mathlib.LinearAlgebra.FreeModule.Finite.Rank                       instructions          -61.9%
+ ~Mathlib.LinearAlgebra.FreeModule.PID                               instructions          -31.2%
+ ~Mathlib.LinearAlgebra.FreeModule.Rank                              instructions          -51.6%
+ ~Mathlib.LinearAlgebra.InvariantBasisNumber                         instructions          -56.4%
+ ~Mathlib.LinearAlgebra.Isomorphisms                                 instructions          -81.6%
+ ~Mathlib.LinearAlgebra.Lagrange                                     instructions          -68.9%
+ ~Mathlib.LinearAlgebra.LinearIndependent                            instructions          -29.1%
+ ~Mathlib.LinearAlgebra.LinearPMap                                   instructions          -10.3%
- ~Mathlib.LinearAlgebra.Matrix.AbsoluteValue                         instructions            6.7%
+ ~Mathlib.LinearAlgebra.Matrix.Adjugate                              instructions          -73.8%
+ ~Mathlib.LinearAlgebra.Matrix.Block                                 instructions          -12.3%
+ ~Mathlib.LinearAlgebra.Matrix.Circulant                             instructions           -6.6%
+ ~Mathlib.LinearAlgebra.Matrix.Determinant                           instructions           -8.8%
+ ~Mathlib.LinearAlgebra.Matrix.Diagonal                              instructions          -68.3%
+ ~Mathlib.LinearAlgebra.Matrix.FiniteDimensional                     instructions          -84.4%
+ ~Mathlib.LinearAlgebra.Matrix.MvPolynomial                          instructions          -37.1%
+ ~Mathlib.LinearAlgebra.Matrix.Nondegenerate                         instructions          -15.4%
+ ~Mathlib.LinearAlgebra.Matrix.NonsingularInverse                    instructions          -33.7%
+ ~Mathlib.LinearAlgebra.Matrix.Polynomial                            instructions          -43.8%
+ ~Mathlib.LinearAlgebra.Matrix.Reindex                               instructions          -18.1%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin                                 instructions          -43.6%
+ ~Mathlib.LinearAlgebra.Matrix.Transvection                          instructions          -30.4%
+ ~Mathlib.LinearAlgebra.Matrix.ZPow                                  instructions          -35.5%
+ ~Mathlib.LinearAlgebra.Multilinear.Basic                            instructions           -5.9%
+ ~Mathlib.LinearAlgebra.Multilinear.TensorProduct                    instructions           -7.9%
+ ~Mathlib.LinearAlgebra.Pi                                           instructions           -7.3%
+ ~Mathlib.LinearAlgebra.Prod                                         instructions          -19.7%
+ ~Mathlib.LinearAlgebra.Projection                                   instructions          -43.5%
+ ~Mathlib.LinearAlgebra.ProjectiveSpace.Basic                        instructions          -62.5%
+ ~Mathlib.LinearAlgebra.ProjectiveSpace.Independence                 instructions           -8.3%
+ ~Mathlib.LinearAlgebra.Quotient                                     instructions          -14.5%
+ ~Mathlib.LinearAlgebra.QuotientPi                                   instructions          -55.5%
+ ~Mathlib.LinearAlgebra.Ray                                          instructions          -24.7%
+ ~Mathlib.LinearAlgebra.SModEq                                       instructions           -8.3%
+ ~Mathlib.LinearAlgebra.SesquilinearForm                             instructions          -74.0%
+ ~Mathlib.LinearAlgebra.Span                                         instructions          -35.9%
+ ~Mathlib.LinearAlgebra.StdBasis                                     instructions          -34.1%
+ ~Mathlib.LinearAlgebra.SymplecticGroup                              instructions          -46.2%
+ ~Mathlib.LinearAlgebra.TensorProduct                                instructions          -15.4%
+ ~Mathlib.LinearAlgebra.TensorProductBasis                           instructions          -44.6%
+ ~Mathlib.Logic.Denumerable                                          instructions           -8.2%
+ ~Mathlib.Logic.Embedding.Basic                                      instructions           -6.8%
+ ~Mathlib.Logic.Equiv.Basic                                          instructions           -5.2%
+ ~Mathlib.Logic.Equiv.Defs                                           instructions          -11.5%
+ ~Mathlib.Logic.Equiv.Fin                                            instructions           -5.5%
+ ~Mathlib.Logic.Equiv.List                                           instructions           -8.8%
+ ~Mathlib.Logic.Equiv.TransferInstance                               instructions           -7.3%
+ ~Mathlib.Logic.Hydra                                                instructions          -11.6%
- ~Mathlib.MeasureTheory.MeasurableSpace                              instructions            8.1%
+ ~Mathlib.MeasureTheory.Measure.OuterMeasure                         instructions          -51.6%
+ ~Mathlib.ModelTheory.Encoding                                       instructions          -10.0%
+ ~Mathlib.NumberTheory.ADEInequality                                 instructions           -6.3%
+ ~Mathlib.NumberTheory.Basic                                         instructions          -42.2%
+ ~Mathlib.NumberTheory.ClassNumber.AdmissibleAbs                     instructions          -24.4%
+ ~Mathlib.NumberTheory.Fermat4                                       instructions           -7.7%
+ ~Mathlib.NumberTheory.LucasLehmer                                   instructions          -40.7%
+ ~Mathlib.NumberTheory.Padics.PadicNorm                              instructions          -14.2%
+ ~Mathlib.NumberTheory.PellMatiyasevic                               instructions           -5.2%
+ ~Mathlib.NumberTheory.Primorial                                     instructions           -6.8%
+ ~Mathlib.NumberTheory.PythagoreanTriples                            instructions          -36.7%
+ ~Mathlib.NumberTheory.Zsqrtd.Basic                                  instructions          -33.1%
- ~Mathlib.Order.Bounded                                              instructions            5.0%
+ ~Mathlib.Order.Category.DistLatCat                                  instructions          -60.4%
+ ~Mathlib.Order.Category.LatCat                                      instructions          -49.4%
+ ~Mathlib.Order.Category.LinOrdCat                                   instructions          -57.8%
+ ~Mathlib.Order.Category.NonemptyFinLinOrdCat                        instructions          -14.8%
+ ~Mathlib.Order.Category.PartOrdCat                                  instructions          -23.6%
+ ~Mathlib.Order.Category.PreordCat                                   instructions          -20.6%
+ ~Mathlib.Order.CompleteLatticeIntervals                             instructions          -14.1%
+ ~Mathlib.Order.ConditionallyCompleteLattice.Basic                   instructions           -7.7%
+ ~Mathlib.Order.Disjointed                                           instructions          -13.1%
+ ~Mathlib.Order.Filter.Archimedean                                   instructions          -10.9%
+ ~Mathlib.Order.Filter.AtTopBot                                      instructions           -5.4%
+ ~Mathlib.Order.Filter.Basic                                         instructions           -6.9%
+ ~Mathlib.Order.Filter.ENNReal                                       instructions           -6.0%
+ ~Mathlib.Order.Filter.Pi                                            instructions           -5.2%
+ ~Mathlib.Order.Filter.Pointwise                                     instructions          -17.5%
+ ~Mathlib.Order.Filter.Ultrafilter                                   instructions          -38.3%
+ ~Mathlib.Order.Filter.ZeroAndBoundedAtFilter                        instructions          -19.7%
+ ~Mathlib.Order.FixedPoints                                          instructions           -7.1%
+ ~Mathlib.Order.GaloisConnection                                     instructions           -6.1%
+ ~Mathlib.Order.Heyting.Basic                                        instructions           -7.1%
+ ~Mathlib.Order.Heyting.Hom                                          instructions           -7.4%
+ ~Mathlib.Order.Heyting.Regular                                      instructions          -13.4%
+ ~Mathlib.Order.Hom.CompleteLattice                                  instructions           -7.0%
+ ~Mathlib.Order.Hom.Lattice                                          instructions          -10.2%
+ ~Mathlib.Order.JordanHolder                                         instructions          -11.5%
+ ~Mathlib.Order.LatticeIntervals                                     instructions           -5.2%
+ ~Mathlib.Order.ModularLattice                                       instructions           -5.7%
+ ~Mathlib.Order.OmegaCompletePartialOrder                            instructions           -8.8%
+ ~Mathlib.Order.RelIso.Group                                         instructions          -40.2%
+ ~Mathlib.Order.SuccPred.IntervalSucc                                instructions          -11.1%
+ ~Mathlib.RepresentationTheory.Maschke                               instructions          -74.4%
+ ~Mathlib.RingTheory.Adjoin.Basic                                    instructions          -50.0%
+ ~Mathlib.RingTheory.Adjoin.Fg                                       instructions          -42.0%
+ ~Mathlib.RingTheory.Adjoin.Tower                                    instructions          -67.8%
+ ~Mathlib.RingTheory.AlgebraTower                                    instructions           -7.3%
+ ~Mathlib.RingTheory.ChainOfDivisors                                 instructions           -9.9%
+ ~Mathlib.RingTheory.Congruence                                      instructions           -5.2%
+ ~Mathlib.RingTheory.Coprime.Ideal                                   instructions          -20.0%
+ ~Mathlib.RingTheory.EisensteinCriterion                             instructions          -52.8%
+ ~Mathlib.RingTheory.EuclideanDomain                                 instructions          -20.5%
+ ~Mathlib.RingTheory.FiniteType                                      instructions          -78.5%
+ ~Mathlib.RingTheory.Finiteness                                      instructions          -39.2%
+ ~Mathlib.RingTheory.Flat                                            instructions          -23.4%
+ ~Mathlib.RingTheory.FreeRing                                        instructions          -13.0%
+ ~Mathlib.RingTheory.Ideal.AssociatedPrime                           instructions          -60.3%
+ ~Mathlib.RingTheory.Ideal.Basic                                     instructions          -10.8%
+ ~Mathlib.RingTheory.Ideal.IdempotentFg                              instructions          -64.1%
+ ~Mathlib.RingTheory.Ideal.Operations                                instructions          -52.0%
+ ~Mathlib.RingTheory.Ideal.Prod                                      instructions          -60.5%
+ ~Mathlib.RingTheory.Ideal.Quotient                                  instructions          -43.2%
+ ~Mathlib.RingTheory.Ideal.QuotientOperations                        instructions          -25.6%
+ ~Mathlib.RingTheory.Localization.Basic                              instructions          -33.4%
+ ~Mathlib.RingTheory.Localization.FractionRing                       instructions          -55.8%
+ ~Mathlib.RingTheory.Localization.Ideal                              instructions          -15.1%
+ ~Mathlib.RingTheory.Localization.Integer                            instructions          -37.8%
+ ~Mathlib.RingTheory.Localization.InvSubmonoid                       instructions          -24.0%
+ ~Mathlib.RingTheory.Localization.Module                             instructions          -34.6%
+ ~Mathlib.RingTheory.Localization.NumDen                             instructions          -25.1%
+ ~Mathlib.RingTheory.Localization.Submodule                          instructions          -53.5%
+ ~Mathlib.RingTheory.Multiplicity                                    instructions           -6.4%
+ ~Mathlib.RingTheory.MvPolynomial.Basic                              instructions          -56.6%
+ ~Mathlib.RingTheory.MvPolynomial.Ideal                              instructions          -49.6%
+ ~Mathlib.RingTheory.MvPolynomial.Symmetric                          instructions          -33.9%
+ ~Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous                instructions          -17.0%
+ ~Mathlib.RingTheory.Nilpotent                                       instructions           -9.7%
+ ~Mathlib.RingTheory.Noetherian                                      instructions          -15.3%
+ ~Mathlib.RingTheory.OreLocalization.Basic                           instructions          -17.3%
+ ~Mathlib.RingTheory.Polynomial.Basic                                instructions          -63.1%
+ ~Mathlib.RingTheory.Polynomial.Chebyshev                            instructions          -26.0%
+ ~Mathlib.RingTheory.Polynomial.Content                              instructions          -28.3%
+ ~Mathlib.RingTheory.Polynomial.Eisenstein.Basic                     instructions          -26.6%
- ~Mathlib.RingTheory.Polynomial.Opposites                            instructions            6.0%
+ ~Mathlib.RingTheory.Polynomial.ScaleRoots                           instructions          -26.4%
+ ~Mathlib.RingTheory.Polynomial.Vieta                                instructions           -5.8%
+ ~Mathlib.RingTheory.Prime                                           instructions          -13.0%
+ ~Mathlib.RingTheory.PrincipalIdealDomain                            instructions          -45.6%
+ ~Mathlib.RingTheory.QuotientNilpotent                               instructions          -48.6%
+ ~Mathlib.RingTheory.ReesAlgebra                                     instructions          -70.7%
+ ~Mathlib.RingTheory.SimpleModule                                    instructions          -89.5%
+ ~Mathlib.RingTheory.Subring.Basic                                   instructions          -28.0%
+ ~Mathlib.RingTheory.Subring.Pointwise                               instructions          -12.0%
+ ~Mathlib.RingTheory.Subsemiring.Basic                               instructions           -5.6%
+ ~Mathlib.RingTheory.Valuation.Quotient                              instructions          -42.1%
- ~Mathlib.RingTheory.ZMod                                            instructions           10.2%
+ ~Mathlib.SetTheory.Cardinal.Cofinality                              instructions          -56.3%
+ ~Mathlib.SetTheory.Cardinal.Divisibility                            instructions           -6.5%
+ ~Mathlib.SetTheory.Ordinal.Arithmetic                               instructions          -44.2%
+ ~Mathlib.SetTheory.Ordinal.FixedPoint                               instructions          -44.6%
+ ~Mathlib.SetTheory.Ordinal.NaturalOps                               instructions           -7.6%
+ ~Mathlib.Topology.Algebra.Affine                                    instructions           -5.6%
+ ~Mathlib.Topology.Algebra.Algebra                                   instructions           -8.0%
+ ~Mathlib.Topology.Algebra.Field                                     instructions          -39.2%
+ ~Mathlib.Topology.Algebra.Group.Basic                               instructions          -10.5%
+ ~Mathlib.Topology.Algebra.GroupCompletion                           instructions           -8.7%
+ ~Mathlib.Topology.Algebra.GroupWithZero                             instructions          -12.7%
+ ~Mathlib.Topology.Algebra.InfiniteSum.Real                          instructions           -7.4%
+ ~Mathlib.Topology.Algebra.Localization                              instructions          -15.3%
+ ~Mathlib.Topology.Algebra.Module.Basic                              instructions          -54.6%
+ ~Mathlib.Topology.Algebra.Module.Determinant                        instructions          -63.2%
+ ~Mathlib.Topology.Algebra.Module.LinearPMap                         instructions           -6.6%
+ ~Mathlib.Topology.Algebra.Module.Multilinear                        instructions          -19.4%
+ ~Mathlib.Topology.Algebra.Module.Simple                             instructions          -21.9%
+ ~Mathlib.Topology.Algebra.Module.StrongTopology                     instructions          -74.4%
+ ~Mathlib.Topology.Algebra.Module.WeakDual                           instructions          -51.4%
+ ~Mathlib.Topology.Algebra.Nonarchimedean.Bases                      instructions          -11.5%
+ ~Mathlib.Topology.Algebra.Nonarchimedean.Basic                      instructions          -11.5%
+ ~Mathlib.Topology.Algebra.Order.Compact                             instructions           -6.2%
+ ~Mathlib.Topology.Algebra.Order.Field                               instructions          -10.8%
+ ~Mathlib.Topology.Algebra.Order.Floor                               instructions           -5.7%
+ ~Mathlib.Topology.Algebra.Order.IntermediateValue                   instructions          -16.3%
+ ~Mathlib.Topology.Algebra.Order.LeftRightLim                        instructions           -6.3%
+ ~Mathlib.Topology.Algebra.Order.LiminfLimsup                        instructions           -6.5%
+ ~Mathlib.Topology.Algebra.Polynomial                                instructions          -45.2%
+ ~Mathlib.Topology.Algebra.Ring.Basic                                instructions          -34.6%
+ ~Mathlib.Topology.Algebra.StarSubalgebra                            instructions          -57.4%
+ ~Mathlib.Topology.Algebra.UniformConvergence                        instructions          -22.7%
+ ~Mathlib.Topology.Algebra.UniformField                              instructions          -36.7%
+ ~Mathlib.Topology.Algebra.UniformGroup                              instructions           -5.8%
+ ~Mathlib.Topology.Algebra.UniformRing                               instructions          -17.9%
+ ~Mathlib.Topology.Basic                                             instructions           -6.2%
+ ~Mathlib.Topology.Category.CompHaus.Basic                           instructions          -11.2%
+ ~Mathlib.Topology.Category.Profinite.Basic                          instructions          -15.7%
+ ~Mathlib.Topology.Category.Top.Adjunctions                          instructions          -26.9%
- ~Mathlib.Topology.ContinuousFunction.T0Sierpinski                   instructions            7.4%
+ ~Mathlib.Topology.Filter                                            instructions           -6.1%
+ ~Mathlib.Topology.Homotopy.Basic                                    instructions           -6.1%
+ ~Mathlib.Topology.Homotopy.Equiv                                    instructions          -10.8%
+ ~Mathlib.Topology.Instances.ENNReal                                 instructions          -34.9%
+ ~Mathlib.Topology.Instances.EReal                                   instructions          -10.9%
+ ~Mathlib.Topology.Instances.Matrix                                  instructions          -22.5%
+ ~Mathlib.Topology.Instances.NNReal                                  instructions          -28.3%
+ ~Mathlib.Topology.Instances.Nat                                     instructions          -17.8%
+ ~Mathlib.Topology.Instances.Rat                                     instructions           -5.6%
+ ~Mathlib.Topology.Instances.Real                                    instructions          -13.1%
+ ~Mathlib.Topology.Instances.RealVectorSpace                         instructions          -17.3%
+ ~Mathlib.Topology.Instances.TrivSqZeroExt                           instructions           -7.5%
+ ~Mathlib.Topology.LocalHomeomorph                                   instructions          -38.2%
+ ~Mathlib.Topology.LocallyConstant.Algebra                           instructions           -6.1%
+ ~Mathlib.Topology.MetricSpace.Algebra                               instructions          -16.0%
+ ~Mathlib.Topology.MetricSpace.Basic                                 instructions           -5.9%
+ ~Mathlib.Topology.MetricSpace.CauSeqFilter                          instructions          -12.8%
+ ~Mathlib.Topology.MetricSpace.Completion                            instructions           -6.7%
+ ~Mathlib.Topology.MetricSpace.EMetricSpace                          instructions           -5.6%
+ ~Mathlib.Topology.MetricSpace.HausdorffDistance                     instructions          -11.8%
+ ~Mathlib.Topology.MetricSpace.Infsep                                instructions           -7.6%
+ ~Mathlib.Topology.MetricSpace.Isometry                              instructions           -9.0%
+ ~Mathlib.Topology.MetricSpace.Lipschitz                             instructions           -8.0%
+ ~Mathlib.Topology.MetricSpace.PiNat                                 instructions          -32.7%
+ ~Mathlib.Topology.MetricSpace.Polish                                instructions           -5.1%
- ~Mathlib.Topology.OmegaCompletePartialOrder                         instructions            7.3%
+ ~Mathlib.Topology.Order                                             instructions          -12.8%
+ ~Mathlib.Topology.PathConnected                                     instructions          -13.0%
+ ~Mathlib.Topology.Separation                                        instructions           -8.3%
+ ~Mathlib.Topology.Sequences                                         instructions           -5.8%
+ ~Mathlib.Topology.Sets.Closeds                                      instructions          -61.9%
- ~Mathlib.Topology.Sets.Compacts                                     instructions           10.0%
+ ~Mathlib.Topology.Sets.Opens                                        instructions           -7.3%
+ ~Mathlib.Topology.StoneCech                                         instructions          -11.6%
+ ~Mathlib.Topology.UniformSpace.AbsoluteValue                        instructions          -12.7%
+ ~Mathlib.Topology.UniformSpace.CompareReals                         instructions          -19.0%
+ ~Mathlib.Topology.UniformSpace.Completion                           instructions          -19.3%
+ ~Mathlib.Topology.UniformSpace.Pi                                   instructions           -9.2%
+ ~Mathlib.Topology.UniformSpace.Separation                           instructions           -7.7%
+ ~Mathlib.Topology.UniformSpace.UniformConvergenceTopology           instructions          -34.5%
+ ~Mathlib.Topology.UrysohnsLemma                                     instructions          -37.3%

There were significant changes against commit 4f47420:

  Benchmark                                                           Metric                Change
  ================================================================================================
+ build                                                               branch-misses         -22.3%
+ build                                                               branches              -26.4%
+ build                                                               elaboration           -42.4%
+ build                                                               instructions          -25.4%
+ build                                                               interpretation         -6.2%
+ build                                                               linting                -6.4%
+ build                                                               simp                  -33.7%
+ build                                                               tactic execution      -58.3%
+ build                                                               task-clock            -22.8%
+ build                                                               typeclass inference   -17.7%
+ build                                                               wall-clock            -24.3%
+ lint                                                                instructions          -39.8%
+ lint                                                                wall-clock            -41.3%
+ ~Mathlib.Algebra.Algebra.Basic                                      instructions          -29.1%
+ ~Mathlib.Algebra.Algebra.Bilinear                                   instructions          -17.9%
+ ~Mathlib.Algebra.Algebra.Equiv                                      instructions          -24.3%
+ ~Mathlib.Algebra.Algebra.Hom                                        instructions          -11.3%
+ ~Mathlib.Algebra.Algebra.Operations                                 instructions          -42.8%
+ ~Mathlib.Algebra.Algebra.Pi                                         instructions          -30.8%
+ ~Mathlib.Algebra.Algebra.Prod                                       instructions          -18.2%
+ ~Mathlib.Algebra.Algebra.RestrictScalars                            instructions          -35.1%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Basic                           instructions          -24.9%
+ ~Mathlib.Algebra.Algebra.Tower                                      instructions           -6.1%
+ ~Mathlib.Algebra.Algebra.Unitization                                instructions          -15.9%
+ ~Mathlib.Algebra.BigOperators.Associated                            instructions          -43.7%
+ ~Mathlib.Algebra.BigOperators.Finprod                               instructions           -6.4%
+ ~Mathlib.Algebra.BigOperators.Finsupp                               instructions          -16.5%
+ ~Mathlib.Algebra.BigOperators.Order                                 instructions           -8.4%
+ ~Mathlib.Algebra.BigOperators.Pi                                    instructions          -10.5%
+ ~Mathlib.Algebra.Category.GroupCat.Basic                            instructions          -23.5%
+ ~Mathlib.Algebra.Category.GroupCat.Preadditive                      instructions           -6.5%
+ ~Mathlib.Algebra.Category.ModuleCat.Basic                           instructions          -20.8%
+ ~Mathlib.Algebra.Category.ModuleCat.EpiMono                         instructions          -62.1%
+ ~Mathlib.Algebra.Category.ModuleCat.Products                        instructions          -52.1%
+ ~Mathlib.Algebra.Category.ModuleCat.Tannaka                         instructions          -12.6%
+ ~Mathlib.Algebra.Category.MonCat.Basic                              instructions          -12.6%
+ ~Mathlib.Algebra.CharP.Algebra                                      instructions          -26.0%
+ ~Mathlib.Algebra.CharP.Quotient                                     instructions          -20.2%
+ ~Mathlib.Algebra.CharZero.Lemmas                                    instructions           -5.4%
+ ~Mathlib.Algebra.CharZero.Quotient                                  instructions          -26.3%
+ ~Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv                instructions          -15.5%
+ ~Mathlib.Algebra.CubicDiscriminant                                  instructions          -61.9%
+ ~Mathlib.Algebra.DirectSum.Basic                                    instructions          -19.6%
+ ~Mathlib.Algebra.DirectSum.Finsupp                                  instructions          -26.4%
+ ~Mathlib.Algebra.DirectSum.Module                                   instructions          -38.2%
+ ~Mathlib.Algebra.DualNumber                                         instructions          -22.7%
+ ~Mathlib.Algebra.EuclideanDomain.Basic                              instructions           -6.6%
+ ~Mathlib.Algebra.Field.Power                                        instructions           -5.5%
+ ~Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra                       instructions          -27.5%
+ ~Mathlib.Algebra.GCDMonoid.Basic                                    instructions           -5.0%
+ ~Mathlib.Algebra.GCDMonoid.Div                                      instructions          -61.1%
+ ~Mathlib.Algebra.GeomSum                                            instructions          -46.4%
+ ~Mathlib.Algebra.Group.Conj                                         instructions          -15.3%
+ ~Mathlib.Algebra.Group.Opposite                                     instructions          -15.9%
+ ~Mathlib.Algebra.Group.Prod                                         instructions           -7.2%
+ ~Mathlib.Algebra.Group.TypeTags                                     instructions           -5.3%
+ ~Mathlib.Algebra.Group.WithOne.Basic                                instructions           -9.0%
+ ~Mathlib.Algebra.Group.WithOne.Units                                instructions           -7.8%
+ ~Mathlib.Algebra.GroupPower.Identities                              instructions           -8.5%
+ ~Mathlib.Algebra.GroupRingAction.Invariant                          instructions          -49.1%
+ ~Mathlib.Algebra.Hom.Centroid                                       instructions          -20.7%
+ ~Mathlib.Algebra.Hom.Equiv.Basic                                    instructions           -6.6%
+ ~Mathlib.Algebra.Hom.Equiv.Units.Basic                              instructions           -7.2%
+ ~Mathlib.Algebra.Hom.GroupInstances                                 instructions          -20.9%
+ ~Mathlib.Algebra.Hom.NonUnitalAlg                                   instructions           -8.2%
+ ~Mathlib.Algebra.Hom.Units                                          instructions           -5.0%
+ ~Mathlib.Algebra.Homology.Additive                                  instructions          -32.7%
+ ~Mathlib.Algebra.Homology.Flip                                      instructions          -75.7%
+ ~Mathlib.Algebra.Homology.Homology                                  instructions          -30.9%
+ ~Mathlib.Algebra.Homology.Homotopy                                  instructions          -34.7%
+ ~Mathlib.Algebra.Homology.HomotopyCategory                          instructions          -57.2%
+ ~Mathlib.Algebra.Homology.Single                                    instructions          -21.4%
+ ~Mathlib.Algebra.Lie.Basic                                          instructions          -26.2%
+ ~Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra                       instructions           -6.6%
+ ~Mathlib.Algebra.Lie.Subalgebra                                     instructions          -32.7%
+ ~Mathlib.Algebra.LinearRecurrence                                   instructions          -24.4%
+ ~Mathlib.Algebra.Module.Algebra                                     instructions          -15.1%
+ ~Mathlib.Algebra.Module.Equiv                                       instructions           -9.3%
+ ~Mathlib.Algebra.Module.LinearMap                                   instructions           -9.6%
+ ~Mathlib.Algebra.Module.Pi                                          instructions          -12.0%
+ ~Mathlib.Algebra.Module.Projective                                  instructions          -35.5%
+ ~Mathlib.Algebra.Module.Submodule.Pointwise                         instructions           -6.6%
+ ~Mathlib.Algebra.Module.ULift                                       instructions          -17.4%
+ ~Mathlib.Algebra.MonoidAlgebra.Basic                                instructions          -40.1%
+ ~Mathlib.Algebra.MonoidAlgebra.Division                             instructions          -48.8%
+ ~Mathlib.Algebra.MonoidAlgebra.Ideal                                instructions          -49.5%
+ ~Mathlib.Algebra.MonoidAlgebra.Support                              instructions          -23.9%
+ ~Mathlib.Algebra.Order.AbsoluteValue                                instructions          -18.3%
+ ~Mathlib.Algebra.Order.Algebra                                      instructions           -9.2%
+ ~Mathlib.Algebra.Order.Archimedean                                  instructions          -16.7%
+ ~Mathlib.Algebra.Order.Chebyshev                                    instructions          -20.8%
+ ~Mathlib.Algebra.Order.EuclideanAbsoluteValue                       instructions           -5.1%
+ ~Mathlib.Algebra.Order.Field.Basic                                  instructions           -8.0%
+ ~Mathlib.Algebra.Order.Field.Power                                  instructions           -9.0%
+ ~Mathlib.Algebra.Order.Floor                                        instructions          -10.2%
+ ~Mathlib.Algebra.Order.Group.Defs                                   instructions          -16.1%
+ ~Mathlib.Algebra.Order.Group.OrderIso                               instructions           -7.9%
+ ~Mathlib.Algebra.Order.Hom.Monoid                                   instructions           -6.8%
+ ~Mathlib.Algebra.Order.Hom.Ring                                     instructions           -7.1%
+ ~Mathlib.Algebra.Order.Kleene                                       instructions           -5.4%
+ ~Mathlib.Algebra.Order.LatticeGroup                                 instructions           -7.4%
+ ~Mathlib.Algebra.Order.Module                                       instructions          -18.3%
+ ~Mathlib.Algebra.Order.Monoid.ToMulBot                              instructions           -7.7%
+ ~Mathlib.Algebra.Order.Nonneg.Field                                 instructions          -24.6%
+ ~Mathlib.Algebra.Order.Nonneg.Ring                                  instructions           -7.9%
+ ~Mathlib.Algebra.Order.Positive.Field                               instructions           -6.5%
+ ~Mathlib.Algebra.Order.Rearrangement                                instructions          -14.2%
+ ~Mathlib.Algebra.Order.Ring.Abs                                     instructions          -10.1%
+ ~Mathlib.Algebra.Order.Ring.Cone                                    instructions           -6.4%
+ ~Mathlib.Algebra.Order.Ring.Defs                                    instructions          -14.8%
+ ~Mathlib.Algebra.Order.Ring.WithTop                                 instructions          -11.8%
+ ~Mathlib.Algebra.Order.SMul                                         instructions           -9.3%
+ ~Mathlib.Algebra.Order.WithZero                                     instructions          -17.7%
+ ~Mathlib.Algebra.Periodic                                           instructions           -6.1%
+ ~Mathlib.Algebra.Polynomial.BigOperators                            instructions          -15.5%
+ ~Mathlib.Algebra.Polynomial.GroupRingAction                         instructions          -27.8%
+ ~Mathlib.Algebra.QuadraticDiscriminant                              instructions          -38.0%
+ ~Mathlib.Algebra.Quandle                                            instructions          -35.5%
+ ~Mathlib.Algebra.Ring.AddAut                                        instructions          -11.5%
+ ~Mathlib.Algebra.Ring.Aut                                           instructions          -13.5%
+ ~Mathlib.Algebra.Ring.CompTypeclasses                               instructions          -10.7%
+ ~Mathlib.Algebra.Ring.Equiv                                         instructions          -10.5%
+ ~Mathlib.Algebra.Ring.Opposite                                      instructions          -16.1%
+ ~Mathlib.Algebra.Ring.Prod                                          instructions          -11.6%
+ ~Mathlib.Algebra.RingQuot                                           instructions          -13.1%
+ ~Mathlib.Algebra.Star.Basic                                         instructions           -7.9%
+ ~Mathlib.Algebra.Star.CHSH                                          instructions          -56.4%
+ ~Mathlib.Algebra.Star.Free                                          instructions           -5.6%
+ ~Mathlib.Algebra.Star.Module                                        instructions          -34.7%
+ ~Mathlib.Algebra.Star.SelfAdjoint                                   instructions          -20.8%
+ ~Mathlib.Algebra.Star.StarAlgHom                                    instructions           -9.4%
+ ~Mathlib.Algebra.Star.Subalgebra                                    instructions           -9.1%
+ ~Mathlib.Algebra.TrivSqZeroExt                                      instructions          -29.2%
+ ~Mathlib.Algebra.Tropical.Lattice                                   instructions           -7.2%
+ ~Mathlib.AlgebraicTopology.AlternatingFaceMapComplex                instructions          -29.8%
+ ~Mathlib.AlgebraicTopology.CechNerve                                instructions          -12.4%
+ ~Mathlib.AlgebraicTopology.DoldKan.Compatibility                    instructions          -44.8%
+ ~Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive              instructions          -88.5%
+ ~Mathlib.AlgebraicTopology.DoldKan.FunctorN                         instructions          -70.7%
+ ~Mathlib.AlgebraicTopology.DoldKan.GammaCompN                       instructions          -86.3%
+ ~Mathlib.AlgebraicTopology.DoldKan.Homotopies                       instructions          -11.9%
+ ~Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence              instructions          -25.3%
+ ~Mathlib.AlgebraicTopology.DoldKan.NCompGamma                       instructions          -63.3%
+ ~Mathlib.AlgebraicTopology.DoldKan.NReflectsIso                     instructions          -55.5%
+ ~Mathlib.AlgebraicTopology.DoldKan.Normalized                       instructions          -68.5%
+ ~Mathlib.AlgebraicTopology.DoldKan.PInfty                           instructions          -58.8%
+ ~Mathlib.AlgebraicTopology.DoldKan.Projections                      instructions          -28.2%
+ ~Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject            instructions          -21.1%
+ ~Mathlib.AlgebraicTopology.ExtraDegeneracy                          instructions          -12.5%
+ ~Mathlib.AlgebraicTopology.MooreComplex                             instructions          -16.5%
+ ~Mathlib.AlgebraicTopology.Nerve                                    instructions          -14.7%
+ ~Mathlib.AlgebraicTopology.SimplicialObject                         instructions          -32.1%
+ ~Mathlib.AlgebraicTopology.SimplicialSet                            instructions          -14.6%
+ ~Mathlib.AlgebraicTopology.TopologicalSimplex                       instructions          -13.4%
+ ~Mathlib.Analysis.Asymptotics.AsymptoticEquivalent                  instructions          -21.6%
+ ~Mathlib.Analysis.Asymptotics.SpecificAsymptotics                   instructions          -15.7%
+ ~Mathlib.Analysis.Asymptotics.SuperpolynomialDecay                  instructions          -13.4%
+ ~Mathlib.Analysis.BoxIntegral.Box.Basic                             instructions           -8.1%
+ ~Mathlib.Analysis.BoxIntegral.Box.SubboxInduction                   instructions           -5.6%
+ ~Mathlib.Analysis.Convex.Basic                                      instructions           -5.7%
+ ~Mathlib.Analysis.Convex.Caratheodory                               instructions           -9.9%
+ ~Mathlib.Analysis.Convex.Combination                                instructions          -42.4%
+ ~Mathlib.Analysis.Convex.Complex                                    instructions          -35.5%
+ ~Mathlib.Analysis.Convex.Exposed                                    instructions          -65.5%
+ ~Mathlib.Analysis.Convex.Extrema                                    instructions          -15.3%
+ ~Mathlib.Analysis.Convex.Function                                   instructions          -11.2%
+ ~Mathlib.Analysis.Convex.Independent                                instructions          -12.9%
+ ~Mathlib.Analysis.Convex.Jensen                                     instructions          -18.0%
+ ~Mathlib.Analysis.Convex.Normed                                     instructions          -16.3%
+ ~Mathlib.Analysis.Convex.Quasiconvex                                instructions          -16.2%
+ ~Mathlib.Analysis.Convex.Segment                                    instructions           -9.4%
+ ~Mathlib.Analysis.Convex.Slope                                      instructions          -40.6%
+ ~Mathlib.Analysis.Convex.Strict                                     instructions           -5.9%
+ ~Mathlib.Analysis.Convex.Topology                                   instructions          -10.2%
+ ~Mathlib.Analysis.Hofer                                             instructions           -7.8%
+ ~Mathlib.Analysis.LocallyConvex.Bounded                             instructions          -44.9%
+ ~Mathlib.Analysis.LocallyConvex.Polar                               instructions          -71.8%
+ ~Mathlib.Analysis.Normed.Field.Basic                                instructions          -14.6%
+ ~Mathlib.Analysis.Normed.Field.InfiniteSum                          instructions          -17.2%
+ ~Mathlib.Analysis.Normed.Group.AddTorsor                            instructions          -19.1%
+ ~Mathlib.Analysis.Normed.Group.Basic                                instructions           -7.7%
+ ~Mathlib.Analysis.Normed.Group.Hom                                  instructions          -13.0%
+ ~Mathlib.Analysis.Normed.Group.HomCompletion                        instructions          -49.8%
+ ~Mathlib.Analysis.Normed.Group.InfiniteSum                          instructions           -5.8%
+ ~Mathlib.Analysis.Normed.Order.Lattice                              instructions           -5.6%
+ ~Mathlib.Analysis.Normed.Order.UpperLower                           instructions           -6.4%
+ ~Mathlib.Analysis.Normed.Ring.Seminorm                              instructions          -36.9%
+ ~Mathlib.Analysis.NormedSpace.AddTorsor                             instructions          -55.6%
+ ~Mathlib.Analysis.NormedSpace.Basic                                 instructions          -34.0%
+ ~Mathlib.Analysis.NormedSpace.ConformalLinearMap                    instructions          -68.0%
+ ~Mathlib.Analysis.NormedSpace.ContinuousLinearMap                   instructions          -80.3%
+ ~Mathlib.Analysis.NormedSpace.LinearIsometry                        instructions          -21.3%
+ ~Mathlib.Analysis.NormedSpace.Ray                                   instructions          -11.8%
+ ~Mathlib.Analysis.NormedSpace.RieszLemma                            instructions          -12.8%
+ ~Mathlib.Analysis.NormedSpace.Star.Basic                            instructions          -65.0%
+ ~Mathlib.Analysis.Seminorm                                          instructions          -30.9%
+ ~Mathlib.Analysis.SpecialFunctions.Polynomials                      instructions          -17.9%
+ ~Mathlib.Analysis.SpecificLimits.Basic                              instructions          -20.2%
+ ~Mathlib.CategoryTheory.Abelian.Basic                               instructions          -10.6%
+ ~Mathlib.CategoryTheory.Abelian.Exact                               instructions           -6.4%
+ ~Mathlib.CategoryTheory.Abelian.FunctorCategory                     instructions          -11.6%
+ ~Mathlib.CategoryTheory.Abelian.Opposite                            instructions          -16.6%
+ ~Mathlib.CategoryTheory.Abelian.Subobject                           instructions           -8.0%
+ ~Mathlib.CategoryTheory.Action                                      instructions          -17.6%
+ ~Mathlib.CategoryTheory.Adjunction.Basic                            instructions           -5.2%
+ ~Mathlib.CategoryTheory.Adjunction.FullyFaithful                    instructions          -15.1%
+ ~Mathlib.CategoryTheory.Adjunction.Limits                           instructions          -31.1%
+ ~Mathlib.CategoryTheory.Adjunction.Opposites                        instructions           -6.7%
+ ~Mathlib.CategoryTheory.Adjunction.Over                             instructions          -15.1%
+ ~Mathlib.CategoryTheory.Adjunction.Whiskering                       instructions          -63.1%
+ ~Mathlib.CategoryTheory.Arrow                                       instructions           -7.9%
+ ~Mathlib.CategoryTheory.Category.Bipointed                          instructions          -14.4%
+ ~Mathlib.CategoryTheory.Category.Cat                                instructions          -51.9%
+ ~Mathlib.CategoryTheory.Category.QuivCat                            instructions           -7.3%
+ ~Mathlib.CategoryTheory.Category.TwoP                               instructions          -29.9%
+ ~Mathlib.CategoryTheory.Conj                                        instructions           -6.9%
+ ~Mathlib.CategoryTheory.Elements                                    instructions          -50.8%
+ ~Mathlib.CategoryTheory.Equivalence                                 instructions           -6.7%
+ ~Mathlib.CategoryTheory.EssentialImage                              instructions           -7.8%
+ ~Mathlib.CategoryTheory.FinCategory                                 instructions          -28.2%
+ ~Mathlib.CategoryTheory.FintypeCat                                  instructions           -9.6%
+ ~Mathlib.CategoryTheory.Functor.Currying                            instructions          -15.0%
+ ~Mathlib.CategoryTheory.Functor.InvIsos                             instructions           -7.5%
+ ~Mathlib.CategoryTheory.Functor.LeftDerived                         instructions          -76.9%
+ ~Mathlib.CategoryTheory.GradedObject                                instructions          -37.9%
+ ~Mathlib.CategoryTheory.Grothendieck                                instructions          -34.4%
+ ~Mathlib.CategoryTheory.Idempotents.FunctorCategories               instructions          -11.7%
+ ~Mathlib.CategoryTheory.Idempotents.FunctorExtension                instructions          -71.6%
+ ~Mathlib.CategoryTheory.Idempotents.HomologicalComplex              instructions          -50.5%
+ ~Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi                  instructions          -25.1%
+ ~Mathlib.CategoryTheory.Limits.ColimitLimit                         instructions          -42.2%
+ ~Mathlib.CategoryTheory.Limits.Comma                                instructions          -35.4%
+ ~Mathlib.CategoryTheory.Limits.Cones                                instructions          -17.9%
+ ~Mathlib.CategoryTheory.Limits.Constructions.Over.Connected         instructions           -7.5%
+ ~Mathlib.CategoryTheory.Limits.Creates                              instructions           -6.1%
+ ~Mathlib.CategoryTheory.Limits.ExactFunctor                         instructions          -12.2%
+ ~Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit   instructions          -15.3%
+ ~Mathlib.CategoryTheory.Limits.FunctorCategory                      instructions          -19.9%
+ ~Mathlib.CategoryTheory.Limits.HasLimits                            instructions          -15.2%
+ ~Mathlib.CategoryTheory.Limits.KanExtension                         instructions          -35.4%
+ ~Mathlib.CategoryTheory.Limits.Opposites                            instructions           -8.9%
+ ~Mathlib.CategoryTheory.Limits.Preserves.Basic                      instructions          -29.0%
+ ~Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory            instructions          -59.0%
+ ~Mathlib.CategoryTheory.Limits.Preserves.Limits                     instructions           -7.6%
+ ~Mathlib.CategoryTheory.Limits.Preserves.Opposites                  instructions          -35.9%
+ ~Mathlib.CategoryTheory.Limits.Presheaf                             instructions          -77.0%
+ ~Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer                instructions           -6.2%
+ ~Mathlib.CategoryTheory.Limits.Shapes.Products                      instructions           -7.1%
+ ~Mathlib.CategoryTheory.Limits.Shapes.Types                         instructions           -6.3%
+ ~Mathlib.CategoryTheory.Linear.Basic                                instructions          -75.3%
+ ~Mathlib.CategoryTheory.Linear.Yoneda                               instructions          -80.8%
+ ~Mathlib.CategoryTheory.Localization.Construction                   instructions          -49.0%
+ ~Mathlib.CategoryTheory.Localization.Opposite                       instructions          -32.7%
+ ~Mathlib.CategoryTheory.Localization.Predicate                      instructions          -24.8%
+ ~Mathlib.CategoryTheory.Monad.Adjunction                            instructions          -30.8%
+ ~Mathlib.CategoryTheory.Monad.Limits                                instructions           -9.7%
+ ~Mathlib.CategoryTheory.Monad.Products                              instructions           -6.7%
+ ~Mathlib.CategoryTheory.Monoidal.Functor                            instructions           -7.9%
+ ~Mathlib.CategoryTheory.Monoidal.Linear                             instructions           -5.6%
+ ~Mathlib.CategoryTheory.Monoidal.NaturalTransformation              instructions           -8.4%
+ ~Mathlib.CategoryTheory.Monoidal.Transport                          instructions          -12.7%
+ ~Mathlib.CategoryTheory.Opposites                                   instructions          -12.1%
+ ~Mathlib.CategoryTheory.Over                                        instructions           -6.9%
+ ~Mathlib.CategoryTheory.PEmpty                                      instructions           -6.0%
+ ~Mathlib.CategoryTheory.Preadditive.AdditiveFunctor                 instructions           -8.9%
+ ~Mathlib.CategoryTheory.Preadditive.EilenbergMoore                  instructions           -6.9%
+ ~Mathlib.CategoryTheory.Preadditive.Yoneda.Basic                    instructions          -61.2%
+ ~Mathlib.CategoryTheory.Products.Basic                              instructions           -8.2%
+ ~Mathlib.CategoryTheory.Shift.Basic                                 instructions           -6.3%
+ ~Mathlib.CategoryTheory.Sigma.Basic                                 instructions          -16.5%
+ ~Mathlib.CategoryTheory.SingleObj                                   instructions          -23.6%
+ ~Mathlib.CategoryTheory.Sites.Adjunction                            instructions          -92.7%
+ ~Mathlib.CategoryTheory.Sites.LeftExact                             instructions          -71.3%
+ ~Mathlib.CategoryTheory.Sites.Limits                                instructions           -9.1%
+ ~Mathlib.CategoryTheory.Sites.Plus                                  instructions          -40.0%
+ ~Mathlib.CategoryTheory.Sites.Sheaf                                 instructions           -7.9%
+ ~Mathlib.CategoryTheory.Sites.Sheafification                        instructions          -70.0%
+ ~Mathlib.CategoryTheory.Skeletal                                    instructions           -6.5%
+ ~Mathlib.CategoryTheory.StructuredArrow                             instructions           -7.5%
+ ~Mathlib.CategoryTheory.Subobject.Basic                             instructions          -34.4%
+ ~Mathlib.CategoryTheory.Subobject.Lattice                           instructions          -25.3%
+ ~Mathlib.CategoryTheory.Subobject.MonoOver                          instructions          -12.5%
+ ~Mathlib.CategoryTheory.Whiskering                                  instructions          -20.4%
+ ~Mathlib.CategoryTheory.Yoneda                                      instructions          -31.4%
+ ~Mathlib.Combinatorics.Additive.Energy                              instructions           -7.9%
+ ~Mathlib.Combinatorics.Additive.PluenneckeRuzsa                     instructions          -13.4%
+ ~Mathlib.Combinatorics.Catalan                                      instructions          -55.4%
+ ~Mathlib.Combinatorics.Composition                                  instructions           -8.1%
+ ~Mathlib.Combinatorics.SetFamily.Compression.UV                     instructions           -8.0%
+ ~Mathlib.Combinatorics.SetFamily.Kleitman                           instructions          -17.7%
+ ~Mathlib.Combinatorics.SetFamily.LYM                                instructions           -9.2%
+ ~Mathlib.Combinatorics.SimpleGraph.Density                          instructions          -14.4%
+ ~Mathlib.Combinatorics.SimpleGraph.Matching                         instructions          -15.3%
+ ~Mathlib.Combinatorics.SimpleGraph.Prod                             instructions           -6.7%
+ ~Mathlib.Combinatorics.SimpleGraph.Regularity.Energy                instructions           -6.7%
+ ~Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform               instructions           -6.9%
+ ~Mathlib.Control.LawfulFix                                          instructions          -30.1%
+ ~Mathlib.Data.Complex.Basic                                         instructions          -54.0%
+ ~Mathlib.Data.Complex.Determinant                                   instructions          -63.7%
+ ~Mathlib.Data.Complex.Exponential                                   instructions          -32.6%
+ ~Mathlib.Data.Complex.Module                                        instructions          -38.1%
+ ~Mathlib.Data.Dfinsupp.Basic                                        instructions          -18.1%
+ ~Mathlib.Data.Dfinsupp.Interval                                     instructions           -5.5%
+ ~Mathlib.Data.Dfinsupp.NeLocus                                      instructions          -13.3%
- ~Mathlib.Data.Fin.Basic                                             instructions           12.0%
+ ~Mathlib.Data.Fin.Tuple.BubbleSortInduction                         instructions          -18.1%
+ ~Mathlib.Data.Fin.Tuple.Sort                                        instructions           -7.0%
+ ~Mathlib.Data.Finset.Pi                                             instructions          -20.2%
+ ~Mathlib.Data.Finset.Sym                                            instructions           -8.0%
+ ~Mathlib.Data.Finsupp.Antidiagonal                                  instructions          -45.2%
+ ~Mathlib.Data.Finsupp.Basic                                         instructions          -16.7%
+ ~Mathlib.Data.Finsupp.Multiset                                      instructions          -68.5%
+ ~Mathlib.Data.Finsupp.NeLocus                                       instructions          -15.6%
+ ~Mathlib.Data.Finsupp.Pointwise                                     instructions           -5.5%
+ ~Mathlib.Data.Finsupp.ToDfinsupp                                    instructions          -17.8%
+ ~Mathlib.Data.Fintype.Basic                                         instructions           -9.2%
+ ~Mathlib.Data.Fintype.Powerset                                      instructions          -22.5%
+ ~Mathlib.Data.Int.AbsoluteValue                                     instructions          -44.9%
+ ~Mathlib.Data.Int.Associated                                        instructions           -6.1%
+ ~Mathlib.Data.Int.Cast.Lemmas                                       instructions           -7.9%
+ ~Mathlib.Data.Int.Cast.Prod                                         instructions           -7.2%
- ~Mathlib.Data.Int.ConditionallyCompleteOrder                        instructions           15.0%
+ ~Mathlib.Data.Int.Log                                               instructions          -40.0%
+ ~Mathlib.Data.List.Cycle                                            instructions          -17.1%
+ ~Mathlib.Data.List.Join                                             instructions           -5.1%
+ ~Mathlib.Data.Matrix.Basic                                          instructions          -18.8%
+ ~Mathlib.Data.Matrix.Block                                          instructions           -5.5%
+ ~Mathlib.Data.Matrix.DualNumber                                     instructions          -23.1%
+ ~Mathlib.Data.Matrix.Rank                                           instructions          -81.1%
+ ~Mathlib.Data.Multiset.Basic                                        instructions           -5.2%
+ ~Mathlib.Data.Multiset.Pi                                           instructions           -5.5%
+ ~Mathlib.Data.MvPolynomial.Basic                                    instructions          -19.9%
+ ~Mathlib.Data.MvPolynomial.CommRing                                 instructions          -51.4%
- ~Mathlib.Data.MvPolynomial.Division                                 instructions            5.1%
+ ~Mathlib.Data.MvPolynomial.Equiv                                    instructions          -56.5%
+ ~Mathlib.Data.MvPolynomial.Expand                                   instructions          -34.8%
+ ~Mathlib.Data.MvPolynomial.Funext                                   instructions          -61.7%
+ ~Mathlib.Data.MvPolynomial.Monad                                    instructions          -30.2%
+ ~Mathlib.Data.MvPolynomial.Polynomial                               instructions           -7.6%
+ ~Mathlib.Data.MvPolynomial.Rename                                   instructions          -29.2%
+ ~Mathlib.Data.MvPolynomial.Supported                                instructions          -51.3%
+ ~Mathlib.Data.MvPolynomial.Variables                                instructions          -11.1%
- ~Mathlib.Data.Nat.Bitwise                                           instructions            5.1%
+ ~Mathlib.Data.Nat.Cast.Field                                        instructions           -6.2%
+ ~Mathlib.Data.Nat.Choose.Bounds                                     instructions           -6.5%
+ ~Mathlib.Data.Nat.Choose.Multinomial                                instructions           -5.8%
- ~Mathlib.Data.Nat.Digits                                            instructions            7.9%
+ ~Mathlib.Data.Nat.Factorization.Basic                               instructions          -21.4%
+ ~Mathlib.Data.Nat.Order.Basic                                       instructions          -11.6%
+ ~Mathlib.Data.Nat.PSub                                              instructions           -7.6%
+ ~Mathlib.Data.Nat.Parity                                            instructions           -5.2%
+ ~Mathlib.Data.Nat.Prime                                             instructions           -6.6%
+ ~Mathlib.Data.Nat.Totient                                           instructions          -10.6%
+ ~Mathlib.Data.Num.Lemmas                                            instructions           -5.1%
+ ~Mathlib.Data.PFunctor.Multivariate.M                               instructions           -5.7%
+ ~Mathlib.Data.PNat.Interval                                         instructions           -8.0%
+ ~Mathlib.Data.PNat.Xgcd                                             instructions           -5.3%
+ ~Mathlib.Data.Pi.Interval                                           instructions          -10.3%
+ ~Mathlib.Data.Polynomial.Basic                                      instructions          -12.3%
+ ~Mathlib.Data.Polynomial.Coeff                                      instructions           -5.6%
+ ~Mathlib.Data.Polynomial.Degree.CardPowDegree                       instructions          -52.2%
+ ~Mathlib.Data.Polynomial.Degree.Definitions                         instructions           -7.8%
+ ~Mathlib.Data.Polynomial.Degree.Lemmas                              instructions           -5.7%
+ ~Mathlib.Data.Polynomial.DenomsClearable                            instructions          -51.5%
+ ~Mathlib.Data.Polynomial.Derivative                                 instructions          -27.8%
+ ~Mathlib.Data.Polynomial.Div                                        instructions          -16.9%
+ ~Mathlib.Data.Polynomial.EraseLead                                  instructions           -6.7%
+ ~Mathlib.Data.Polynomial.Eval                                       instructions          -20.8%
+ ~Mathlib.Data.Polynomial.FieldDivision                              instructions          -78.6%
+ ~Mathlib.Data.Polynomial.HasseDeriv                                 instructions          -40.2%
+ ~Mathlib.Data.Polynomial.Inductions                                 instructions           -5.1%
+ ~Mathlib.Data.Polynomial.IntegralNormalization                      instructions           -8.3%
+ ~Mathlib.Data.Polynomial.Lifts                                      instructions          -39.6%
+ ~Mathlib.Data.Polynomial.Module                                     instructions          -58.0%
+ ~Mathlib.Data.Polynomial.Monic                                      instructions           -6.6%
+ ~Mathlib.Data.Polynomial.Monomial                                   instructions          -58.4%
+ ~Mathlib.Data.Polynomial.PartialFractions                           instructions          -70.4%
+ ~Mathlib.Data.Polynomial.Reverse                                    instructions           -6.0%
+ ~Mathlib.Data.Polynomial.RingDivision                               instructions          -22.5%
+ ~Mathlib.Data.Polynomial.Splits                                     instructions          -83.6%
+ ~Mathlib.Data.Polynomial.Taylor                                     instructions          -14.0%
+ ~Mathlib.Data.Rat.BigOperators                                      instructions           -5.9%
+ ~Mathlib.Data.Rat.Cast                                              instructions          -18.7%
+ ~Mathlib.Data.Rat.Floor                                             instructions          -23.2%
+ ~Mathlib.Data.Rat.Lemmas                                            instructions           -6.9%
+ ~Mathlib.Data.Rat.NNRat                                             instructions          -25.1%
+ ~Mathlib.Data.Rat.Order                                             instructions           -9.0%
+ ~Mathlib.Data.Real.Basic                                            instructions          -65.9%
+ ~Mathlib.Data.Real.Cardinality                                      instructions           -7.7%
+ ~Mathlib.Data.Real.CauSeq                                           instructions          -45.1%
+ ~Mathlib.Data.Real.CauSeqCompletion                                 instructions          -39.7%
+ ~Mathlib.Data.Real.ConjugateExponents                               instructions           -6.0%
+ ~Mathlib.Data.Real.ENNReal                                          instructions          -38.6%
+ ~Mathlib.Data.Real.ENatENNReal                                      instructions          -49.4%
+ ~Mathlib.Data.Real.EReal                                            instructions           -9.8%
+ ~Mathlib.Data.Real.Hyperreal                                        instructions          -10.4%
+ ~Mathlib.Data.Real.NNReal                                           instructions          -30.3%
+ ~Mathlib.Data.Real.Pointwise                                        instructions          -12.5%
+ ~Mathlib.Data.Real.Sqrt                                             instructions          -11.5%
+ ~Mathlib.Data.Set.Intervals.Disjoint                                instructions           -6.1%
+ ~Mathlib.Data.Set.Intervals.IsoIoo                                  instructions          -17.1%
+ ~Mathlib.Data.Set.Intervals.SurjOn                                  instructions           -8.2%
- ~Mathlib.Data.Set.Semiring                                          instructions            7.5%
+ ~Mathlib.Data.String.Basic                                          instructions          -24.0%
+ ~Mathlib.Data.Vector.Basic                                          instructions          -21.6%
+ ~Mathlib.Data.ZMod.Basic                                            instructions           -7.9%
- ~Mathlib.Data.ZMod.Coprime                                          instructions            7.6%
+ ~Mathlib.Data.ZMod.Defs                                             instructions           -8.2%
+ ~Mathlib.Deprecated.Subfield                                        instructions          -10.5%
+ ~Mathlib.Deprecated.Subgroup                                        instructions           -8.5%
+ ~Mathlib.Deprecated.Subring                                         instructions           -9.9%
+ ~Mathlib.FieldTheory.MvPolynomial                                   instructions          -51.3%
+ ~Mathlib.FieldTheory.PerfectClosure                                 instructions          -12.4%
+ ~Mathlib.FieldTheory.Subfield                                       instructions          -21.6%
+ ~Mathlib.FieldTheory.Tower                                          instructions          -82.2%
+ ~Mathlib.GroupTheory.Abelianization                                 instructions          -18.0%
+ ~Mathlib.GroupTheory.Commensurable                                  instructions           -5.6%
+ ~Mathlib.GroupTheory.Commutator                                     instructions           -8.9%
+ ~Mathlib.GroupTheory.CommutingProbability                           instructions          -14.8%
- ~Mathlib.GroupTheory.Divisible                                      instructions            6.5%
+ ~Mathlib.GroupTheory.Finiteness                                     instructions           -9.3%
+ ~Mathlib.GroupTheory.FreeAbelianGroup                               instructions          -15.2%
+ ~Mathlib.GroupTheory.FreeAbelianGroupFinsupp                        instructions          -11.3%
+ ~Mathlib.GroupTheory.FreeGroup                                      instructions           -7.7%
+ ~Mathlib.GroupTheory.FreeProduct                                    instructions          -33.8%
+ ~Mathlib.GroupTheory.GroupAction.ConjAct                            instructions          -28.3%
+ ~Mathlib.GroupTheory.GroupAction.FixingSubgroup                     instructions          -10.2%
+ ~Mathlib.GroupTheory.Index                                          instructions           -6.9%
+ ~Mathlib.GroupTheory.IsFreeGroup                                    instructions           -7.1%
+ ~Mathlib.GroupTheory.MonoidLocalization                             instructions           -7.2%
+ ~Mathlib.GroupTheory.Perm.Basic                                     instructions           -8.4%
+ ~Mathlib.GroupTheory.Perm.Cycle.Basic                               instructions          -13.9%
+ ~Mathlib.GroupTheory.Perm.Cycle.Type                                instructions          -24.5%
+ ~Mathlib.GroupTheory.Perm.Fin                                       instructions           -9.0%
+ ~Mathlib.GroupTheory.Perm.Sign                                      instructions           -8.0%
+ ~Mathlib.GroupTheory.Perm.Subgroup                                  instructions           -8.9%
+ ~Mathlib.GroupTheory.QuotientGroup                                  instructions          -13.1%
+ ~Mathlib.GroupTheory.SemidirectProduct                              instructions           -7.2%
+ ~Mathlib.GroupTheory.SpecificGroups.Alternating                     instructions          -63.7%
+ ~Mathlib.GroupTheory.Subgroup.Basic                                 instructions          -13.1%
+ ~Mathlib.GroupTheory.Subgroup.Finite                                instructions          -11.5%
+ ~Mathlib.GroupTheory.Subgroup.Pointwise                             instructions          -11.9%
+ ~Mathlib.GroupTheory.Submonoid.Inverses                             instructions          -14.2%
+ ~Mathlib.GroupTheory.Submonoid.Pointwise                            instructions          -20.0%
+ ~Mathlib.LinearAlgebra.AffineSpace.AffineEquiv                      instructions          -18.3%
+ ~Mathlib.LinearAlgebra.AffineSpace.AffineMap                        instructions          -45.5%
+ ~Mathlib.LinearAlgebra.AffineSpace.AffineSubspace                   instructions          -13.1%
+ ~Mathlib.LinearAlgebra.AffineSpace.Basis                            instructions          -32.5%
+ ~Mathlib.LinearAlgebra.AffineSpace.Combination                      instructions          -60.1%
+ ~Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional                instructions          -55.2%
+ ~Mathlib.LinearAlgebra.AffineSpace.Independent                      instructions          -37.0%
+ ~Mathlib.LinearAlgebra.AffineSpace.Matrix                           instructions          -58.6%
+ ~Mathlib.LinearAlgebra.AffineSpace.MidpointZero                     instructions          -18.1%
+ ~Mathlib.LinearAlgebra.AffineSpace.Ordered                          instructions          -42.3%
+ ~Mathlib.LinearAlgebra.AffineSpace.Restrict                         instructions          -60.1%
+ ~Mathlib.LinearAlgebra.AffineSpace.Slope                            instructions          -22.1%
+ ~Mathlib.LinearAlgebra.Alternating                                  instructions          -41.8%
+ ~Mathlib.LinearAlgebra.Basic                                        instructions          -11.7%
+ ~Mathlib.LinearAlgebra.Basis                                        instructions          -28.9%
+ ~Mathlib.LinearAlgebra.BilinearMap                                  instructions          -22.7%
+ ~Mathlib.LinearAlgebra.Determinant                                  instructions          -58.0%
+ ~Mathlib.LinearAlgebra.Dfinsupp                                     instructions          -19.7%
+ ~Mathlib.LinearAlgebra.Dimension                                    instructions          -62.7%
- ~Mathlib.LinearAlgebra.DirectSum.Finsupp                            instructions           31.1%
+ ~Mathlib.LinearAlgebra.DirectSum.TensorProduct                      instructions          -33.4%
+ ~Mathlib.LinearAlgebra.FiniteDimensional                            instructions          -69.7%
+ ~Mathlib.LinearAlgebra.Finrank                                      instructions          -54.1%
+ ~Mathlib.LinearAlgebra.Finsupp                                      instructions          -37.0%
+ ~Mathlib.LinearAlgebra.FinsuppVectorSpace                           instructions          -13.3%
+ ~Mathlib.LinearAlgebra.FreeAlgebra                                  instructions          -79.2%
+ ~Mathlib.LinearAlgebra.FreeModule.Basic                             instructions          -20.5%
+ ~Mathlib.LinearAlgebra.FreeModule.Determinant                       instructions          -22.7%
+ ~Mathlib.LinearAlgebra.FreeModule.Finite.Basic                      instructions          -20.1%
+ ~Mathlib.LinearAlgebra.FreeModule.Finite.Matrix                     instructions          -75.8%
+ ~Mathlib.LinearAlgebra.FreeModule.Finite.Rank                       instructions          -61.9%
+ ~Mathlib.LinearAlgebra.FreeModule.PID                               instructions          -31.2%
+ ~Mathlib.LinearAlgebra.FreeModule.Rank                              instructions          -51.6%
+ ~Mathlib.LinearAlgebra.InvariantBasisNumber                         instructions          -56.0%
+ ~Mathlib.LinearAlgebra.Isomorphisms                                 instructions          -81.6%
+ ~Mathlib.LinearAlgebra.LinearIndependent                            instructions          -29.1%
+ ~Mathlib.LinearAlgebra.LinearPMap                                   instructions          -10.2%
- ~Mathlib.LinearAlgebra.Matrix.AbsoluteValue                         instructions            6.7%
+ ~Mathlib.LinearAlgebra.Matrix.Adjugate                              instructions          -73.8%
+ ~Mathlib.LinearAlgebra.Matrix.Block                                 instructions          -12.3%
+ ~Mathlib.LinearAlgebra.Matrix.Circulant                             instructions           -6.6%
+ ~Mathlib.LinearAlgebra.Matrix.Determinant                           instructions           -8.9%
+ ~Mathlib.LinearAlgebra.Matrix.Diagonal                              instructions          -68.4%
+ ~Mathlib.LinearAlgebra.Matrix.FiniteDimensional                     instructions          -84.4%
+ ~Mathlib.LinearAlgebra.Matrix.MvPolynomial                          instructions          -37.0%
+ ~Mathlib.LinearAlgebra.Matrix.Nondegenerate                         instructions          -15.3%
+ ~Mathlib.LinearAlgebra.Matrix.NonsingularInverse                    instructions          -33.6%
+ ~Mathlib.LinearAlgebra.Matrix.Polynomial                            instructions          -43.8%
+ ~Mathlib.LinearAlgebra.Matrix.Reindex                               instructions          -17.9%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin                                 instructions          -43.7%
+ ~Mathlib.LinearAlgebra.Matrix.Transvection                          instructions          -30.4%
+ ~Mathlib.LinearAlgebra.Matrix.ZPow                                  instructions          -35.5%
+ ~Mathlib.LinearAlgebra.Multilinear.Basic                            instructions           -5.9%
+ ~Mathlib.LinearAlgebra.Multilinear.TensorProduct                    instructions           -7.9%
+ ~Mathlib.LinearAlgebra.Pi                                           instructions           -7.4%
+ ~Mathlib.LinearAlgebra.Prod                                         instructions          -19.7%
+ ~Mathlib.LinearAlgebra.Projection                                   instructions          -43.5%
+ ~Mathlib.LinearAlgebra.ProjectiveSpace.Basic                        instructions          -62.4%
+ ~Mathlib.LinearAlgebra.ProjectiveSpace.Independence                 instructions           -8.2%
+ ~Mathlib.LinearAlgebra.Quotient                                     instructions          -14.5%
+ ~Mathlib.LinearAlgebra.QuotientPi                                   instructions          -55.5%
+ ~Mathlib.LinearAlgebra.Ray                                          instructions          -24.7%
+ ~Mathlib.LinearAlgebra.SModEq                                       instructions           -8.3%
+ ~Mathlib.LinearAlgebra.SesquilinearForm                             instructions          -74.0%
+ ~Mathlib.LinearAlgebra.Span                                         instructions          -35.9%
+ ~Mathlib.LinearAlgebra.StdBasis                                     instructions          -34.1%
+ ~Mathlib.LinearAlgebra.SymplecticGroup                              instructions          -46.2%
+ ~Mathlib.LinearAlgebra.TensorProduct                                instructions          -15.4%
+ ~Mathlib.LinearAlgebra.TensorProductBasis                           instructions          -44.6%
+ ~Mathlib.Logic.Denumerable                                          instructions           -8.2%
+ ~Mathlib.Logic.Embedding.Basic                                      instructions           -6.8%
+ ~Mathlib.Logic.Equiv.Basic                                          instructions           -5.2%
+ ~Mathlib.Logic.Equiv.Defs                                           instructions          -11.5%
+ ~Mathlib.Logic.Equiv.Fin                                            instructions           -5.5%
+ ~Mathlib.Logic.Equiv.List                                           instructions           -8.9%
+ ~Mathlib.Logic.Equiv.TransferInstance                               instructions           -7.3%
+ ~Mathlib.Logic.Hydra                                                instructions          -11.6%
- ~Mathlib.MeasureTheory.MeasurableSpace                              instructions            8.1%
+ ~Mathlib.MeasureTheory.Measure.OuterMeasure                         instructions          -51.6%
+ ~Mathlib.ModelTheory.Encoding                                       instructions          -11.1%
+ ~Mathlib.NumberTheory.ADEInequality                                 instructions           -6.4%
+ ~Mathlib.NumberTheory.Basic                                         instructions          -42.1%
+ ~Mathlib.NumberTheory.ClassNumber.AdmissibleAbs                     instructions          -24.2%
+ ~Mathlib.NumberTheory.Fermat4                                       instructions           -7.6%
+ ~Mathlib.NumberTheory.LucasLehmer                                   instructions          -40.7%
+ ~Mathlib.NumberTheory.Padics.PadicNorm                              instructions          -14.1%
+ ~Mathlib.NumberTheory.PellMatiyasevic                               instructions           -5.2%
+ ~Mathlib.NumberTheory.Primorial                                     instructions           -6.7%
+ ~Mathlib.NumberTheory.PythagoreanTriples                            instructions          -36.8%
+ ~Mathlib.NumberTheory.Zsqrtd.Basic                                  instructions          -33.4%
- ~Mathlib.Order.Bounded                                              instructions            5.0%
+ ~Mathlib.Order.Category.DistLatCat                                  instructions          -60.5%
+ ~Mathlib.Order.Category.LatCat                                      instructions          -49.5%
+ ~Mathlib.Order.Category.LinOrdCat                                   instructions          -57.8%
+ ~Mathlib.Order.Category.NonemptyFinLinOrdCat                        instructions          -14.8%
+ ~Mathlib.Order.Category.PartOrdCat                                  instructions          -23.6%
+ ~Mathlib.Order.Category.PreordCat                                   instructions          -20.6%
+ ~Mathlib.Order.CompleteLatticeIntervals                             instructions          -14.1%
+ ~Mathlib.Order.ConditionallyCompleteLattice.Basic                   instructions           -7.7%
+ ~Mathlib.Order.Disjointed                                           instructions          -13.0%
+ ~Mathlib.Order.Filter.Archimedean                                   instructions          -10.8%
+ ~Mathlib.Order.Filter.AtTopBot                                      instructions           -5.4%
+ ~Mathlib.Order.Filter.Basic                                         instructions           -6.9%
+ ~Mathlib.Order.Filter.ENNReal                                       instructions           -5.8%
+ ~Mathlib.Order.Filter.Pi                                            instructions           -5.2%
+ ~Mathlib.Order.Filter.Pointwise                                     instructions          -17.5%
+ ~Mathlib.Order.Filter.Ultrafilter                                   instructions          -38.3%
+ ~Mathlib.Order.Filter.ZeroAndBoundedAtFilter                        instructions          -19.6%
+ ~Mathlib.Order.FixedPoints                                          instructions           -7.1%
+ ~Mathlib.Order.GaloisConnection                                     instructions           -6.1%
+ ~Mathlib.Order.Heyting.Basic                                        instructions           -7.1%
+ ~Mathlib.Order.Heyting.Hom                                          instructions           -7.4%
+ ~Mathlib.Order.Heyting.Regular                                      instructions          -13.4%
+ ~Mathlib.Order.Hom.CompleteLattice                                  instructions           -7.0%
+ ~Mathlib.Order.Hom.Lattice                                          instructions          -10.2%
+ ~Mathlib.Order.JordanHolder                                         instructions          -11.5%
+ ~Mathlib.Order.LatticeIntervals                                     instructions           -5.2%
+ ~Mathlib.Order.ModularLattice                                       instructions           -5.7%
+ ~Mathlib.Order.OmegaCompletePartialOrder                            instructions           -8.8%
+ ~Mathlib.Order.RelIso.Group                                         instructions          -40.3%
+ ~Mathlib.Order.SuccPred.IntervalSucc                                instructions          -11.1%
+ ~Mathlib.RepresentationTheory.Maschke                               instructions          -74.4%
+ ~Mathlib.RingTheory.Adjoin.Basic                                    instructions          -50.0%
+ ~Mathlib.RingTheory.Adjoin.Fg                                       instructions          -42.0%
+ ~Mathlib.RingTheory.Adjoin.Tower                                    instructions          -67.6%
+ ~Mathlib.RingTheory.AlgebraTower                                    instructions           -7.3%
+ ~Mathlib.RingTheory.ChainOfDivisors                                 instructions           -9.4%
+ ~Mathlib.RingTheory.Congruence                                      instructions           -5.2%
+ ~Mathlib.RingTheory.Coprime.Ideal                                   instructions          -21.1%
+ ~Mathlib.RingTheory.EisensteinCriterion                             instructions          -52.8%
+ ~Mathlib.RingTheory.EuclideanDomain                                 instructions          -20.4%
+ ~Mathlib.RingTheory.FiniteType                                      instructions          -78.5%
+ ~Mathlib.RingTheory.Finiteness                                      instructions          -39.3%
+ ~Mathlib.RingTheory.Flat                                            instructions          -23.3%
+ ~Mathlib.RingTheory.FreeRing                                        instructions          -13.0%
+ ~Mathlib.RingTheory.Ideal.Basic                                     instructions          -10.7%
+ ~Mathlib.RingTheory.Ideal.IdempotentFg                              instructions          -64.1%
+ ~Mathlib.RingTheory.Ideal.Operations                                instructions          -52.0%
+ ~Mathlib.RingTheory.Ideal.Prod                                      instructions          -60.4%
+ ~Mathlib.RingTheory.Ideal.Quotient                                  instructions          -43.2%
+ ~Mathlib.RingTheory.Ideal.QuotientOperations                        instructions          -25.6%
+ ~Mathlib.RingTheory.Localization.Basic                              instructions          -33.4%
+ ~Mathlib.RingTheory.Localization.FractionRing                       instructions          -55.8%
+ ~Mathlib.RingTheory.Localization.Ideal                              instructions          -15.1%
+ ~Mathlib.RingTheory.Localization.Integer                            instructions          -37.8%
+ ~Mathlib.RingTheory.Localization.InvSubmonoid                       instructions          -24.0%
+ ~Mathlib.RingTheory.Localization.Module                             instructions          -34.6%
+ ~Mathlib.RingTheory.Localization.NumDen                             instructions          -25.1%
+ ~Mathlib.RingTheory.Localization.Submodule                          instructions          -53.5%
+ ~Mathlib.RingTheory.Multiplicity                                    instructions           -6.4%
+ ~Mathlib.RingTheory.MvPolynomial.Basic                              instructions          -56.6%
+ ~Mathlib.RingTheory.MvPolynomial.Ideal                              instructions          -49.6%
+ ~Mathlib.RingTheory.MvPolynomial.Symmetric                          instructions          -33.9%
+ ~Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous                instructions          -16.6%
+ ~Mathlib.RingTheory.Nilpotent                                       instructions           -9.6%
+ ~Mathlib.RingTheory.Noetherian                                      instructions          -15.4%
+ ~Mathlib.RingTheory.OreLocalization.Basic                           instructions          -17.3%
+ ~Mathlib.RingTheory.Polynomial.Basic                                instructions          -63.4%
+ ~Mathlib.RingTheory.Polynomial.Chebyshev                            instructions          -26.0%
+ ~Mathlib.RingTheory.Polynomial.Content                              instructions          -28.2%
+ ~Mathlib.RingTheory.Polynomial.Eisenstein.Basic                     instructions          -26.6%
- ~Mathlib.RingTheory.Polynomial.Opposites                            instructions            6.0%
+ ~Mathlib.RingTheory.Polynomial.ScaleRoots                           instructions          -26.3%
+ ~Mathlib.RingTheory.Polynomial.Vieta                                instructions           -5.8%
+ ~Mathlib.RingTheory.Prime                                           instructions          -13.0%
+ ~Mathlib.RingTheory.PrincipalIdealDomain                            instructions          -45.6%
+ ~Mathlib.RingTheory.QuotientNilpotent                               instructions          -48.6%
+ ~Mathlib.RingTheory.ReesAlgebra                                     instructions          -70.7%
+ ~Mathlib.RingTheory.SimpleModule                                    instructions          -89.5%
+ ~Mathlib.RingTheory.Subring.Basic                                   instructions          -28.0%
+ ~Mathlib.RingTheory.Subring.Pointwise                               instructions          -12.0%
+ ~Mathlib.RingTheory.Subsemiring.Basic                               instructions           -5.6%
+ ~Mathlib.RingTheory.Valuation.Quotient                              instructions          -42.0%
- ~Mathlib.RingTheory.ZMod                                            instructions           10.4%
+ ~Mathlib.SetTheory.Cardinal.Cofinality                              instructions          -56.3%
+ ~Mathlib.SetTheory.Cardinal.Divisibility                            instructions           -6.3%
+ ~Mathlib.SetTheory.Ordinal.Arithmetic                               instructions          -44.2%
+ ~Mathlib.SetTheory.Ordinal.FixedPoint                               instructions          -44.6%
+ ~Mathlib.SetTheory.Ordinal.NaturalOps                               instructions           -7.6%
+ ~Mathlib.Topology.Algebra.Affine                                    instructions           -5.6%
+ ~Mathlib.Topology.Algebra.Algebra                                   instructions           -8.0%
+ ~Mathlib.Topology.Algebra.Field                                     instructions          -39.2%
+ ~Mathlib.Topology.Algebra.Group.Basic                               instructions          -10.4%
+ ~Mathlib.Topology.Algebra.GroupCompletion                           instructions           -8.7%
+ ~Mathlib.Topology.Algebra.GroupWithZero                             instructions          -12.7%
+ ~Mathlib.Topology.Algebra.InfiniteSum.Real                          instructions           -7.2%
+ ~Mathlib.Topology.Algebra.Localization                              instructions          -15.1%
+ ~Mathlib.Topology.Algebra.Module.Basic                              instructions          -54.6%
+ ~Mathlib.Topology.Algebra.Module.Determinant                        instructions          -63.1%
+ ~Mathlib.Topology.Algebra.Module.LinearPMap                         instructions           -6.6%
+ ~Mathlib.Topology.Algebra.Module.Multilinear                        instructions          -19.4%
+ ~Mathlib.Topology.Algebra.Module.Simple                             instructions          -21.9%
+ ~Mathlib.Topology.Algebra.Module.StrongTopology                     instructions          -74.4%
+ ~Mathlib.Topology.Algebra.Module.WeakDual                           instructions          -51.4%
+ ~Mathlib.Topology.Algebra.Nonarchimedean.Bases                      instructions          -11.4%
+ ~Mathlib.Topology.Algebra.Nonarchimedean.Basic                      instructions          -11.5%
+ ~Mathlib.Topology.Algebra.Order.Compact                             instructions           -6.2%
+ ~Mathlib.Topology.Algebra.Order.Field                               instructions          -10.8%
+ ~Mathlib.Topology.Algebra.Order.Floor                               instructions           -5.6%
+ ~Mathlib.Topology.Algebra.Order.IntermediateValue                   instructions          -16.3%
+ ~Mathlib.Topology.Algebra.Order.LeftRightLim                        instructions           -6.3%
+ ~Mathlib.Topology.Algebra.Order.LiminfLimsup                        instructions           -6.4%
+ ~Mathlib.Topology.Algebra.Polynomial                                instructions          -45.1%
+ ~Mathlib.Topology.Algebra.Ring.Basic                                instructions          -34.6%
+ ~Mathlib.Topology.Algebra.StarSubalgebra                            instructions          -57.4%
+ ~Mathlib.Topology.Algebra.UniformConvergence                        instructions          -22.7%
+ ~Mathlib.Topology.Algebra.UniformField                              instructions          -36.7%
+ ~Mathlib.Topology.Algebra.UniformGroup                              instructions           -5.8%
+ ~Mathlib.Topology.Algebra.UniformRing                               instructions          -17.9%
+ ~Mathlib.Topology.Basic                                             instructions           -6.2%
+ ~Mathlib.Topology.Category.CompHaus.Basic                           instructions          -11.2%
+ ~Mathlib.Topology.Category.Profinite.Basic                          instructions          -15.6%
+ ~Mathlib.Topology.Category.Top.Adjunctions                          instructions          -26.8%
- ~Mathlib.Topology.ContinuousFunction.T0Sierpinski                   instructions            7.5%
+ ~Mathlib.Topology.Filter                                            instructions           -6.1%
+ ~Mathlib.Topology.Homotopy.Equiv                                    instructions          -10.7%
+ ~Mathlib.Topology.Instances.ENNReal                                 instructions          -34.9%
+ ~Mathlib.Topology.Instances.EReal                                   instructions          -10.8%
+ ~Mathlib.Topology.Instances.Matrix                                  instructions          -22.5%
+ ~Mathlib.Topology.Instances.NNReal                                  instructions          -28.3%
+ ~Mathlib.Topology.Instances.Nat                                     instructions          -17.6%
+ ~Mathlib.Topology.Instances.Rat                                     instructions           -5.5%
+ ~Mathlib.Topology.Instances.Real                                    instructions          -13.0%
+ ~Mathlib.Topology.Instances.RealVectorSpace                         instructions          -17.2%
+ ~Mathlib.Topology.Instances.TrivSqZeroExt                           instructions           -7.6%
+ ~Mathlib.Topology.LocalHomeomorph                                   instructions          -38.2%
+ ~Mathlib.Topology.LocallyConstant.Algebra                           instructions           -6.1%
+ ~Mathlib.Topology.MetricSpace.Algebra                               instructions          -15.9%
- ~Mathlib.Topology.MetricSpace.CantorScheme                          instructions            5.9%
+ ~Mathlib.Topology.MetricSpace.CauSeqFilter                          instructions          -12.6%
+ ~Mathlib.Topology.MetricSpace.Completion                            instructions           -6.6%
+ ~Mathlib.Topology.MetricSpace.EMetricSpace                          instructions           -5.6%
+ ~Mathlib.Topology.MetricSpace.HausdorffDistance                     instructions          -11.8%
+ ~Mathlib.Topology.MetricSpace.Infsep                                instructions           -7.6%
+ ~Mathlib.Topology.MetricSpace.Isometry                              instructions           -9.0%
+ ~Mathlib.Topology.MetricSpace.Lipschitz                             instructions           -7.9%
+ ~Mathlib.Topology.MetricSpace.PiNat                                 instructions          -32.7%
- ~Mathlib.Topology.OmegaCompletePartialOrder                         instructions            7.3%
+ ~Mathlib.Topology.Order                                             instructions          -12.8%
+ ~Mathlib.Topology.PathConnected                                     instructions           -8.3%
+ ~Mathlib.Topology.Separation                                        instructions           -8.3%
+ ~Mathlib.Topology.Sequences                                         instructions           -5.7%
+ ~Mathlib.Topology.Sets.Closeds                                      instructions          -61.9%
- ~Mathlib.Topology.Sets.Compacts                                     instructions           10.0%
+ ~Mathlib.Topology.Sets.Opens                                        instructions           -7.3%
+ ~Mathlib.Topology.StoneCech                                         instructions          -11.6%
+ ~Mathlib.Topology.UniformSpace.AbsoluteValue                        instructions          -12.7%
+ ~Mathlib.Topology.UniformSpace.CompareReals                         instructions          -18.9%
+ ~Mathlib.Topology.UniformSpace.Completion                           instructions          -19.3%
+ ~Mathlib.Topology.UniformSpace.Pi                                   instructions           -9.2%
+ ~Mathlib.Topology.UniformSpace.Separation                           instructions           -7.6%
+ ~Mathlib.Topology.UniformSpace.UniformConvergenceTopology           instructions          -34.4%
+ ~Mathlib.Topology.UrysohnsLemma                                     instructions          -37.3%
- ~Mathlib.Util.Qq                                                    instructions            9.9%
- ~Mathlib.Util.SynthesizeUsing                                       instructions           34.9%

There were significant changes against commit c5372bb:

  Benchmark                                                     Metric                  Change
  ============================================================================================
- build                                                         .olean serialization     17.1%
- build                                                         branch-misses             8.8%
- build                                                         compilation              19.9%
- build                                                         compilation new          13.3%
+ build                                                         elaboration             -22.9%
- build                                                         import                   22.8%
- build                                                         initialization           15.2%
+ build                                                         interpretation          -11.4%
- build                                                         linting                  35.5%
- build                                                         maxrss                   12.1%
- build                                                         parsing                  13.3%
+ build                                                         simp                     -5.0%
+ build                                                         tactic execution        -40.6%
- build                                                         type checking            38.3%
- build                                                         typeclass inference      26.8%
+ lint                                                          instructions            -15.7%
+ lint                                                          wall-clock              -18.9%
- size                                                          .lean                    13.0%
- size                                                          .olean                   17.1%
- ~Aesop.Builder.Apply                                          instructions             11.6%
- ~Aesop.Builder.Cases                                          instructions              6.5%
- ~Aesop.Builder.Constructors                                   instructions             12.3%
- ~Aesop.Builder.Forward                                        instructions             13.9%
- ~Aesop.BuiltinRules.ApplyHyps                                 instructions             19.9%
- ~Aesop.BuiltinRules.Assumption                                instructions             10.6%
- ~Aesop.BuiltinRules.DestructProducts                          instructions              8.8%
- ~Aesop.BuiltinRules.Intros                                    instructions             14.0%
+ ~Aesop.Frontend.Command                                       instructions            -19.3%
- ~Aesop.Index                                                  instructions              7.8%
+ ~Aesop.Main                                                   instructions            -22.0%
+ ~Aesop.Options                                                instructions            -80.4%
- ~Aesop.Rule.Name                                              instructions             13.3%
- ~Aesop.RuleTac.Apply                                          instructions              9.7%
+ ~Aesop.RuleTac.Basic                                          instructions            -11.4%
- ~Aesop.RuleTac.Forward                                        instructions             10.2%
+ ~Aesop.RuleTac.Tactic                                         instructions             -7.1%
- ~Aesop.Script                                                 instructions              5.1%
+ ~Aesop.Search.ExpandSafePrefix                                instructions             -8.2%
+ ~Aesop.Search.Expansion                                       instructions            -53.9%
+ ~Aesop.Search.Main                                            instructions             -7.3%
+ ~Aesop.Search.Queue                                           instructions            -16.1%
+ ~Aesop.Search.RuleSelection                                   instructions            -41.8%
- ~Aesop.Tracing                                                instructions            103.5%
- ~Aesop.Tree.ExtractScript                                     instructions             21.1%
- ~Aesop.Util.Basic                                             instructions             25.1%
- ~Mathlib                                                      instructions             12.5%
+ ~Mathlib.Algebra.Algebra.Basic                                instructions            -10.0%
+ ~Mathlib.Algebra.Algebra.Bilinear                             instructions            -23.9%
- ~Mathlib.Algebra.Algebra.Equiv                                instructions              8.5%
- ~Mathlib.Algebra.Algebra.Hom                                  instructions             41.1%
+ ~Mathlib.Algebra.Algebra.Operations                           instructions            -42.2%
+ ~Mathlib.Algebra.Algebra.Pi                                   instructions            -22.2%
+ ~Mathlib.Algebra.Algebra.RestrictScalars                      instructions            -11.4%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Basic                     instructions            -15.4%
- ~Mathlib.Algebra.Algebra.Subalgebra.Pointwise                 instructions             95.2%
- ~Mathlib.Algebra.Algebra.Subalgebra.Tower                     instructions              9.3%
- ~Mathlib.Algebra.Algebra.Tower                                instructions             23.0%
+ ~Mathlib.Algebra.Algebra.Unitization                          instructions            -10.4%
+ ~Mathlib.Algebra.BigOperators.Associated                      instructions            -45.7%
- ~Mathlib.Algebra.BigOperators.Basic                           instructions             10.0%
- ~Mathlib.Algebra.BigOperators.Fin                             instructions             59.8%
+ ~Mathlib.Algebra.BigOperators.Finprod                         instructions            -17.1%
+ ~Mathlib.Algebra.BigOperators.Finsupp                         instructions             -7.3%
+ ~Mathlib.Algebra.BigOperators.Multiset.Basic                  instructions            -11.4%
- ~Mathlib.Algebra.BigOperators.Option                          instructions              6.0%
+ ~Mathlib.Algebra.BigOperators.Order                           instructions             -7.0%
- ~Mathlib.Algebra.BigOperators.RingEquiv                       instructions             95.2%
+ ~Mathlib.Algebra.Category.GroupCat.Basic                      instructions            -26.8%
+ ~Mathlib.Algebra.Category.GroupCat.Zero                       instructions             -5.6%
+ ~Mathlib.Algebra.Category.MonCat.Basic                        instructions            -12.8%
+ ~Mathlib.Algebra.CharP.Algebra                                instructions            -24.6%
+ ~Mathlib.Algebra.CharP.Quotient                               instructions            -18.9%
+ ~Mathlib.Algebra.CharZero.Quotient                            instructions            -24.6%
+ ~Mathlib.Algebra.CovariantAndContravariant                    instructions            -13.5%
+ ~Mathlib.Algebra.CubicDiscriminant                            instructions            -61.5%
+ ~Mathlib.Algebra.DirectSum.Finsupp                            instructions            -20.6%
+ ~Mathlib.Algebra.DirectSum.Module                             instructions            -35.5%
+ ~Mathlib.Algebra.DualNumber                                   instructions            -17.5%
+ ~Mathlib.Algebra.Free                                         instructions            -54.5%
+ ~Mathlib.Algebra.FreeMonoid.Basic                             instructions            -15.1%
+ ~Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra                 instructions            -24.6%
+ ~Mathlib.Algebra.GCDMonoid.Div                                instructions            -60.9%
+ ~Mathlib.Algebra.GeomSum                                      instructions            -28.7%
+ ~Mathlib.Algebra.Group.Basic                                  instructions            -34.0%
+ ~Mathlib.Algebra.Group.Commute                                instructions            -20.3%
+ ~Mathlib.Algebra.Group.Conj                                   instructions            -11.0%
+ ~Mathlib.Algebra.Group.Defs                                   instructions            -12.4%
+ ~Mathlib.Algebra.Group.Ext                                    instructions            -20.3%
+ ~Mathlib.Algebra.Group.InjSurj                                instructions            -33.3%
+ ~Mathlib.Algebra.Group.Opposite                               instructions            -41.7%
+ ~Mathlib.Algebra.Group.Pi                                     instructions            -10.6%
+ ~Mathlib.Algebra.Group.Prod                                   instructions            -41.7%
+ ~Mathlib.Algebra.Group.Semiconj                               instructions            -30.7%
- ~Mathlib.Algebra.Group.UniqueProds                            instructions             12.2%
+ ~Mathlib.Algebra.Group.Units                                  instructions            -25.7%
+ ~Mathlib.Algebra.Group.WithOne.Basic                          instructions            -65.7%
+ ~Mathlib.Algebra.Group.WithOne.Units                          instructions             -6.3%
+ ~Mathlib.Algebra.GroupPower.Identities                        instructions             -7.8%
+ ~Mathlib.Algebra.GroupRingAction.Invariant                    instructions            -47.6%
- ~Mathlib.Algebra.GroupWithZero.Divisibility                   instructions             15.5%
+ ~Mathlib.Algebra.Hom.Centroid                                 instructions            -19.4%
+ ~Mathlib.Algebra.Hom.Equiv.Basic                              instructions            -27.0%
+ ~Mathlib.Algebra.Hom.Equiv.Units.Basic                        instructions            -10.4%
+ ~Mathlib.Algebra.Hom.Freiman                                  instructions            -20.3%
+ ~Mathlib.Algebra.Hom.Group                                    instructions            -22.1%
+ ~Mathlib.Algebra.Hom.GroupInstances                           instructions            -47.3%
+ ~Mathlib.Algebra.Hom.Units                                    instructions            -32.8%
+ ~Mathlib.Algebra.IndicatorFunction                            instructions            -12.9%
- ~Mathlib.Algebra.Invertible                                   instructions              7.2%
- ~Mathlib.Algebra.IsPrimePow                                   instructions             30.7%
+ ~Mathlib.Algebra.Lie.Basic                                    instructions            -20.0%
+ ~Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra                 instructions             -5.2%
+ ~Mathlib.Algebra.Lie.Subalgebra                               instructions            -38.1%
+ ~Mathlib.Algebra.Module.Algebra                               instructions            -13.8%
- ~Mathlib.Algebra.Module.BigOperators                          instructions             29.3%
+ ~Mathlib.Algebra.Module.Equiv                                 instructions             -7.1%
+ ~Mathlib.Algebra.Module.LinearMap                             instructions             -7.6%
+ ~Mathlib.Algebra.Module.Pi                                    instructions            -10.9%
+ ~Mathlib.Algebra.Module.Projective                            instructions            -31.7%
+ ~Mathlib.Algebra.Module.Submodule.Pointwise                   instructions             -5.2%
+ ~Mathlib.Algebra.Module.ULift                                 instructions            -16.7%
+ ~Mathlib.Algebra.MonoidAlgebra.Basic                          instructions            -31.6%
+ ~Mathlib.Algebra.MonoidAlgebra.Division                       instructions            -47.7%
+ ~Mathlib.Algebra.MonoidAlgebra.Support                        instructions            -18.5%
+ ~Mathlib.Algebra.Order.AbsoluteValue                          instructions            -16.2%
- ~Mathlib.Algebra.Order.Algebra                                instructions              5.4%
+ ~Mathlib.Algebra.Order.Archimedean                            instructions            -15.9%
+ ~Mathlib.Algebra.Order.Field.Power                            instructions             -5.8%
+ ~Mathlib.Algebra.Order.Floor                                  instructions             -9.0%
+ ~Mathlib.Algebra.Order.Group.Defs                             instructions            -35.3%
+ ~Mathlib.Algebra.Order.Group.DenselyOrdered                   instructions             -5.4%
+ ~Mathlib.Algebra.Order.Group.MinMax                           instructions            -12.7%
+ ~Mathlib.Algebra.Order.Group.OrderIso                         instructions             -8.5%
+ ~Mathlib.Algebra.Order.Hom.Basic                              instructions            -12.4%
+ ~Mathlib.Algebra.Order.Hom.Monoid                             instructions            -11.4%
+ ~Mathlib.Algebra.Order.Kleene                                 instructions             -5.6%
+ ~Mathlib.Algebra.Order.LatticeGroup                           instructions            -61.5%
+ ~Mathlib.Algebra.Order.Module                                 instructions            -17.5%
+ ~Mathlib.Algebra.Order.Monoid.Canonical.Defs                  instructions            -15.4%
+ ~Mathlib.Algebra.Order.Monoid.Lemmas                          instructions             -6.7%
+ ~Mathlib.Algebra.Order.Monoid.MinMax                          instructions            -11.0%
+ ~Mathlib.Algebra.Order.Monoid.Prod                            instructions             -7.3%
+ ~Mathlib.Algebra.Order.Monoid.ToMulBot                        instructions             -5.6%
+ ~Mathlib.Algebra.Order.Nonneg.Field                           instructions            -23.7%
+ ~Mathlib.Algebra.Order.Nonneg.Ring                            instructions             -5.1%
+ ~Mathlib.Algebra.Order.Positive.Field                         instructions             -5.3%
- ~Mathlib.Algebra.Order.Rearrangement                          instructions             35.1%
+ ~Mathlib.Algebra.Order.Ring.Abs                               instructions             -9.0%
+ ~Mathlib.Algebra.Order.Ring.Cone                              instructions             -5.5%
+ ~Mathlib.Algebra.Order.Ring.Defs                              instructions            -12.7%
+ ~Mathlib.Algebra.Order.Ring.WithTop                           instructions             -8.7%
+ ~Mathlib.Algebra.Order.SMul                                   instructions             -8.3%
+ ~Mathlib.Algebra.Order.UpperLower                             instructions            -19.8%
+ ~Mathlib.Algebra.Order.WithZero                               instructions            -16.7%
+ ~Mathlib.Algebra.PUnitInstances                               instructions             -5.6%
+ ~Mathlib.Algebra.Polynomial.BigOperators                      instructions             -8.7%
+ ~Mathlib.Algebra.Polynomial.GroupRingAction                   instructions            -26.0%
+ ~Mathlib.Algebra.QuadraticDiscriminant                        instructions            -36.4%
+ ~Mathlib.Algebra.Quandle                                      instructions            -20.5%
+ ~Mathlib.Algebra.Ring.AddAut                                  instructions             -9.9%
+ ~Mathlib.Algebra.Ring.Aut                                     instructions            -12.6%
+ ~Mathlib.Algebra.Ring.CompTypeclasses                         instructions             -8.2%
+ ~Mathlib.Algebra.Ring.Divisibility                            instructions             -5.2%
+ ~Mathlib.Algebra.Ring.Equiv                                   instructions             -8.0%
+ ~Mathlib.Algebra.Ring.Opposite                                instructions            -15.3%
+ ~Mathlib.Algebra.Ring.Prod                                    instructions            -10.3%
+ ~Mathlib.Algebra.Star.CHSH                                    instructions            -67.8%
+ ~Mathlib.Algebra.Star.Free                                    instructions             -7.0%
+ ~Mathlib.Algebra.Star.Module                                  instructions            -33.1%
+ ~Mathlib.Algebra.Star.SelfAdjoint                             instructions            -20.0%
- ~Mathlib.Algebra.Star.StarAlgHom                              instructions             26.7%
+ ~Mathlib.Algebra.Star.Subalgebra                              instructions             -7.4%
+ ~Mathlib.Algebra.TrivSqZeroExt                                instructions            -23.1%
- ~Mathlib.Algebra.Tropical.Basic                               instructions              5.6%
+ ~Mathlib.Algebra.Tropical.Lattice                             instructions             -6.2%
+ ~Mathlib.AlgebraicTopology.DoldKan.Compatibility              instructions            -44.0%
- ~Mathlib.AlgebraicTopology.SimplexCategory                    instructions              7.0%
- ~Mathlib.Analysis.Convex.Extreme                              instructions             13.5%
+ ~Mathlib.Analysis.Convex.Function                             instructions            -10.1%
+ ~Mathlib.Analysis.Convex.Segment                              instructions             -5.2%
+ ~Mathlib.Analysis.Convex.Strict                               instructions             -5.1%
+ ~Mathlib.Analysis.Hofer                                       instructions             -7.1%
+ ~Mathlib.Analysis.LocallyConvex.Polar                         instructions            -75.3%
+ ~Mathlib.Analysis.Normed.Field.Basic                          instructions            -17.8%
+ ~Mathlib.Analysis.Normed.Field.InfiniteSum                    instructions            -16.5%
+ ~Mathlib.Analysis.Normed.Group.Basic                          instructions            -10.9%
+ ~Mathlib.Analysis.Normed.Group.Hom                            instructions            -12.9%
+ ~Mathlib.Analysis.Normed.Group.HomCompletion                  instructions            -49.4%
+ ~Mathlib.Analysis.Normed.Group.InfiniteSum                    instructions             -6.2%
+ ~Mathlib.Analysis.Normed.Group.Pointwise                      instructions            -16.1%
+ ~Mathlib.Analysis.SpecificLimits.Basic                        instructions            -19.4%
+ ~Mathlib.CategoryTheory.Abelian.Basic                         instructions            -10.6%
+ ~Mathlib.CategoryTheory.Abelian.FunctorCategory               instructions            -40.9%
+ ~Mathlib.CategoryTheory.Adjunction.Evaluation                 instructions             -5.6%
+ ~Mathlib.CategoryTheory.Adjunction.FullyFaithful              instructions            -14.2%
+ ~Mathlib.CategoryTheory.Adjunction.Limits                     instructions            -32.1%
+ ~Mathlib.CategoryTheory.Adjunction.Mates                      instructions             -5.1%
+ ~Mathlib.CategoryTheory.Adjunction.Whiskering                 instructions            -62.6%
+ ~Mathlib.CategoryTheory.Category.Bipointed                    instructions            -12.9%
+ ~Mathlib.CategoryTheory.Category.Cat                          instructions            -51.7%
+ ~Mathlib.CategoryTheory.Category.QuivCat                      instructions             -6.7%
+ ~Mathlib.CategoryTheory.Category.TwoP                         instructions            -28.9%
+ ~Mathlib.CategoryTheory.Elements                              instructions            -44.4%
+ ~Mathlib.CategoryTheory.Equivalence                           instructions             -5.6%
+ ~Mathlib.CategoryTheory.EssentialImage                        instructions             -6.6%
+ ~Mathlib.CategoryTheory.FinCategory                           instructions            -28.7%
+ ~Mathlib.CategoryTheory.FintypeCat                            instructions             -8.5%
+ ~Mathlib.CategoryTheory.Functor.Currying                      instructions            -17.2%
+ ~Mathlib.CategoryTheory.Functor.InvIsos                       instructions             -6.4%
+ ~Mathlib.CategoryTheory.Grothendieck                          instructions            -34.0%
+ ~Mathlib.CategoryTheory.Idempotents.FunctorCategories         instructions            -11.7%
+ ~Mathlib.CategoryTheory.Idempotents.FunctorExtension          instructions            -75.5%
+ ~Mathlib.CategoryTheory.Idempotents.Karoubi                   instructions             -6.3%
+ ~Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi            instructions            -23.6%
+ ~Mathlib.CategoryTheory.Limits.ColimitLimit                   instructions            -41.4%
+ ~Mathlib.CategoryTheory.Limits.Comma                          instructions            -34.7%
+ ~Mathlib.CategoryTheory.Limits.Cones                          instructions            -10.2%
- ~Mathlib.CategoryTheory.Limits.Constructions.EpiMono          instructions              5.3%
+ ~Mathlib.CategoryTheory.Limits.Constructions.Over.Connected   instructions             -6.8%
+ ~Mathlib.CategoryTheory.Limits.Creates                        instructions             -5.0%
+ ~Mathlib.CategoryTheory.Limits.ExactFunctor                   instructions            -11.2%
+ ~Mathlib.CategoryTheory.Limits.FunctorCategory                instructions            -18.6%
+ ~Mathlib.CategoryTheory.Limits.HasLimits                      instructions            -13.3%
+ ~Mathlib.CategoryTheory.Limits.KanExtension                   instructions            -36.0%
+ ~Mathlib.CategoryTheory.Limits.Lattice                        instructions             -9.0%
+ ~Mathlib.CategoryTheory.Limits.Opposites                      instructions            -16.3%
+ ~Mathlib.CategoryTheory.Limits.Preserves.Basic                instructions            -19.6%
+ ~Mathlib.CategoryTheory.Limits.Preserves.Limits               instructions             -6.4%
+ ~Mathlib.CategoryTheory.Limits.Preserves.Opposites            instructions            -23.1%
+ ~Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer          instructions             -5.7%
+ ~Mathlib.CategoryTheory.Limits.Shapes.Products                instructions             -5.2%
+ ~Mathlib.CategoryTheory.Limits.Shapes.Types                   instructions             -5.2%
+ ~Mathlib.CategoryTheory.Linear.Basic                          instructions            -75.1%
+ ~Mathlib.CategoryTheory.Localization.Construction             instructions            -50.9%
+ ~Mathlib.CategoryTheory.Localization.Opposite                 instructions            -36.0%
+ ~Mathlib.CategoryTheory.Localization.Predicate                instructions            -24.5%
+ ~Mathlib.CategoryTheory.Monoidal.Discrete                     instructions            -75.8%
+ ~Mathlib.CategoryTheory.Monoidal.Functor                      instructions             -7.7%
- ~Mathlib.CategoryTheory.Monoidal.Linear                       instructions             37.6%
+ ~Mathlib.CategoryTheory.Monoidal.NaturalTransformation        instructions             -8.0%
- ~Mathlib.CategoryTheory.Monoidal.Preadditive                  instructions             77.2%
+ ~Mathlib.CategoryTheory.Monoidal.Transport                    instructions            -12.6%
+ ~Mathlib.CategoryTheory.Opposites                             instructions            -19.1%
+ ~Mathlib.CategoryTheory.Over                                  instructions             -6.5%
+ ~Mathlib.CategoryTheory.PEmpty                                instructions             -5.2%
+ ~Mathlib.CategoryTheory.Preadditive.AdditiveFunctor           instructions             -5.5%
- ~Mathlib.CategoryTheory.Preadditive.FunctorCategory           instructions              6.1%
+ ~Mathlib.CategoryTheory.Products.Basic                        instructions             -8.9%
+ ~Mathlib.CategoryTheory.Sigma.Basic                           instructions            -15.8%
+ ~Mathlib.CategoryTheory.SingleObj                             instructions            -22.7%
+ ~Mathlib.CategoryTheory.Sites.Plus                            instructions            -45.7%
+ ~Mathlib.CategoryTheory.Sites.Sheaf                           instructions             -9.8%
+ ~Mathlib.CategoryTheory.Skeletal                              instructions             -6.4%
+ ~Mathlib.CategoryTheory.StructuredArrow                       instructions            -10.1%
+ ~Mathlib.CategoryTheory.Whiskering                            instructions            -23.9%
+ ~Mathlib.CategoryTheory.Yoneda                                instructions            -31.8%
+ ~Mathlib.Combinatorics.Additive.Energy                        instructions             -8.6%
+ ~Mathlib.Combinatorics.Additive.Etransform                    instructions            -32.8%
+ ~Mathlib.Combinatorics.Additive.PluenneckeRuzsa               instructions            -11.2%
+ ~Mathlib.Combinatorics.Additive.RuzsaCovering                 instructions            -30.6%
+ ~Mathlib.Combinatorics.Catalan                                instructions            -57.0%
- ~Mathlib.Combinatorics.Composition                            instructions             10.7%
- ~Mathlib.Combinatorics.Derangements.Basic                     instructions             25.5%
- ~Mathlib.Combinatorics.HalesJewett                            instructions              8.4%
+ ~Mathlib.Combinatorics.Hindman                                instructions            -11.5%
+ ~Mathlib.Combinatorics.SetFamily.Compression.UV               instructions             -6.8%
+ ~Mathlib.Combinatorics.SetFamily.Kleitman                     instructions            -16.0%
+ ~Mathlib.Combinatorics.SetFamily.LYM                          instructions             -7.6%
- ~Mathlib.Combinatorics.SimpleGraph.Basic                      instructions             31.0%
- ~Mathlib.Combinatorics.SimpleGraph.Clique                     instructions              6.6%
- ~Mathlib.Combinatorics.SimpleGraph.Coloring                   instructions             70.3%
- ~Mathlib.Combinatorics.SimpleGraph.Connectivity               instructions             25.9%
+ ~Mathlib.Combinatorics.SimpleGraph.Density                    instructions             -9.6%
+ ~Mathlib.Combinatorics.SimpleGraph.Matching                   instructions            -14.5%
- ~Mathlib.Combinatorics.SimpleGraph.Prod                       instructions             16.3%
+ ~Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform         instructions             -5.2%
- ~Mathlib.Combinatorics.SimpleGraph.Subgraph                   instructions              6.1%
- ~Mathlib.Combinatorics.SimpleGraph.Trails                     instructions              5.4%
- ~Mathlib.Combinatorics.SimpleGraph.Triangle.Basic             instructions             14.4%
- ~Mathlib.Combinatorics.Young.YoungDiagram                     instructions              6.9%
+ ~Mathlib.Control.LawfulFix                                    instructions            -29.4%
- ~Mathlib.Data.Array.Defs                                      instructions             14.1%
+ ~Mathlib.Data.Complex.Basic                                   instructions            -46.4%
+ ~Mathlib.Data.Complex.Exponential                             instructions            -25.6%
+ ~Mathlib.Data.Dfinsupp.Basic                                  instructions             -8.7%
+ ~Mathlib.Data.Dfinsupp.Lex                                    instructions             -8.7%
- ~Mathlib.Data.Dfinsupp.Multiset                               instructions             37.4%
+ ~Mathlib.Data.Dfinsupp.NeLocus                                instructions            -12.1%
- ~Mathlib.Data.Dfinsupp.Order                                  instructions             15.6%
- ~Mathlib.Data.Fin.Basic                                       instructions             19.1%
- ~Mathlib.Data.Fin.Tuple.Basic                                 instructions             28.0%
+ ~Mathlib.Data.Fin.Tuple.BubbleSortInduction                   instructions            -16.1%
- ~Mathlib.Data.Fin.Tuple.NatAntidiagonal                       instructions              6.8%
- ~Mathlib.Data.Fin.VecNotation                                 instructions             11.2%
- ~Mathlib.Data.FinEnum                                         instructions              5.2%
- ~Mathlib.Data.Finite.Basic                                    instructions             16.6%
- ~Mathlib.Data.Finmap                                          instructions             42.8%
- ~Mathlib.Data.Finset.Basic                                    instructions              6.3%
- ~Mathlib.Data.Finset.Finsupp                                  instructions             15.0%
- ~Mathlib.Data.Finset.Lattice                                  instructions              5.3%
+ ~Mathlib.Data.Finset.MulAntidiagonal                          instructions            -13.7%
- ~Mathlib.Data.Finset.NAry                                     instructions             11.1%
+ ~Mathlib.Data.Finset.NoncommProd                              instructions            -43.2%
+ ~Mathlib.Data.Finset.Pi                                       instructions            -19.2%
- ~Mathlib.Data.Finset.Pointwise                                instructions             15.3%
- ~Mathlib.Data.Finset.Powerset                                 instructions             17.6%
- ~Mathlib.Data.Finset.Preimage                                 instructions              9.0%
- ~Mathlib.Data.Finset.Sort                                     instructions             12.0%
- ~Mathlib.Data.Finset.Sups                                     instructions             13.7%
+ ~Mathlib.Data.Finset.Sym                                      instructions             -6.5%
+ ~Mathlib.Data.Finsupp.Antidiagonal                            instructions            -41.3%
+ ~Mathlib.Data.Finsupp.Basic                                   instructions            -13.2%
- ~Mathlib.Data.Finsupp.Defs                                    instructions             25.5%
+ ~Mathlib.Data.Finsupp.Multiset                                instructions            -56.0%
+ ~Mathlib.Data.Finsupp.NeLocus                                 instructions            -14.1%
- ~Mathlib.Data.Finsupp.Order                                   instructions             25.1%
+ ~Mathlib.Data.Finsupp.ToDfinsupp                              instructions            -14.6%
+ ~Mathlib.Data.Fintype.Basic                                   instructions             -7.3%
+ ~Mathlib.Data.Fintype.BigOperators                            instructions             -6.6%
- ~Mathlib.Data.Fintype.CardEmbedding                           instructions              7.3%
- ~Mathlib.Data.Fintype.Order                                   instructions             46.9%
+ ~Mathlib.Data.Fintype.Powerset                                instructions            -21.4%
- ~Mathlib.Data.Fintype.Sort                                    instructions              5.5%
+ ~Mathlib.Data.Int.AbsoluteValue                               instructions            -43.8%
+ ~Mathlib.Data.Int.Cast.Prod                                   instructions             -6.0%
- ~Mathlib.Data.Int.ConditionallyCompleteOrder                  instructions             16.6%
+ ~Mathlib.Data.Int.Dvd.Basic                                   instructions             -8.5%
+ ~Mathlib.Data.Int.Log                                         instructions            -39.0%
+ ~Mathlib.Data.List.BigOperators.Basic                         instructions            -23.5%
+ ~Mathlib.Data.List.BigOperators.Lemmas                        instructions             -8.0%
+ ~Mathlib.Data.List.Cycle                                      instructions            -12.1%
+ ~Mathlib.Data.List.Zip                                        instructions             -8.0%
+ ~Mathlib.Data.Matrix.Basic                                    instructions             -5.8%
+ ~Mathlib.Data.Matrix.DualNumber                               instructions            -22.2%
- ~Mathlib.Data.Multiset.Fintype                                instructions             13.6%
- ~Mathlib.Data.Multiset.Functor                                instructions              5.0%
- ~Mathlib.Data.Multiset.Interval                               instructions             20.4%
- ~Mathlib.Data.Multiset.LocallyFinite                          instructions             24.7%
+ ~Mathlib.Data.MvPolynomial.Basic                              instructions            -16.9%
+ ~Mathlib.Data.MvPolynomial.CommRing                           instructions            -50.9%
- ~Mathlib.Data.MvPolynomial.Division                           instructions              6.3%
+ ~Mathlib.Data.MvPolynomial.Equiv                              instructions            -58.4%
+ ~Mathlib.Data.MvPolynomial.Expand                             instructions            -33.6%
+ ~Mathlib.Data.MvPolynomial.Monad                              instructions            -28.7%
+ ~Mathlib.Data.MvPolynomial.Rename                             instructions            -27.8%
+ ~Mathlib.Data.MvPolynomial.Supported                          instructions            -53.3%
+ ~Mathlib.Data.MvPolynomial.Variables                          instructions            -13.3%
- ~Mathlib.Data.Nat.Bitwise                                     instructions              6.5%
+ ~Mathlib.Data.Nat.Choose.Bounds                               instructions             -5.2%
- ~Mathlib.Data.Nat.Choose.Multinomial                          instructions              5.0%
- ~Mathlib.Data.Nat.Choose.Sum                                  instructions             33.4%
- ~Mathlib.Data.Nat.Count                                       instructions             12.3%
- ~Mathlib.Data.Nat.Digits                                      instructions             10.2%
+ ~Mathlib.Data.Nat.Factorization.Basic                         instructions            -19.8%
+ ~Mathlib.Data.Nat.Fib                                         instructions             -8.8%
+ ~Mathlib.Data.Nat.Order.Basic                                 instructions            -12.2%
+ ~Mathlib.Data.Nat.PSub                                        instructions             -6.5%
- ~Mathlib.Data.Nat.PartENat                                    instructions             15.4%
- ~Mathlib.Data.Nat.Periodic                                    instructions             11.0%
+ ~Mathlib.Data.Nat.Totient                                     instructions             -8.8%
- ~Mathlib.Data.PFunctor.Multivariate.Basic                     instructions              6.7%
- ~Mathlib.Data.PFunctor.Multivariate.M                         instructions             31.8%
- ~Mathlib.Data.PFunctor.Multivariate.W                         instructions             13.0%
- ~Mathlib.Data.PFunctor.Univariate.M                           instructions              7.2%
- ~Mathlib.Data.PNat.Find                                       instructions              5.2%
+ ~Mathlib.Data.PNat.Interval                                   instructions             -6.3%
+ ~Mathlib.Data.Pi.Algebra                                      instructions            -10.2%
+ ~Mathlib.Data.Pi.Interval                                     instructions             -8.3%
- ~Mathlib.Data.Polynomial.Basic                                instructions             21.3%
- ~Mathlib.Data.Polynomial.CancelLeads                          instructions             19.5%
- ~Mathlib.Data.Polynomial.Coeff                                instructions             27.1%
+ ~Mathlib.Data.Polynomial.Degree.CardPowDegree                 instructions            -52.0%
- ~Mathlib.Data.Polynomial.Degree.Definitions                   instructions             48.6%
- ~Mathlib.Data.Polynomial.Degree.Lemmas                        instructions             36.2%
- ~Mathlib.Data.Polynomial.Degree.TrailingDegree                instructions             11.9%
+ ~Mathlib.Data.Polynomial.DenomsClearable                      instructions            -46.4%
+ ~Mathlib.Data.Polynomial.Derivative                           instructions            -20.1%
+ ~Mathlib.Data.Polynomial.Div                                  instructions            -18.8%
- ~Mathlib.Data.Polynomial.EraseLead                            instructions             46.6%
+ ~Mathlib.Data.Polynomial.FieldDivision                        instructions            -78.5%
+ ~Mathlib.Data.Polynomial.HasseDeriv                           instructions            -34.7%
- ~Mathlib.Data.Polynomial.Induction                            instructions             38.7%
- ~Mathlib.Data.Polynomial.Inductions                           instructions             33.0%
+ ~Mathlib.Data.Polynomial.IntegralNormalization                instructions             -6.2%
+ ~Mathlib.Data.Polynomial.Lifts                                instructions            -39.7%
- ~Mathlib.Data.Polynomial.Monic                                instructions             24.4%
+ ~Mathlib.Data.Polynomial.Monomial                             instructions            -56.6%
+ ~Mathlib.Data.Polynomial.PartialFractions                     instructions            -72.1%
- ~Mathlib.Data.Polynomial.Reverse                              instructions             28.6%
+ ~Mathlib.Data.Polynomial.RingDivision                         instructions            -22.1%
+ ~Mathlib.Data.Polynomial.Splits                               instructions            -83.5%
+ ~Mathlib.Data.Polynomial.Taylor                               instructions            -12.5%
- ~Mathlib.Data.QPF.Multivariate.Constructions.Comp             instructions             38.8%
- ~Mathlib.Data.QPF.Multivariate.Constructions.Fix              instructions             55.5%
- ~Mathlib.Data.Rat.BigOperators                                instructions              8.6%
+ ~Mathlib.Data.Rat.Cast                                        instructions            -16.3%
- ~Mathlib.Data.Rat.Defs                                        instructions              6.5%
+ ~Mathlib.Data.Rat.Floor                                       instructions            -22.0%
+ ~Mathlib.Data.Rat.NNRat                                       instructions            -22.1%
+ ~Mathlib.Data.Rat.Order                                       instructions             -7.4%
+ ~Mathlib.Data.Real.Basic                                      instructions            -64.0%
+ ~Mathlib.Data.Real.CauSeq                                     instructions            -44.8%
+ ~Mathlib.Data.Real.CauSeqCompletion                           instructions            -39.3%
+ ~Mathlib.Data.Real.ConjugateExponents                         instructions             -5.4%
+ ~Mathlib.Data.Real.ENNReal                                    instructions            -26.2%
+ ~Mathlib.Data.Real.ENatENNReal                                instructions            -49.1%
+ ~Mathlib.Data.Real.NNReal                                     instructions            -23.8%
+ ~Mathlib.Data.Real.Pointwise                                  instructions            -11.4%
+ ~Mathlib.Data.Real.Sqrt                                       instructions            -11.3%
- ~Mathlib.Data.Set.Countable                                   instructions             22.9%
- ~Mathlib.Data.Set.Finite                                      instructions             31.6%
+ ~Mathlib.Data.Set.Intervals.Disjoint                          instructions             -5.1%
+ ~Mathlib.Data.Set.Intervals.IsoIoo                            instructions            -16.5%
- ~Mathlib.Data.Set.Intervals.Pi                                instructions             80.5%
+ ~Mathlib.Data.Set.Intervals.SurjOn                            instructions             -7.1%
+ ~Mathlib.Data.Set.Pointwise.Basic                             instructions            -28.5%
- ~Mathlib.Data.Set.Pointwise.BigOperators                      instructions             36.4%
- ~Mathlib.Data.Set.Pointwise.Finite                            instructions             68.6%
+ ~Mathlib.Data.Set.Pointwise.Iterate                           instructions            -13.9%
+ ~Mathlib.Data.Set.Pointwise.ListOfFn                          instructions            -20.8%
- ~Mathlib.Data.Set.Semiring                                    instructions              7.2%
- ~Mathlib.Data.Setoid.Partition                                instructions             13.1%
- ~Mathlib.Data.Sign                                            instructions              7.4%
+ ~Mathlib.Data.String.Basic                                    instructions            -27.1%
- ~Mathlib.Data.String.Defs                                     instructions             43.8%
- ~Mathlib.Data.UInt                                            instructions             11.6%
+ ~Mathlib.Data.Vector.Basic                                    instructions            -17.6%
+ ~Mathlib.Data.ZMod.Basic                                      instructions             -5.5%
- ~Mathlib.Data.ZMod.Coprime                                    instructions              8.7%
+ ~Mathlib.Data.ZMod.Defs                                       instructions             -8.0%
+ ~Mathlib.Deprecated.Group                                     instructions             -7.3%
- ~Mathlib.Deprecated.Subfield                                  instructions             10.8%
+ ~Mathlib.Deprecated.Subgroup                                  instructions            -37.8%
+ ~Mathlib.Deprecated.Submonoid                                 instructions             -8.4%
- ~Mathlib.Deprecated.Subring                                   instructions             13.4%
- ~Mathlib.Dynamics.PeriodicPts                                 instructions             26.4%
+ ~Mathlib.FieldTheory.MvPolynomial                             instructions            -56.0%
+ ~Mathlib.FieldTheory.PerfectClosure                           instructions            -10.5%
+ ~Mathlib.FieldTheory.Subfield                                 instructions            -17.0%
- ~Mathlib.GroupTheory.Abelianization                           instructions             21.4%
+ ~Mathlib.GroupTheory.CommutingProbability                     instructions            -12.7%
+ ~Mathlib.GroupTheory.Congruence                               instructions            -41.4%
+ ~Mathlib.GroupTheory.Coset                                    instructions            -31.7%
- ~Mathlib.GroupTheory.Divisible                                instructions             48.5%
+ ~Mathlib.GroupTheory.Finiteness                               instructions            -24.9%
- ~Mathlib.GroupTheory.FreeAbelianGroup                         instructions             15.7%
+ ~Mathlib.GroupTheory.FreeGroup                                instructions            -18.3%
+ ~Mathlib.GroupTheory.FreeProduct                              instructions            -17.0%
+ ~Mathlib.GroupTheory.GroupAction.Basic                        instructions            -12.1%
+ ~Mathlib.GroupTheory.GroupAction.ConjAct                      instructions            -25.3%
+ ~Mathlib.GroupTheory.GroupAction.Defs                         instructions            -14.4%
+ ~Mathlib.GroupTheory.GroupAction.FixingSubgroup               instructions            -11.7%
+ ~Mathlib.GroupTheory.GroupAction.Quotient                     instructions            -14.3%
+ ~Mathlib.GroupTheory.GroupAction.Sigma                        instructions            -54.5%
+ ~Mathlib.GroupTheory.Index                                    instructions            -10.1%
+ ~Mathlib.GroupTheory.IsFreeGroup                              instructions             -5.3%
+ ~Mathlib.GroupTheory.MonoidLocalization                       instructions            -61.3%
+ ~Mathlib.GroupTheory.NoncommPiCoprod                          instructions            -25.5%
- ~Mathlib.GroupTheory.OrderOfElement                           instructions             61.2%
+ ~Mathlib.GroupTheory.Perm.Basic                               instructions             -5.7%
- ~Mathlib.GroupTheory.Perm.Cycle.Basic                         instructions             40.7%
+ ~Mathlib.GroupTheory.Perm.Cycle.Type                          instructions            -22.4%
- ~Mathlib.GroupTheory.Perm.Fin                                 instructions             27.9%
- ~Mathlib.GroupTheory.Perm.Option                              instructions             23.7%
- ~Mathlib.GroupTheory.Perm.Sign                                instructions             38.8%
- ~Mathlib.GroupTheory.Perm.Subgroup                            instructions              8.1%
- ~Mathlib.GroupTheory.PresentedGroup                           instructions             53.5%
+ ~Mathlib.GroupTheory.QuotientGroup                            instructions            -46.3%
- ~Mathlib.GroupTheory.Solvable                                 instructions             15.4%
+ ~Mathlib.GroupTheory.Subgroup.Basic                           instructions            -51.2%
+ ~Mathlib.GroupTheory.Subgroup.Finite                          instructions            -13.8%
+ ~Mathlib.GroupTheory.Subgroup.MulOpposite                     instructions             -8.6%
+ ~Mathlib.GroupTheory.Subgroup.Pointwise                       instructions            -18.8%
+ ~Mathlib.GroupTheory.Submonoid.Basic                          instructions            -15.7%
+ ~Mathlib.GroupTheory.Submonoid.Inverses                       instructions            -58.4%
+ ~Mathlib.GroupTheory.Submonoid.Membership                     instructions            -30.3%
+ ~Mathlib.GroupTheory.Submonoid.Operations                     instructions            -22.3%
+ ~Mathlib.GroupTheory.Submonoid.Pointwise                      instructions            -13.8%
+ ~Mathlib.GroupTheory.Subsemigroup.Basic                       instructions             -8.3%
+ ~Mathlib.GroupTheory.Subsemigroup.Center                      instructions            -13.4%
+ ~Mathlib.GroupTheory.Subsemigroup.Centralizer                 instructions             -7.5%
+ ~Mathlib.GroupTheory.Subsemigroup.Membership                  instructions            -10.6%
+ ~Mathlib.GroupTheory.Subsemigroup.Operations                  instructions            -17.1%
- ~Mathlib.Init.Classical                                       instructions              9.0%
- ~Mathlib.Init.Data.Prod                                       instructions              7.7%
- ~Mathlib.Lean.Exception                                       instructions              5.1%
- ~Mathlib.Lean.Expr.Basic                                      instructions             12.0%
- ~Mathlib.Lean.Meta                                            instructions             39.3%
+ ~Mathlib.LinearAlgebra.AffineSpace.AffineEquiv                instructions             -8.8%
+ ~Mathlib.LinearAlgebra.AffineSpace.AffineMap                  instructions            -44.0%
+ ~Mathlib.LinearAlgebra.AffineSpace.AffineSubspace             instructions            -11.8%
+ ~Mathlib.LinearAlgebra.AffineSpace.Combination                instructions            -51.9%
+ ~Mathlib.LinearAlgebra.AffineSpace.MidpointZero               instructions            -17.2%
+ ~Mathlib.LinearAlgebra.AffineSpace.Ordered                    instructions            -41.8%
+ ~Mathlib.LinearAlgebra.AffineSpace.Restrict                   instructions            -59.7%
+ ~Mathlib.LinearAlgebra.AffineSpace.Slope                      instructions            -20.9%
+ ~Mathlib.LinearAlgebra.Alternating                            instructions            -38.7%
+ ~Mathlib.LinearAlgebra.Basis                                  instructions            -21.1%
- ~Mathlib.LinearAlgebra.Basis.Bilinear                         instructions              5.8%
+ ~Mathlib.LinearAlgebra.BilinearMap                            instructions            -21.0%
+ ~Mathlib.LinearAlgebra.Dfinsupp                               instructions            -14.5%
+ ~Mathlib.LinearAlgebra.Dimension                              instructions            -64.0%
- ~Mathlib.LinearAlgebra.DirectSum.Finsupp                      instructions             30.7%
+ ~Mathlib.LinearAlgebra.DirectSum.TensorProduct                instructions            -33.4%
+ ~Mathlib.LinearAlgebra.Finsupp                                instructions            -35.4%
+ ~Mathlib.LinearAlgebra.FinsuppVectorSpace                     instructions            -12.7%
+ ~Mathlib.LinearAlgebra.FreeModule.Basic                       instructions            -19.2%
+ ~Mathlib.LinearAlgebra.FreeModule.Finite.Basic                instructions            -21.1%
+ ~Mathlib.LinearAlgebra.InvariantBasisNumber                   instructions            -51.3%
+ ~Mathlib.LinearAlgebra.Isomorphisms                           instructions            -81.5%
+ ~Mathlib.LinearAlgebra.LinearIndependent                      instructions            -14.3%
- ~Mathlib.LinearAlgebra.LinearPMap                             instructions             45.8%
- ~Mathlib.LinearAlgebra.Matrix.DotProduct                      instructions             44.7%
- ~Mathlib.LinearAlgebra.Multilinear.Basis                      instructions              5.6%
+ ~Mathlib.LinearAlgebra.Multilinear.TensorProduct              instructions             -6.4%
+ ~Mathlib.LinearAlgebra.Prod                                   instructions            -17.2%
+ ~Mathlib.LinearAlgebra.Projection                             instructions            -43.0%
+ ~Mathlib.LinearAlgebra.Quotient                               instructions            -12.7%
+ ~Mathlib.LinearAlgebra.Ray                                    instructions            -23.7%
+ ~Mathlib.LinearAlgebra.SModEq                                 instructions             -6.7%
+ ~Mathlib.LinearAlgebra.SesquilinearForm                       instructions            -70.7%
+ ~Mathlib.LinearAlgebra.StdBasis                               instructions            -32.5%
+ ~Mathlib.LinearAlgebra.TensorProduct                          instructions            -13.6%
+ ~Mathlib.LinearAlgebra.TensorProductBasis                     instructions            -28.9%
+ ~Mathlib.Logic.Denumerable                                    instructions             -5.6%
+ ~Mathlib.Logic.Equiv.Defs                                     instructions             -9.8%
- ~Mathlib.Logic.Equiv.Fintype                                  instructions             54.0%
+ ~Mathlib.Logic.Hydra                                          instructions             -5.2%
- ~Mathlib.MeasureTheory.MeasurableSpace                        instructions             13.9%
- ~Mathlib.ModelTheory.Basic                                    instructions             46.4%
+ ~Mathlib.NumberTheory.Basic                                   instructions            -39.7%
+ ~Mathlib.NumberTheory.ClassNumber.AdmissibleAbs               instructions            -23.3%
- ~Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue     instructions             35.4%
+ ~Mathlib.NumberTheory.Fermat4                                 instructions             -6.7%
+ ~Mathlib.NumberTheory.LucasPrimality                          instructions            -20.0%
+ ~Mathlib.NumberTheory.Padics.PadicNorm                        instructions            -12.4%
- ~Mathlib.NumberTheory.Primorial                               instructions             45.6%
+ ~Mathlib.NumberTheory.PythagoreanTriples                      instructions            -35.4%
+ ~Mathlib.NumberTheory.Zsqrtd.Basic                            instructions            -33.2%
- ~Mathlib.Order.Bounded                                        instructions              6.5%
+ ~Mathlib.Order.Category.LatCat                                instructions            -52.6%
+ ~Mathlib.Order.Category.LinOrdCat                             instructions            -60.1%
+ ~Mathlib.Order.Category.NonemptyFinLinOrdCat                  instructions            -13.6%
+ ~Mathlib.Order.Category.PartOrdCat                            instructions            -22.6%
+ ~Mathlib.Order.Category.PreordCat                             instructions            -19.5%
- ~Mathlib.Order.CompactlyGenerated                             instructions             17.6%
+ ~Mathlib.Order.CompleteLatticeIntervals                       instructions            -13.1%
+ ~Mathlib.Order.ConditionallyCompleteLattice.Basic             instructions             -6.8%
+ ~Mathlib.Order.Copy                                           instructions            -18.4%
- ~Mathlib.Order.Directed                                       instructions             10.4%
+ ~Mathlib.Order.Disjointed                                     instructions            -11.6%
- ~Mathlib.Order.Extension.Well                                 instructions             19.4%
+ ~Mathlib.Order.Filter.Archimedean                             instructions             -9.3%
- ~Mathlib.Order.Filter.Bases                                   instructions             48.2%
+ ~Mathlib.Order.Filter.Basic                                   instructions             -5.9%
+ ~Mathlib.Order.Filter.ENNReal                                 instructions             -9.3%
- ~Mathlib.Order.Filter.Germ                                    instructions             10.2%
- ~Mathlib.Order.Filter.Interval                                instructions              9.7%
- ~Mathlib.Order.Filter.Lift                                    instructions             47.5%
- ~Mathlib.Order.Filter.NAry                                    instructions             13.3%
- ~Mathlib.Order.Filter.Prod                                    instructions            135.0%
+ ~Mathlib.Order.Filter.Ultrafilter                             instructions            -36.7%
+ ~Mathlib.Order.FixedPoints                                    instructions             -6.1%
+ ~Mathlib.Order.Heyting.Basic                                  instructions             -5.6%
+ ~Mathlib.Order.Heyting.Hom                                    instructions             -9.8%
+ ~Mathlib.Order.Heyting.Regular                                instructions            -13.0%
+ ~Mathlib.Order.Hom.CompleteLattice                            instructions             -8.9%
+ ~Mathlib.Order.Hom.Lattice                                    instructions            -32.3%
- ~Mathlib.Order.LocallyFinite                                  instructions             16.3%
+ ~Mathlib.Order.ModularLattice                                 instructions             -9.1%
+ ~Mathlib.Order.OmegaCompletePartialOrder                      instructions             -7.7%
- ~Mathlib.Order.OrderIsoNat                                    instructions             30.4%
- ~Mathlib.Order.PartialSups                                    instructions              5.1%
- ~Mathlib.Order.Partition.Equipartition                        instructions             21.8%
- ~Mathlib.Order.RelIso.Basic                                   instructions              6.3%
+ ~Mathlib.Order.RelIso.Group                                   instructions            -38.9%
+ ~Mathlib.Order.SuccPred.IntervalSucc                          instructions            -10.2%
+ ~Mathlib.Order.UpperLower.Hom                                 instructions            -27.8%
+ ~Mathlib.Order.WellFounded                                    instructions            -13.3%
- ~Mathlib.Order.WellFoundedSet                                 instructions             32.6%
+ ~Mathlib.RepresentationTheory.Maschke                         instructions            -74.3%
+ ~Mathlib.RingTheory.Adjoin.Basic                              instructions            -44.4%
+ ~Mathlib.RingTheory.Adjoin.Fg                                 instructions            -21.8%
+ ~Mathlib.RingTheory.Adjoin.Tower                              instructions            -67.9%
- ~Mathlib.RingTheory.AlgebraTower                              instructions             10.5%
+ ~Mathlib.RingTheory.Coprime.Ideal                             instructions            -20.2%
+ ~Mathlib.RingTheory.EisensteinCriterion                       instructions            -52.5%
+ ~Mathlib.RingTheory.EuclideanDomain                           instructions            -19.7%
+ ~Mathlib.RingTheory.FiniteType                                instructions            -78.4%
+ ~Mathlib.RingTheory.Finiteness                                instructions            -40.1%
+ ~Mathlib.RingTheory.Flat                                      instructions            -16.8%
- ~Mathlib.RingTheory.FreeRing                                  instructions              9.3%
+ ~Mathlib.RingTheory.Ideal.IdempotentFg                        instructions            -70.8%
+ ~Mathlib.RingTheory.Ideal.Operations                          instructions            -51.5%
+ ~Mathlib.RingTheory.Ideal.Prod                                instructions            -63.1%
+ ~Mathlib.RingTheory.Ideal.Quotient                            instructions            -38.5%
+ ~Mathlib.RingTheory.Ideal.QuotientOperations                  instructions            -24.6%
+ ~Mathlib.RingTheory.Localization.Basic                        instructions            -23.3%
+ ~Mathlib.RingTheory.Localization.FractionRing                 instructions            -50.3%
+ ~Mathlib.RingTheory.Localization.Integer                      instructions            -33.1%
+ ~Mathlib.RingTheory.Localization.Module                       instructions            -29.4%
+ ~Mathlib.RingTheory.Localization.NumDen                       instructions            -23.7%
+ ~Mathlib.RingTheory.MvPolynomial.Basic                        instructions            -56.8%
+ ~Mathlib.RingTheory.MvPolynomial.Symmetric                    instructions            -32.0%
+ ~Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous          instructions            -15.2%
+ ~Mathlib.RingTheory.Nilpotent                                 instructions             -8.7%
+ ~Mathlib.RingTheory.Noetherian                                instructions            -15.4%
- ~Mathlib.RingTheory.NonZeroDivisors                           instructions             15.0%
- ~Mathlib.RingTheory.OreLocalization.Basic                     instructions              9.3%
+ ~Mathlib.RingTheory.Polynomial.Basic                          instructions            -65.3%
+ ~Mathlib.RingTheory.Polynomial.Chebyshev                      instructions            -25.7%
+ ~Mathlib.RingTheory.Polynomial.Content                        instructions            -28.0%
- ~Mathlib.RingTheory.Polynomial.Opposites                      instructions             52.3%
+ ~Mathlib.RingTheory.Polynomial.ScaleRoots                     instructions            -27.4%
- ~Mathlib.RingTheory.Prime                                     instructions              8.5%
+ ~Mathlib.RingTheory.PrincipalIdealDomain                      instructions            -52.8%
+ ~Mathlib.RingTheory.QuotientNilpotent                         instructions            -48.7%
+ ~Mathlib.RingTheory.QuotientNoetherian                        instructions            -13.5%
+ ~Mathlib.RingTheory.ReesAlgebra                               instructions            -71.6%
+ ~Mathlib.RingTheory.SimpleModule                              instructions            -89.7%
+ ~Mathlib.RingTheory.Subring.Basic                             instructions            -18.4%
+ ~Mathlib.RingTheory.Subring.Pointwise                         instructions            -10.7%
- ~Mathlib.RingTheory.Subsemiring.Basic                         instructions             14.2%
- ~Mathlib.RingTheory.Valuation.Basic                           instructions              5.2%
- ~Mathlib.RingTheory.Valuation.Integers                        instructions              6.5%
+ ~Mathlib.RingTheory.Valuation.Quotient                        instructions            -41.5%
- ~Mathlib.RingTheory.ZMod                                      instructions             11.5%
- ~Mathlib.SetTheory.Cardinal.Basic                             instructions             33.3%
+ ~Mathlib.SetTheory.Cardinal.Cofinality                        instructions            -54.2%
- ~Mathlib.SetTheory.Cardinal.Continuum                         instructions              8.7%
+ ~Mathlib.SetTheory.Cardinal.Divisibility                      instructions             -7.8%
- ~Mathlib.SetTheory.Cardinal.Finite                            instructions             15.6%
- ~Mathlib.SetTheory.Cardinal.Ordinal                           instructions             15.4%
+ ~Mathlib.SetTheory.Ordinal.Arithmetic                         instructions            -42.4%
- ~Mathlib.SetTheory.Ordinal.Basic                              instructions              7.1%
+ ~Mathlib.SetTheory.Ordinal.FixedPoint                         instructions            -43.9%
+ ~Mathlib.SetTheory.Ordinal.NaturalOps                         instructions             -6.4%
- ~Mathlib.SetTheory.ZFC.Basic                                  instructions              8.1%
- ~Mathlib.Tactic                                               instructions              5.9%
- ~Mathlib.Tactic.Alias                                         instructions              6.2%
- ~Mathlib.Tactic.ApplyFun                                      instructions             47.3%
- ~Mathlib.Tactic.Backtracking                                  instructions             22.6%
- ~Mathlib.Tactic.Congr!                                        instructions             10.2%
- ~Mathlib.Tactic.Continuity                                    instructions             33.8%
- ~Mathlib.Tactic.Conv                                          instructions              5.2%
- ~Mathlib.Tactic.Convert                                       instructions             20.1%
+ ~Mathlib.Tactic.Have                                          instructions             -8.4%
- ~Mathlib.Tactic.IrreducibleDef                                instructions            104.7%
- ~Mathlib.Tactic.LibrarySearch                                 instructions             36.7%
- ~Mathlib.Tactic.NormNum.Basic                                 instructions             11.4%
- ~Mathlib.Tactic.PushNeg                                       instructions             20.0%
- ~Mathlib.Tactic.Relation.Rfl                                  instructions             14.9%
- ~Mathlib.Tactic.Relation.Symm                                 instructions              5.7%
+ ~Mathlib.Tactic.Replace                                       instructions            -10.3%
- ~Mathlib.Tactic.SimpRw                                        instructions             97.6%
- ~Mathlib.Tactic.SolveByElim                                   instructions             11.9%
- ~Mathlib.Tactic.ToAdditive                                    instructions              5.1%
- ~Mathlib.Topology.Algebra.Constructions                       instructions             11.2%
+ ~Mathlib.Topology.Algebra.Field                               instructions            -38.4%
+ ~Mathlib.Topology.Algebra.FilterBasis                         instructions            -25.2%
+ ~Mathlib.Topology.Algebra.Group.Basic                         instructions            -26.9%
- ~Mathlib.Topology.Algebra.GroupCompletion                     instructions             17.8%
- ~Mathlib.Topology.Algebra.GroupWithZero                       instructions             13.7%
- ~Mathlib.Topology.Algebra.InfiniteSum.Module                  instructions              5.1%
+ ~Mathlib.Topology.Algebra.InfiniteSum.Real                    instructions             -7.9%
+ ~Mathlib.Topology.Algebra.Localization                        instructions            -13.9%
+ ~Mathlib.Topology.Algebra.Module.Basic                        instructions            -53.7%
+ ~Mathlib.Topology.Algebra.Module.LinearPMap                   instructions             -5.3%
+ ~Mathlib.Topology.Algebra.Module.Simple                       instructions            -20.6%
+ ~Mathlib.Topology.Algebra.Module.WeakDual                     instructions            -50.5%
- ~Mathlib.Topology.Algebra.Monoid                              instructions              7.1%
+ ~Mathlib.Topology.Algebra.Nonarchimedean.Basic                instructions            -13.9%
- ~Mathlib.Topology.Algebra.Order.Floor                         instructions             15.4%
+ ~Mathlib.Topology.Algebra.Order.IntermediateValue             instructions            -15.2%
+ ~Mathlib.Topology.Algebra.Order.LeftRightLim                  instructions            -21.0%
- ~Mathlib.Topology.Algebra.Order.LiminfLimsup                  instructions              5.2%
- ~Mathlib.Topology.Algebra.Order.ProjIcc                       instructions             19.2%
+ ~Mathlib.Topology.Algebra.Order.UpperLower                    instructions             -7.4%
+ ~Mathlib.Topology.Algebra.Polynomial                          instructions            -44.5%
+ ~Mathlib.Topology.Algebra.Ring.Basic                          instructions            -28.4%
- ~Mathlib.Topology.Algebra.Ring.Ideal                          instructions             30.8%
+ ~Mathlib.Topology.Algebra.Semigroup                           instructions            -19.6%
+ ~Mathlib.Topology.Algebra.StarSubalgebra                      instructions            -56.9%
+ ~Mathlib.Topology.Algebra.UniformField                        instructions            -32.4%
- ~Mathlib.Topology.Algebra.UniformGroup                        instructions             11.7%
+ ~Mathlib.Topology.Algebra.UniformRing                         instructions            -11.0%
- ~Mathlib.Topology.Algebra.WithZeroTopology                    instructions             14.6%
- ~Mathlib.Topology.Bases                                       instructions             10.3%
+ ~Mathlib.Topology.Basic                                       instructions             -7.0%
- ~Mathlib.Topology.Bornology.Constructions                     instructions            128.8%
- ~Mathlib.Topology.CompactOpen                                 instructions             30.5%
- ~Mathlib.Topology.Connected                                   instructions             12.9%
- ~Mathlib.Topology.Constructions                               instructions            119.0%
- ~Mathlib.Topology.ContinuousFunction.Basic                    instructions             15.3%
- ~Mathlib.Topology.ContinuousFunction.T0Sierpinski             instructions             10.5%
- ~Mathlib.Topology.ContinuousOn                                instructions             41.2%
- ~Mathlib.Topology.FiberBundle.Basic                           instructions              6.1%
- ~Mathlib.Topology.FiberBundle.Trivialization                  instructions              7.5%
- ~Mathlib.Topology.Homeomorph                                  instructions             12.7%
- ~Mathlib.Topology.Homotopy.Equiv                              instructions             11.8%
- ~Mathlib.Topology.Inseparable                                 instructions             14.9%
+ ~Mathlib.Topology.Instances.ENNReal                           instructions            -34.5%
+ ~Mathlib.Topology.Instances.EReal                             instructions             -9.8%
+ ~Mathlib.Topology.Instances.NNReal                            instructions            -19.6%
+ ~Mathlib.Topology.Instances.Nat                               instructions            -16.6%
+ ~Mathlib.Topology.Instances.Rat                               instructions            -15.4%
- ~Mathlib.Topology.Instances.Real                              instructions              9.0%
- ~Mathlib.Topology.List                                        instructions             15.5%
+ ~Mathlib.Topology.LocalHomeomorph                             instructions            -37.6%
- ~Mathlib.Topology.LocallyFinite                               instructions              6.7%
- ~Mathlib.Topology.Maps                                        instructions             72.6%
+ ~Mathlib.Topology.MetricSpace.Algebra                         instructions            -17.8%
- ~Mathlib.Topology.MetricSpace.Antilipschitz                   instructions             22.3%
- ~Mathlib.Topology.MetricSpace.Basic                           instructions              6.2%
+ ~Mathlib.Topology.MetricSpace.CauSeqFilter                    instructions            -13.9%
+ ~Mathlib.Topology.MetricSpace.HausdorffDistance               instructions            -10.2%
+ ~Mathlib.Topology.MetricSpace.Infsep                          instructions             -5.3%
- ~Mathlib.Topology.MetricSpace.Isometry                        instructions             60.9%
- ~Mathlib.Topology.MetricSpace.Lipschitz                       instructions             18.1%
+ ~Mathlib.Topology.MetricSpace.PiNat                           instructions            -34.7%
- ~Mathlib.Topology.OmegaCompletePartialOrder                   instructions             17.3%
+ ~Mathlib.Topology.Order                                       instructions            -11.8%
- ~Mathlib.Topology.Paracompact                                 instructions            196.4%
- ~Mathlib.Topology.Perfect                                     instructions           4650.8%
- ~Mathlib.Topology.Separation                                  instructions              7.1%
- ~Mathlib.Topology.Sequences                                   instructions             35.3%
+ ~Mathlib.Topology.Sets.Closeds                                instructions            -61.7%
- ~Mathlib.Topology.Sets.Compacts                               instructions             13.3%
+ ~Mathlib.Topology.StoneCech                                   instructions            -10.0%
- ~Mathlib.Topology.SubsetProperties                            instructions             38.9%
+ ~Mathlib.Topology.Support                                     instructions             -6.0%
+ ~Mathlib.Topology.UniformSpace.AbsoluteValue                  instructions             -5.5%
- ~Mathlib.Topology.UniformSpace.AbstractCompletion             instructions              6.7%
- ~Mathlib.Topology.UniformSpace.Basic                          instructions             17.9%
- ~Mathlib.Topology.UniformSpace.Cauchy                         instructions             41.1%
- ~Mathlib.Topology.UniformSpace.Compact                        instructions             68.5%
+ ~Mathlib.Topology.UniformSpace.CompareReals                   instructions            -12.1%
- ~Mathlib.Topology.UniformSpace.Completion                     instructions             11.1%
- ~Mathlib.Topology.UniformSpace.Equicontinuity                 instructions             56.5%
- ~Mathlib.Topology.UniformSpace.Equiv                          instructions            150.0%
+ ~Mathlib.Topology.UniformSpace.Pi                             instructions             -7.8%
+ ~Mathlib.Topology.UniformSpace.Separation                     instructions             -6.3%
- ~Mathlib.Topology.UniformSpace.UniformConvergence             instructions             49.3%
+ ~Mathlib.Topology.UniformSpace.UniformConvergenceTopology     instructions            -29.7%
- ~Mathlib.Topology.UniformSpace.UniformEmbedding               instructions             33.1%
- ~Mathlib.Util.SynthesizeUsing                                 instructions             35.5%
- ~Qq.AssertInstancesCommute                                    instructions             10.9%
- ~Std.Data.AssocList                                           instructions              8.3%
- ~Std.Data.HashMap.Basic                                       instructions              6.4%
- ~Std.Data.HashMap.WF                                          instructions              7.2%
+ ~Std.Data.String                                              instructions            -80.1%
+ ~Std.Tactic.Lint.TypeClass                                    instructions            -73.3%

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented May 8, 2023

!bench

@kim-em kim-em mentioned this pull request May 11, 2023
Closed
1 task
@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 16, 2023
@kim-em kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 16, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented May 16, 2023

I have a clean build/test/lint locally, so:

bors p=10

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels May 16, 2023
bors bot pushed a commit that referenced this pull request May 16, 2023
@gebner @kim-em @mattrobball
chore: reenable eta, bump to nightly 2023-05-16 (#3414)
a6e1045 
Now that leanprover/lean4#2210 has been merged, this PR:
* removes all the `set_option synthInstance.etaExperiment true` commands (and some `etaExperiment%` term elaborators)
* removes many but not quite all `set_option maxHeartbeats` commands
* makes various other changes required to cope with leanprover/lean4#2210.



Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Matthew Ballard <matt@mrb.email>
yuma-mizuno added a commit that referenced this pull request May 16, 2023
@yuma-mizuno
simplified after merging #3414
0bfad04
@bors
Copy link
Copy Markdown

bors bot commented May 16, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title chore: reenable eta, bump to nightly 2023-05-16 [Merged by Bors] - chore: reenable eta, bump to nightly 2023-05-16 May 16, 2023
@bors bors bot closed this May 16, 2023
@bors bors bot deleted the reenableeta branch May 16, 2023 13:10
@mattrobball mattrobball mentioned this pull request May 16, 2023
Closed
kim-em added a commit that referenced this pull request May 16, 2023
@kim-em
chore: some simpNF cleanaup after #3414
609d7e6
bors bot pushed a commit that referenced this pull request May 16, 2023
@kim-em @yuma-mizuno
@mattrobball @collares @gebner
feat: port Algebra.Module.LocalizedModule (#3993)
69853c5 
- [x] depends on: #3414 



Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: yuma-mizuno <mizuno.y.aj@gmail.com>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Mauricio Collares <mauricio@collares.org>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
bors bot pushed a commit that referenced this pull request May 16, 2023
@kim-em @yuma-mizuno
@mattrobball @collares @gebner
feat: port Algebra.Module.LocalizedModule (#3993)
41d747a 
- [x] depends on: #3414 



Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: yuma-mizuno <mizuno.y.aj@gmail.com>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Mauricio Collares <mauricio@collares.org>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
bors bot pushed a commit that referenced this pull request May 17, 2023
@kim-em @Komyyy
@mattrobball @collares @gebner
feat: port RingTheory.FreeCommRing (#3994)
c948d8a 
- [x] depends on: #3414

original: #3087

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)


Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Mauricio Collares <mauricio@collares.org>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
bors bot pushed a commit that referenced this pull request May 17, 2023
@kim-em
chore: some simpNF cleanaup after #3414 (#4033)
3d49f21 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
bors bot pushed a commit that referenced this pull request May 17, 2023
@jjaassoonn @Ruben-VandeVelde
@kim-em @kbuzzard @int-y1 @Parcly-Taxel
feat: port RingTheory.Polynomial.Quotient (#3932)
d8a59ae 
Coming from #3292


- [x] depends on: #3414

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)


Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
@mattrobball mattrobball mentioned this pull request May 18, 2023
Closed
1 task
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Jun 21, 2023

Here are the benchmark results for commit 3fc0de8.
There were significant changes against commit da8157c:

  Benchmark                                                           Metric                Change
  ================================================================================================
+ build                                                               aesop                  -7.8%
+ build                                                               branch-misses         -19.7%
+ build                                                               branches              -27.3%
+ build                                                               elaboration           -42.9%
+ build                                                               instructions          -26.3%
+ build                                                               interpretation         -6.9%
+ build                                                               simp                  -32.3%
+ build                                                               tactic execution      -58.0%
+ build                                                               task-clock            -22.4%
+ build                                                               typeclass inference   -16.0%
+ build                                                               wall-clock            -23.3%
+ lint                                                                instructions          -39.8%
+ lint                                                                wall-clock            -42.4%
+ ~Mathlib.Algebra.Algebra.Basic                                      instructions          -29.1%
+ ~Mathlib.Algebra.Algebra.Bilinear                                   instructions          -17.9%
+ ~Mathlib.Algebra.Algebra.Equiv                                      instructions          -24.3%
+ ~Mathlib.Algebra.Algebra.Hom                                        instructions          -11.3%
+ ~Mathlib.Algebra.Algebra.Operations                                 instructions          -43.0%
+ ~Mathlib.Algebra.Algebra.Pi                                         instructions          -30.8%
+ ~Mathlib.Algebra.Algebra.Prod                                       instructions          -18.2%
+ ~Mathlib.Algebra.Algebra.RestrictScalars                            instructions          -35.1%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Basic                           instructions          -24.7%
+ ~Mathlib.Algebra.Algebra.Tower                                      instructions           -6.1%
+ ~Mathlib.Algebra.Algebra.Unitization                                instructions          -15.9%
+ ~Mathlib.Algebra.BigOperators.Associated                            instructions          -43.7%
+ ~Mathlib.Algebra.BigOperators.Finprod                               instructions           -6.4%
+ ~Mathlib.Algebra.BigOperators.Finsupp                               instructions          -16.4%
+ ~Mathlib.Algebra.BigOperators.Order                                 instructions           -8.5%
+ ~Mathlib.Algebra.BigOperators.Pi                                    instructions           -9.6%
+ ~Mathlib.Algebra.Category.GroupCat.Basic                            instructions          -23.5%
+ ~Mathlib.Algebra.Category.GroupCat.Preadditive                      instructions           -6.4%
+ ~Mathlib.Algebra.Category.ModuleCat.Basic                           instructions          -20.8%
+ ~Mathlib.Algebra.Category.ModuleCat.EpiMono                         instructions          -62.1%
+ ~Mathlib.Algebra.Category.ModuleCat.Products                        instructions          -52.1%
+ ~Mathlib.Algebra.Category.ModuleCat.Tannaka                         instructions          -12.6%
+ ~Mathlib.Algebra.Category.MonCat.Basic                              instructions          -12.6%
+ ~Mathlib.Algebra.CharP.Algebra                                      instructions          -26.0%
+ ~Mathlib.Algebra.CharP.Quotient                                     instructions          -20.4%
+ ~Mathlib.Algebra.CharZero.Lemmas                                    instructions           -5.3%
+ ~Mathlib.Algebra.CharZero.Quotient                                  instructions          -26.2%
+ ~Mathlib.Algebra.ContinuedFractions.Computation.Translations        instructions          -10.4%
+ ~Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv                instructions          -15.5%
+ ~Mathlib.Algebra.CubicDiscriminant                                  instructions          -61.9%
+ ~Mathlib.Algebra.DirectSum.Basic                                    instructions          -19.5%
+ ~Mathlib.Algebra.DirectSum.Finsupp                                  instructions          -26.4%
+ ~Mathlib.Algebra.DirectSum.Module                                   instructions          -38.2%
+ ~Mathlib.Algebra.DualNumber                                         instructions          -22.7%
+ ~Mathlib.Algebra.EuclideanDomain.Basic                              instructions           -6.6%
+ ~Mathlib.Algebra.Field.Power                                        instructions           -5.5%
+ ~Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra                       instructions          -27.5%
+ ~Mathlib.Algebra.GCDMonoid.Basic                                    instructions           -5.0%
+ ~Mathlib.Algebra.GCDMonoid.Div                                      instructions          -61.1%
+ ~Mathlib.Algebra.GeomSum                                            instructions          -46.4%
+ ~Mathlib.Algebra.Group.Conj                                         instructions          -15.3%
+ ~Mathlib.Algebra.Group.Opposite                                     instructions          -15.9%
+ ~Mathlib.Algebra.Group.Prod                                         instructions           -7.2%
+ ~Mathlib.Algebra.Group.TypeTags                                     instructions           -5.3%
+ ~Mathlib.Algebra.Group.WithOne.Basic                                instructions           -9.0%
+ ~Mathlib.Algebra.Group.WithOne.Units                                instructions           -7.7%
+ ~Mathlib.Algebra.GroupPower.Identities                              instructions           -8.5%
+ ~Mathlib.Algebra.GroupRingAction.Invariant                          instructions          -49.1%
+ ~Mathlib.Algebra.Hom.Centroid                                       instructions          -20.7%
+ ~Mathlib.Algebra.Hom.Equiv.Basic                                    instructions           -6.6%
+ ~Mathlib.Algebra.Hom.Equiv.Units.Basic                              instructions           -7.2%
+ ~Mathlib.Algebra.Hom.GroupInstances                                 instructions          -20.9%
+ ~Mathlib.Algebra.Hom.NonUnitalAlg                                   instructions           -8.2%
+ ~Mathlib.Algebra.Hom.Units                                          instructions           -5.0%
+ ~Mathlib.Algebra.Homology.Additive                                  instructions          -32.7%
+ ~Mathlib.Algebra.Homology.Flip                                      instructions          -75.6%
+ ~Mathlib.Algebra.Homology.Homology                                  instructions          -30.9%
+ ~Mathlib.Algebra.Homology.Homotopy                                  instructions          -34.7%
+ ~Mathlib.Algebra.Homology.HomotopyCategory                          instructions          -57.2%
+ ~Mathlib.Algebra.Homology.Single                                    instructions          -21.4%
+ ~Mathlib.Algebra.Lie.Basic                                          instructions          -26.3%
+ ~Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra                       instructions           -6.6%
+ ~Mathlib.Algebra.Lie.Subalgebra                                     instructions          -32.7%
+ ~Mathlib.Algebra.LinearRecurrence                                   instructions          -24.2%
+ ~Mathlib.Algebra.Module.Algebra                                     instructions          -15.1%
+ ~Mathlib.Algebra.Module.Equiv                                       instructions           -9.3%
+ ~Mathlib.Algebra.Module.LinearMap                                   instructions           -9.6%
+ ~Mathlib.Algebra.Module.Pi                                          instructions          -12.0%
+ ~Mathlib.Algebra.Module.Projective                                  instructions          -35.5%
+ ~Mathlib.Algebra.Module.Submodule.Pointwise                         instructions           -6.7%
+ ~Mathlib.Algebra.Module.ULift                                       instructions          -17.4%
+ ~Mathlib.Algebra.MonoidAlgebra.Basic                                instructions          -40.3%
+ ~Mathlib.Algebra.MonoidAlgebra.Division                             instructions          -48.8%
+ ~Mathlib.Algebra.MonoidAlgebra.Ideal                                instructions          -49.6%
+ ~Mathlib.Algebra.MonoidAlgebra.Support                              instructions          -23.9%
+ ~Mathlib.Algebra.Order.AbsoluteValue                                instructions          -18.3%
+ ~Mathlib.Algebra.Order.Algebra                                      instructions           -9.3%
+ ~Mathlib.Algebra.Order.Archimedean                                  instructions          -16.7%
+ ~Mathlib.Algebra.Order.Chebyshev                                    instructions          -20.8%
+ ~Mathlib.Algebra.Order.EuclideanAbsoluteValue                       instructions           -5.0%
+ ~Mathlib.Algebra.Order.Field.Basic                                  instructions           -8.0%
+ ~Mathlib.Algebra.Order.Field.Power                                  instructions           -9.0%
+ ~Mathlib.Algebra.Order.Floor                                        instructions          -12.9%
+ ~Mathlib.Algebra.Order.Group.Defs                                   instructions          -16.1%
+ ~Mathlib.Algebra.Order.Group.OrderIso                               instructions           -7.9%
+ ~Mathlib.Algebra.Order.Hom.Monoid                                   instructions           -6.8%
+ ~Mathlib.Algebra.Order.Hom.Ring                                     instructions           -7.1%
+ ~Mathlib.Algebra.Order.Kleene                                       instructions           -5.4%
+ ~Mathlib.Algebra.Order.LatticeGroup                                 instructions           -6.8%
+ ~Mathlib.Algebra.Order.Module                                       instructions          -18.3%
+ ~Mathlib.Algebra.Order.Monoid.ToMulBot                              instructions           -7.6%
+ ~Mathlib.Algebra.Order.Nonneg.Field                                 instructions          -24.6%
+ ~Mathlib.Algebra.Order.Nonneg.Ring                                  instructions           -7.9%
+ ~Mathlib.Algebra.Order.Positive.Field                               instructions           -6.5%
+ ~Mathlib.Algebra.Order.Rearrangement                                instructions          -14.2%
+ ~Mathlib.Algebra.Order.Ring.Abs                                     instructions          -10.0%
+ ~Mathlib.Algebra.Order.Ring.Cone                                    instructions           -6.4%
+ ~Mathlib.Algebra.Order.Ring.Defs                                    instructions          -14.8%
+ ~Mathlib.Algebra.Order.Ring.WithTop                                 instructions          -11.8%
+ ~Mathlib.Algebra.Order.SMul                                         instructions           -9.3%
+ ~Mathlib.Algebra.Order.WithZero                                     instructions          -17.7%
+ ~Mathlib.Algebra.Periodic                                           instructions           -6.1%
+ ~Mathlib.Algebra.Polynomial.BigOperators                            instructions          -15.5%
+ ~Mathlib.Algebra.Polynomial.GroupRingAction                         instructions          -27.8%
+ ~Mathlib.Algebra.QuadraticDiscriminant                              instructions          -39.8%
+ ~Mathlib.Algebra.Quandle                                            instructions          -35.5%
+ ~Mathlib.Algebra.Ring.AddAut                                        instructions          -11.5%
+ ~Mathlib.Algebra.Ring.Aut                                           instructions          -13.5%
+ ~Mathlib.Algebra.Ring.CompTypeclasses                               instructions          -10.7%
+ ~Mathlib.Algebra.Ring.Equiv                                         instructions          -10.6%
+ ~Mathlib.Algebra.Ring.Opposite                                      instructions          -16.1%
+ ~Mathlib.Algebra.Ring.Prod                                          instructions          -11.6%
+ ~Mathlib.Algebra.RingQuot                                           instructions          -13.2%
+ ~Mathlib.Algebra.Star.Basic                                         instructions           -7.9%
+ ~Mathlib.Algebra.Star.CHSH                                          instructions          -56.4%
+ ~Mathlib.Algebra.Star.Free                                          instructions           -5.7%
+ ~Mathlib.Algebra.Star.Module                                        instructions          -34.6%
+ ~Mathlib.Algebra.Star.SelfAdjoint                                   instructions          -20.8%
+ ~Mathlib.Algebra.Star.StarAlgHom                                    instructions           -9.4%
+ ~Mathlib.Algebra.Star.Subalgebra                                    instructions           -9.1%
+ ~Mathlib.Algebra.TrivSqZeroExt                                      instructions          -29.2%
+ ~Mathlib.Algebra.Tropical.Lattice                                   instructions           -7.1%
+ ~Mathlib.AlgebraicTopology.AlternatingFaceMapComplex                instructions          -29.7%
+ ~Mathlib.AlgebraicTopology.CechNerve                                instructions          -12.5%
+ ~Mathlib.AlgebraicTopology.DoldKan.Compatibility                    instructions          -44.8%
+ ~Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive              instructions          -88.5%
+ ~Mathlib.AlgebraicTopology.DoldKan.FunctorN                         instructions          -70.7%
+ ~Mathlib.AlgebraicTopology.DoldKan.GammaCompN                       instructions          -86.3%
+ ~Mathlib.AlgebraicTopology.DoldKan.Homotopies                       instructions          -11.9%
+ ~Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence              instructions          -25.3%
+ ~Mathlib.AlgebraicTopology.DoldKan.NCompGamma                       instructions          -63.1%
+ ~Mathlib.AlgebraicTopology.DoldKan.NReflectsIso                     instructions          -55.5%
+ ~Mathlib.AlgebraicTopology.DoldKan.Normalized                       instructions          -68.8%
+ ~Mathlib.AlgebraicTopology.DoldKan.PInfty                           instructions          -58.8%
+ ~Mathlib.AlgebraicTopology.DoldKan.Projections                      instructions          -28.2%
+ ~Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject            instructions          -21.1%
+ ~Mathlib.AlgebraicTopology.ExtraDegeneracy                          instructions          -12.5%
+ ~Mathlib.AlgebraicTopology.MooreComplex                             instructions          -16.9%
+ ~Mathlib.AlgebraicTopology.Nerve                                    instructions          -14.8%
+ ~Mathlib.AlgebraicTopology.SimplicialObject                         instructions          -32.1%
+ ~Mathlib.AlgebraicTopology.SimplicialSet                            instructions          -14.6%
+ ~Mathlib.AlgebraicTopology.TopologicalSimplex                       instructions          -13.4%
+ ~Mathlib.Analysis.Asymptotics.AsymptoticEquivalent                  instructions          -21.7%
+ ~Mathlib.Analysis.Asymptotics.SpecificAsymptotics                   instructions          -15.8%
+ ~Mathlib.Analysis.Asymptotics.SuperpolynomialDecay                  instructions          -13.5%
+ ~Mathlib.Analysis.BoxIntegral.Box.Basic                             instructions           -8.1%
+ ~Mathlib.Analysis.BoxIntegral.Box.SubboxInduction                   instructions           -5.6%
+ ~Mathlib.Analysis.Convex.Basic                                      instructions           -5.7%
+ ~Mathlib.Analysis.Convex.Caratheodory                               instructions          -10.0%
+ ~Mathlib.Analysis.Convex.Combination                                instructions          -42.4%
+ ~Mathlib.Analysis.Convex.Complex                                    instructions          -35.7%
+ ~Mathlib.Analysis.Convex.Exposed                                    instructions          -65.5%
+ ~Mathlib.Analysis.Convex.Extrema                                    instructions          -15.4%
+ ~Mathlib.Analysis.Convex.Function                                   instructions          -11.2%
+ ~Mathlib.Analysis.Convex.Independent                                instructions          -12.9%
+ ~Mathlib.Analysis.Convex.Jensen                                     instructions          -18.1%
+ ~Mathlib.Analysis.Convex.Normed                                     instructions          -16.3%
+ ~Mathlib.Analysis.Convex.Quasiconvex                                instructions          -16.2%
+ ~Mathlib.Analysis.Convex.Segment                                    instructions           -9.4%
+ ~Mathlib.Analysis.Convex.Slope                                      instructions          -40.6%
+ ~Mathlib.Analysis.Convex.Strict                                     instructions           -5.9%
+ ~Mathlib.Analysis.Convex.Topology                                   instructions          -10.3%
+ ~Mathlib.Analysis.Hofer                                             instructions           -7.9%
+ ~Mathlib.Analysis.LocallyConvex.Bounded                             instructions          -44.9%
+ ~Mathlib.Analysis.LocallyConvex.Polar                               instructions          -71.8%
+ ~Mathlib.Analysis.Normed.Field.Basic                                instructions          -14.7%
+ ~Mathlib.Analysis.Normed.Field.InfiniteSum                          instructions          -17.3%
+ ~Mathlib.Analysis.Normed.Group.AddTorsor                            instructions          -19.2%
+ ~Mathlib.Analysis.Normed.Group.Basic                                instructions           -7.9%
+ ~Mathlib.Analysis.Normed.Group.Hom                                  instructions          -13.0%
+ ~Mathlib.Analysis.Normed.Group.HomCompletion                        instructions          -49.8%
+ ~Mathlib.Analysis.Normed.Group.InfiniteSum                          instructions           -5.9%
+ ~Mathlib.Analysis.Normed.Group.Quotient                             instructions          -82.4%
+ ~Mathlib.Analysis.Normed.Order.UpperLower                           instructions           -6.2%
+ ~Mathlib.Analysis.Normed.Ring.Seminorm                              instructions          -37.5%
+ ~Mathlib.Analysis.NormedSpace.AddTorsor                             instructions          -55.6%
+ ~Mathlib.Analysis.NormedSpace.Basic                                 instructions          -34.0%
+ ~Mathlib.Analysis.NormedSpace.ConformalLinearMap                    instructions          -68.0%
+ ~Mathlib.Analysis.NormedSpace.ContinuousLinearMap                   instructions          -80.3%
+ ~Mathlib.Analysis.NormedSpace.LinearIsometry                        instructions          -21.3%
+ ~Mathlib.Analysis.NormedSpace.Ray                                   instructions          -11.9%
+ ~Mathlib.Analysis.NormedSpace.RieszLemma                            instructions          -12.9%
+ ~Mathlib.Analysis.NormedSpace.Star.Basic                            instructions          -65.0%
+ ~Mathlib.Analysis.Seminorm                                          instructions          -31.0%
+ ~Mathlib.Analysis.SpecialFunctions.Polynomials                      instructions          -18.4%
+ ~Mathlib.Analysis.SpecificLimits.Basic                              instructions          -20.2%
+ ~Mathlib.CategoryTheory.Abelian.Basic                               instructions          -10.7%
+ ~Mathlib.CategoryTheory.Abelian.Exact                               instructions           -6.4%
+ ~Mathlib.CategoryTheory.Abelian.FunctorCategory                     instructions          -11.6%
+ ~Mathlib.CategoryTheory.Abelian.Opposite                            instructions          -16.5%
+ ~Mathlib.CategoryTheory.Abelian.Subobject                           instructions           -8.0%
+ ~Mathlib.CategoryTheory.Action                                      instructions          -17.7%
+ ~Mathlib.CategoryTheory.Adjunction.Basic                            instructions           -5.2%
+ ~Mathlib.CategoryTheory.Adjunction.FullyFaithful                    instructions          -15.1%
+ ~Mathlib.CategoryTheory.Adjunction.Limits                           instructions          -31.1%
+ ~Mathlib.CategoryTheory.Adjunction.Opposites                        instructions           -6.7%
+ ~Mathlib.CategoryTheory.Adjunction.Over                             instructions          -15.1%
+ ~Mathlib.CategoryTheory.Adjunction.Whiskering                       instructions          -63.1%
+ ~Mathlib.CategoryTheory.Arrow                                       instructions           -7.9%
+ ~Mathlib.CategoryTheory.Category.Bipointed                          instructions          -14.4%
+ ~Mathlib.CategoryTheory.Category.Cat                                instructions          -51.9%
+ ~Mathlib.CategoryTheory.Category.QuivCat                            instructions           -7.3%
+ ~Mathlib.CategoryTheory.Category.TwoP                               instructions          -29.9%
+ ~Mathlib.CategoryTheory.Conj                                        instructions           -6.9%
+ ~Mathlib.CategoryTheory.Elements                                    instructions          -50.9%
+ ~Mathlib.CategoryTheory.Equivalence                                 instructions           -6.6%
+ ~Mathlib.CategoryTheory.EssentialImage                              instructions           -7.7%
+ ~Mathlib.CategoryTheory.FinCategory                                 instructions          -28.2%
+ ~Mathlib.CategoryTheory.FintypeCat                                  instructions           -9.6%
+ ~Mathlib.CategoryTheory.Functor.Currying                            instructions          -14.9%
+ ~Mathlib.CategoryTheory.Functor.InvIsos                             instructions           -7.4%
+ ~Mathlib.CategoryTheory.Functor.LeftDerived                         instructions          -76.9%
+ ~Mathlib.CategoryTheory.GradedObject                                instructions          -37.9%
+ ~Mathlib.CategoryTheory.Grothendieck                                instructions          -34.4%
+ ~Mathlib.CategoryTheory.Idempotents.FunctorCategories               instructions          -11.7%
+ ~Mathlib.CategoryTheory.Idempotents.FunctorExtension                instructions          -71.6%
+ ~Mathlib.CategoryTheory.Idempotents.HomologicalComplex              instructions          -50.5%
+ ~Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi                  instructions          -25.1%
+ ~Mathlib.CategoryTheory.Limits.ColimitLimit                         instructions          -42.2%
+ ~Mathlib.CategoryTheory.Limits.Comma                                instructions          -35.4%
+ ~Mathlib.CategoryTheory.Limits.Cones                                instructions          -17.9%
+ ~Mathlib.CategoryTheory.Limits.Constructions.Over.Connected         instructions           -7.5%
+ ~Mathlib.CategoryTheory.Limits.Creates                              instructions           -6.1%
+ ~Mathlib.CategoryTheory.Limits.ExactFunctor                         instructions          -12.3%
+ ~Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit   instructions          -19.2%
+ ~Mathlib.CategoryTheory.Limits.FunctorCategory                      instructions          -19.9%
+ ~Mathlib.CategoryTheory.Limits.HasLimits                            instructions          -15.2%
+ ~Mathlib.CategoryTheory.Limits.KanExtension                         instructions          -35.4%
+ ~Mathlib.CategoryTheory.Limits.Opposites                            instructions           -8.9%
+ ~Mathlib.CategoryTheory.Limits.Preserves.Basic                      instructions          -29.0%
+ ~Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory            instructions          -59.0%
+ ~Mathlib.CategoryTheory.Limits.Preserves.Limits                     instructions           -7.6%
+ ~Mathlib.CategoryTheory.Limits.Preserves.Opposites                  instructions          -35.9%
+ ~Mathlib.CategoryTheory.Limits.Presheaf                             instructions          -77.0%
+ ~Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer                instructions           -6.2%
+ ~Mathlib.CategoryTheory.Limits.Shapes.Products                      instructions           -7.1%
+ ~Mathlib.CategoryTheory.Limits.Shapes.Types                         instructions           -6.3%
+ ~Mathlib.CategoryTheory.Linear.Basic                                instructions          -75.3%
+ ~Mathlib.CategoryTheory.Linear.Yoneda                               instructions          -80.8%
+ ~Mathlib.CategoryTheory.Localization.Construction                   instructions          -49.0%
+ ~Mathlib.CategoryTheory.Localization.Opposite                       instructions          -32.6%
+ ~Mathlib.CategoryTheory.Localization.Predicate                      instructions          -24.8%
+ ~Mathlib.CategoryTheory.Monad.Adjunction                            instructions          -30.9%
+ ~Mathlib.CategoryTheory.Monad.Limits                                instructions           -9.7%
+ ~Mathlib.CategoryTheory.Monad.Products                              instructions           -6.7%
+ ~Mathlib.CategoryTheory.Monoidal.Functor                            instructions           -7.9%
+ ~Mathlib.CategoryTheory.Monoidal.Linear                             instructions           -5.6%
+ ~Mathlib.CategoryTheory.Monoidal.NaturalTransformation              instructions           -8.4%
+ ~Mathlib.CategoryTheory.Monoidal.Transport                          instructions          -12.7%
+ ~Mathlib.CategoryTheory.Opposites                                   instructions          -12.1%
+ ~Mathlib.CategoryTheory.Over                                        instructions           -6.9%
+ ~Mathlib.CategoryTheory.PEmpty                                      instructions           -5.8%
+ ~Mathlib.CategoryTheory.Preadditive.AdditiveFunctor                 instructions           -8.9%
+ ~Mathlib.CategoryTheory.Preadditive.EilenbergMoore                  instructions           -7.0%
+ ~Mathlib.CategoryTheory.Preadditive.Yoneda.Basic                    instructions          -61.2%
+ ~Mathlib.CategoryTheory.Products.Basic                              instructions           -8.2%
+ ~Mathlib.CategoryTheory.Shift.Basic                                 instructions           -6.3%
+ ~Mathlib.CategoryTheory.Sigma.Basic                                 instructions          -16.4%
+ ~Mathlib.CategoryTheory.SingleObj                                   instructions          -23.6%
+ ~Mathlib.CategoryTheory.Sites.Adjunction                            instructions          -92.7%
+ ~Mathlib.CategoryTheory.Sites.LeftExact                             instructions          -71.3%
+ ~Mathlib.CategoryTheory.Sites.Limits                                instructions           -9.1%
+ ~Mathlib.CategoryTheory.Sites.Plus                                  instructions          -40.0%
+ ~Mathlib.CategoryTheory.Sites.Sheaf                                 instructions           -7.8%
+ ~Mathlib.CategoryTheory.Sites.Sheafification                        instructions          -70.0%
+ ~Mathlib.CategoryTheory.Skeletal                                    instructions           -6.5%
+ ~Mathlib.CategoryTheory.StructuredArrow                             instructions           -7.5%
+ ~Mathlib.CategoryTheory.Subobject.Basic                             instructions          -34.4%
+ ~Mathlib.CategoryTheory.Subobject.Lattice                           instructions          -25.3%
+ ~Mathlib.CategoryTheory.Subobject.MonoOver                          instructions          -12.5%
+ ~Mathlib.CategoryTheory.Whiskering                                  instructions          -20.3%
+ ~Mathlib.CategoryTheory.Yoneda                                      instructions          -31.8%
+ ~Mathlib.Combinatorics.Additive.Energy                              instructions           -7.9%
+ ~Mathlib.Combinatorics.Additive.PluenneckeRuzsa                     instructions          -13.4%
+ ~Mathlib.Combinatorics.Catalan                                      instructions          -55.4%
+ ~Mathlib.Combinatorics.Composition                                  instructions           -8.1%
+ ~Mathlib.Combinatorics.SetFamily.Compression.UV                     instructions           -8.0%
+ ~Mathlib.Combinatorics.SetFamily.Kleitman                           instructions          -17.7%
+ ~Mathlib.Combinatorics.SetFamily.LYM                                instructions           -9.2%
+ ~Mathlib.Combinatorics.SimpleGraph.Density                          instructions          -14.4%
+ ~Mathlib.Combinatorics.SimpleGraph.Matching                         instructions          -15.5%
+ ~Mathlib.Combinatorics.SimpleGraph.Prod                             instructions           -6.7%
+ ~Mathlib.Combinatorics.SimpleGraph.Regularity.Energy                instructions           -6.7%
+ ~Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform               instructions           -6.9%
+ ~Mathlib.Control.LawfulFix                                          instructions          -30.0%
+ ~Mathlib.Data.Complex.Basic                                         instructions          -53.9%
+ ~Mathlib.Data.Complex.Determinant                                   instructions          -63.8%
+ ~Mathlib.Data.Complex.Exponential                                   instructions          -32.8%
+ ~Mathlib.Data.Complex.Module                                        instructions          -38.2%
+ ~Mathlib.Data.Dfinsupp.Basic                                        instructions          -18.3%
+ ~Mathlib.Data.Dfinsupp.Interval                                     instructions           -5.5%
+ ~Mathlib.Data.Dfinsupp.NeLocus                                      instructions          -13.3%
- ~Mathlib.Data.Fin.Basic                                             instructions           12.0%
+ ~Mathlib.Data.Fin.Tuple.BubbleSortInduction                         instructions          -18.1%
+ ~Mathlib.Data.Fin.Tuple.Sort                                        instructions           -7.0%
+ ~Mathlib.Data.Finset.Pi                                             instructions          -20.2%
+ ~Mathlib.Data.Finset.Sym                                            instructions           -8.0%
+ ~Mathlib.Data.Finsupp.Antidiagonal                                  instructions          -45.3%
+ ~Mathlib.Data.Finsupp.Basic                                         instructions          -16.7%
+ ~Mathlib.Data.Finsupp.Multiset                                      instructions          -68.5%
+ ~Mathlib.Data.Finsupp.NeLocus                                       instructions          -15.6%
+ ~Mathlib.Data.Finsupp.Pointwise                                     instructions           -5.4%
+ ~Mathlib.Data.Finsupp.ToDfinsupp                                    instructions          -17.8%
+ ~Mathlib.Data.Fintype.Basic                                         instructions           -9.2%
+ ~Mathlib.Data.Fintype.Powerset                                      instructions          -22.5%
+ ~Mathlib.Data.Int.AbsoluteValue                                     instructions          -44.8%
+ ~Mathlib.Data.Int.Associated                                        instructions           -6.1%
+ ~Mathlib.Data.Int.Cast.Lemmas                                       instructions           -7.9%
+ ~Mathlib.Data.Int.Cast.Prod                                         instructions           -7.1%
- ~Mathlib.Data.Int.ConditionallyCompleteOrder                        instructions           15.0%
+ ~Mathlib.Data.Int.Log                                               instructions          -40.0%
+ ~Mathlib.Data.List.Cycle                                            instructions          -17.1%
+ ~Mathlib.Data.List.Join                                             instructions           -5.1%
+ ~Mathlib.Data.Matrix.Basic                                          instructions          -18.8%
+ ~Mathlib.Data.Matrix.Block                                          instructions           -5.3%
+ ~Mathlib.Data.Matrix.DualNumber                                     instructions          -23.1%
+ ~Mathlib.Data.Matrix.Rank                                           instructions          -81.1%
+ ~Mathlib.Data.Multiset.Basic                                        instructions           -5.2%
+ ~Mathlib.Data.Multiset.Pi                                           instructions           -5.5%
+ ~Mathlib.Data.MvPolynomial.Basic                                    instructions          -19.3%
+ ~Mathlib.Data.MvPolynomial.CommRing                                 instructions          -51.4%
+ ~Mathlib.Data.MvPolynomial.Equiv                                    instructions          -56.5%
+ ~Mathlib.Data.MvPolynomial.Expand                                   instructions          -34.8%
+ ~Mathlib.Data.MvPolynomial.Funext                                   instructions          -61.8%
+ ~Mathlib.Data.MvPolynomial.Monad                                    instructions          -30.2%
+ ~Mathlib.Data.MvPolynomial.Polynomial                               instructions           -7.7%
+ ~Mathlib.Data.MvPolynomial.Rename                                   instructions          -29.2%
+ ~Mathlib.Data.MvPolynomial.Supported                                instructions          -51.4%
+ ~Mathlib.Data.MvPolynomial.Variables                                instructions          -11.0%
+ ~Mathlib.Data.Nat.Cast.Field                                        instructions           -6.1%
+ ~Mathlib.Data.Nat.Choose.Bounds                                     instructions           -6.4%
+ ~Mathlib.Data.Nat.Choose.Multinomial                                instructions           -6.0%
+ ~Mathlib.Data.Nat.Factorization.Basic                               instructions          -21.5%
+ ~Mathlib.Data.Nat.Order.Basic                                       instructions          -11.6%
+ ~Mathlib.Data.Nat.PSub                                              instructions           -7.6%
+ ~Mathlib.Data.Nat.Parity                                            instructions           -5.1%
+ ~Mathlib.Data.Nat.Prime                                             instructions           -6.6%
+ ~Mathlib.Data.Nat.Totient                                           instructions          -10.7%
+ ~Mathlib.Data.PFunctor.Multivariate.M                               instructions           -5.7%
+ ~Mathlib.Data.PNat.Interval                                         instructions           -8.2%
+ ~Mathlib.Data.PNat.Xgcd                                             instructions           -5.3%
+ ~Mathlib.Data.Pi.Interval                                           instructions          -10.3%
+ ~Mathlib.Data.Polynomial.Basic                                      instructions          -12.3%
+ ~Mathlib.Data.Polynomial.Coeff                                      instructions           -5.7%
+ ~Mathlib.Data.Polynomial.Degree.CardPowDegree                       instructions          -52.2%
+ ~Mathlib.Data.Polynomial.Degree.Definitions                         instructions           -7.9%
+ ~Mathlib.Data.Polynomial.Degree.Lemmas                              instructions           -5.7%
+ ~Mathlib.Data.Polynomial.DenomsClearable                            instructions          -51.5%
+ ~Mathlib.Data.Polynomial.Derivative                                 instructions          -27.7%
+ ~Mathlib.Data.Polynomial.Div                                        instructions          -16.9%
+ ~Mathlib.Data.Polynomial.EraseLead                                  instructions           -6.7%
+ ~Mathlib.Data.Polynomial.Eval                                       instructions          -20.8%
+ ~Mathlib.Data.Polynomial.FieldDivision                              instructions          -78.6%
+ ~Mathlib.Data.Polynomial.HasseDeriv                                 instructions          -40.1%
+ ~Mathlib.Data.Polynomial.Identities                                 instructions           -5.1%
+ ~Mathlib.Data.Polynomial.Inductions                                 instructions           -5.1%
+ ~Mathlib.Data.Polynomial.IntegralNormalization                      instructions           -8.3%
+ ~Mathlib.Data.Polynomial.Lifts                                      instructions          -39.7%
+ ~Mathlib.Data.Polynomial.Module                                     instructions          -58.0%
+ ~Mathlib.Data.Polynomial.Monic                                      instructions           -6.7%
+ ~Mathlib.Data.Polynomial.Monomial                                   instructions          -58.4%
+ ~Mathlib.Data.Polynomial.PartialFractions                           instructions          -70.4%
+ ~Mathlib.Data.Polynomial.Reverse                                    instructions           -6.1%
+ ~Mathlib.Data.Polynomial.RingDivision                               instructions          -22.4%
+ ~Mathlib.Data.Polynomial.Splits                                     instructions          -83.6%
+ ~Mathlib.Data.Polynomial.Taylor                                     instructions          -14.1%
+ ~Mathlib.Data.Rat.BigOperators                                      instructions           -5.8%
+ ~Mathlib.Data.Rat.Cast                                              instructions          -18.7%
+ ~Mathlib.Data.Rat.Floor                                             instructions          -23.3%
+ ~Mathlib.Data.Rat.Lemmas                                            instructions           -6.9%
+ ~Mathlib.Data.Rat.NNRat                                             instructions          -25.2%
+ ~Mathlib.Data.Rat.Order                                             instructions           -9.0%
+ ~Mathlib.Data.Real.Basic                                            instructions          -65.9%
+ ~Mathlib.Data.Real.Cardinality                                      instructions           -7.8%
+ ~Mathlib.Data.Real.CauSeq                                           instructions          -45.1%
+ ~Mathlib.Data.Real.CauSeqCompletion                                 instructions          -39.7%
+ ~Mathlib.Data.Real.ConjugateExponents                               instructions           -6.2%
+ ~Mathlib.Data.Real.ENNReal                                          instructions          -38.6%
+ ~Mathlib.Data.Real.ENatENNReal                                      instructions          -49.4%
+ ~Mathlib.Data.Real.EReal                                            instructions           -9.8%
+ ~Mathlib.Data.Real.Hyperreal                                        instructions          -10.5%
+ ~Mathlib.Data.Real.NNReal                                           instructions          -30.3%
+ ~Mathlib.Data.Real.Pointwise                                        instructions          -12.5%
+ ~Mathlib.Data.Real.Sqrt                                             instructions          -11.6%
+ ~Mathlib.Data.Set.Intervals.Disjoint                                instructions           -6.1%
+ ~Mathlib.Data.Set.Intervals.IsoIoo                                  instructions          -17.1%
+ ~Mathlib.Data.Set.Intervals.SurjOn                                  instructions           -8.2%
- ~Mathlib.Data.Set.Semiring                                          instructions            7.5%
+ ~Mathlib.Data.Vector.Basic                                          instructions          -21.6%
+ ~Mathlib.Data.ZMod.Basic                                            instructions           -7.9%
- ~Mathlib.Data.ZMod.Coprime                                          instructions            7.3%
+ ~Mathlib.Data.ZMod.Defs                                             instructions           -8.3%
+ ~Mathlib.Deprecated.Subfield                                        instructions          -10.5%
+ ~Mathlib.Deprecated.Subgroup                                        instructions           -8.5%
+ ~Mathlib.Deprecated.Subring                                         instructions           -9.8%
+ ~Mathlib.FieldTheory.MvPolynomial                                   instructions          -51.3%
+ ~Mathlib.FieldTheory.PerfectClosure                                 instructions          -12.4%
+ ~Mathlib.FieldTheory.Subfield                                       instructions          -21.6%
+ ~Mathlib.FieldTheory.Tower                                          instructions          -82.3%
+ ~Mathlib.GroupTheory.Abelianization                                 instructions          -18.0%
+ ~Mathlib.GroupTheory.Commensurable                                  instructions           -5.6%
+ ~Mathlib.GroupTheory.Commutator                                     instructions           -8.9%
+ ~Mathlib.GroupTheory.CommutingProbability                           instructions          -14.9%
- ~Mathlib.GroupTheory.Divisible                                      instructions            6.5%
+ ~Mathlib.GroupTheory.Finiteness                                     instructions           -9.3%
+ ~Mathlib.GroupTheory.FreeAbelianGroup                               instructions          -15.2%
+ ~Mathlib.GroupTheory.FreeAbelianGroupFinsupp                        instructions          -11.4%
+ ~Mathlib.GroupTheory.FreeGroup                                      instructions           -7.7%
+ ~Mathlib.GroupTheory.FreeProduct                                    instructions          -33.9%
+ ~Mathlib.GroupTheory.GroupAction.ConjAct                            instructions          -28.3%
+ ~Mathlib.GroupTheory.GroupAction.FixingSubgroup                     instructions          -10.0%
+ ~Mathlib.GroupTheory.Index                                          instructions           -6.9%
+ ~Mathlib.GroupTheory.IsFreeGroup                                    instructions           -7.0%
+ ~Mathlib.GroupTheory.MonoidLocalization                             instructions           -7.2%
+ ~Mathlib.GroupTheory.Perm.Basic                                     instructions           -8.3%
+ ~Mathlib.GroupTheory.Perm.Cycle.Basic                               instructions          -13.9%
+ ~Mathlib.GroupTheory.Perm.Cycle.Type                                instructions          -24.5%
+ ~Mathlib.GroupTheory.Perm.Fin                                       instructions           -9.0%
+ ~Mathlib.GroupTheory.Perm.Sign                                      instructions           -8.0%
+ ~Mathlib.GroupTheory.Perm.Subgroup                                  instructions           -8.8%
+ ~Mathlib.GroupTheory.QuotientGroup                                  instructions          -13.1%
+ ~Mathlib.GroupTheory.SemidirectProduct                              instructions           -7.2%
+ ~Mathlib.GroupTheory.SpecificGroups.Alternating                     instructions          -63.7%
+ ~Mathlib.GroupTheory.Subgroup.Basic                                 instructions          -13.1%
+ ~Mathlib.GroupTheory.Subgroup.Finite                                instructions          -11.5%
+ ~Mathlib.GroupTheory.Subgroup.Pointwise                             instructions          -11.9%
+ ~Mathlib.GroupTheory.Submonoid.Inverses                             instructions          -14.2%
+ ~Mathlib.GroupTheory.Submonoid.Pointwise                            instructions          -19.9%
+ ~Mathlib.LinearAlgebra.AffineSpace.AffineEquiv                      instructions          -18.3%
+ ~Mathlib.LinearAlgebra.AffineSpace.AffineMap                        instructions          -45.5%
+ ~Mathlib.LinearAlgebra.AffineSpace.AffineSubspace                   instructions          -13.1%
+ ~Mathlib.LinearAlgebra.AffineSpace.Basis                            instructions          -32.5%
+ ~Mathlib.LinearAlgebra.AffineSpace.Combination                      instructions          -60.1%
+ ~Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional                instructions          -55.1%
+ ~Mathlib.LinearAlgebra.AffineSpace.Independent                      instructions          -37.0%
+ ~Mathlib.LinearAlgebra.AffineSpace.Matrix                           instructions          -58.6%
+ ~Mathlib.LinearAlgebra.AffineSpace.MidpointZero                     instructions          -18.2%
+ ~Mathlib.LinearAlgebra.AffineSpace.Ordered                          instructions          -42.3%
+ ~Mathlib.LinearAlgebra.AffineSpace.Restrict                         instructions          -60.0%
+ ~Mathlib.LinearAlgebra.AffineSpace.Slope                            instructions          -22.1%
+ ~Mathlib.LinearAlgebra.Alternating                                  instructions          -41.8%
+ ~Mathlib.LinearAlgebra.Basic                                        instructions          -11.6%
+ ~Mathlib.LinearAlgebra.Basis                                        instructions          -28.9%
+ ~Mathlib.LinearAlgebra.BilinearMap                                  instructions          -22.7%
+ ~Mathlib.LinearAlgebra.Determinant                                  instructions          -58.0%
+ ~Mathlib.LinearAlgebra.Dfinsupp                                     instructions          -19.8%
+ ~Mathlib.LinearAlgebra.Dimension                                    instructions          -62.7%
- ~Mathlib.LinearAlgebra.DirectSum.Finsupp                            instructions           31.1%
+ ~Mathlib.LinearAlgebra.DirectSum.TensorProduct                      instructions          -33.4%
+ ~Mathlib.LinearAlgebra.FiniteDimensional                            instructions          -69.7%
+ ~Mathlib.LinearAlgebra.Finrank                                      instructions          -54.2%
+ ~Mathlib.LinearAlgebra.Finsupp                                      instructions          -37.0%
+ ~Mathlib.LinearAlgebra.FinsuppVectorSpace                           instructions          -13.2%
+ ~Mathlib.LinearAlgebra.FreeAlgebra                                  instructions          -79.2%
+ ~Mathlib.LinearAlgebra.FreeModule.Basic                             instructions          -20.5%
+ ~Mathlib.LinearAlgebra.FreeModule.Determinant                       instructions          -22.7%
+ ~Mathlib.LinearAlgebra.FreeModule.Finite.Basic                      instructions          -20.0%
+ ~Mathlib.LinearAlgebra.FreeModule.Finite.Matrix                     instructions          -75.8%
+ ~Mathlib.LinearAlgebra.FreeModule.Finite.Rank                       instructions          -61.9%
+ ~Mathlib.LinearAlgebra.FreeModule.PID                               instructions          -31.2%
+ ~Mathlib.LinearAlgebra.FreeModule.Rank                              instructions          -51.6%
+ ~Mathlib.LinearAlgebra.InvariantBasisNumber                         instructions          -56.4%
+ ~Mathlib.LinearAlgebra.Isomorphisms                                 instructions          -81.6%
+ ~Mathlib.LinearAlgebra.Lagrange                                     instructions          -68.8%
+ ~Mathlib.LinearAlgebra.LinearIndependent                            instructions          -29.1%
+ ~Mathlib.LinearAlgebra.LinearPMap                                   instructions          -10.1%
- ~Mathlib.LinearAlgebra.Matrix.AbsoluteValue                         instructions            6.7%
+ ~Mathlib.LinearAlgebra.Matrix.Adjugate                              instructions          -73.8%
+ ~Mathlib.LinearAlgebra.Matrix.Block                                 instructions          -12.3%
+ ~Mathlib.LinearAlgebra.Matrix.Circulant                             instructions           -6.6%
+ ~Mathlib.LinearAlgebra.Matrix.Determinant                           instructions           -8.9%
+ ~Mathlib.LinearAlgebra.Matrix.Diagonal                              instructions          -68.3%
+ ~Mathlib.LinearAlgebra.Matrix.FiniteDimensional                     instructions          -84.4%
+ ~Mathlib.LinearAlgebra.Matrix.MvPolynomial                          instructions          -37.1%
+ ~Mathlib.LinearAlgebra.Matrix.Nondegenerate                         instructions          -15.4%
+ ~Mathlib.LinearAlgebra.Matrix.NonsingularInverse                    instructions          -33.7%
+ ~Mathlib.LinearAlgebra.Matrix.Polynomial                            instructions          -43.8%
+ ~Mathlib.LinearAlgebra.Matrix.Reindex                               instructions          -18.1%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin                                 instructions          -43.5%
+ ~Mathlib.LinearAlgebra.Matrix.Transvection                          instructions          -30.4%
+ ~Mathlib.LinearAlgebra.Matrix.ZPow                                  instructions          -35.5%
+ ~Mathlib.LinearAlgebra.Multilinear.TensorProduct                    instructions           -7.9%
+ ~Mathlib.LinearAlgebra.Pi                                           instructions           -7.2%
+ ~Mathlib.LinearAlgebra.Prod                                         instructions          -19.6%
+ ~Mathlib.LinearAlgebra.Projection                                   instructions          -43.5%
+ ~Mathlib.LinearAlgebra.ProjectiveSpace.Basic                        instructions          -62.5%
+ ~Mathlib.LinearAlgebra.ProjectiveSpace.Independence                 instructions           -8.3%
+ ~Mathlib.LinearAlgebra.Quotient                                     instructions          -14.5%
+ ~Mathlib.LinearAlgebra.QuotientPi                                   instructions          -55.5%
+ ~Mathlib.LinearAlgebra.Ray                                          instructions          -24.7%
+ ~Mathlib.LinearAlgebra.SModEq                                       instructions           -8.3%
+ ~Mathlib.LinearAlgebra.SesquilinearForm                             instructions          -74.0%
+ ~Mathlib.LinearAlgebra.Span                                         instructions          -35.9%
+ ~Mathlib.LinearAlgebra.StdBasis                                     instructions          -34.2%
+ ~Mathlib.LinearAlgebra.SymplecticGroup                              instructions          -46.2%
+ ~Mathlib.LinearAlgebra.TensorProduct                                instructions          -15.4%
+ ~Mathlib.LinearAlgebra.TensorProductBasis                           instructions          -44.6%
+ ~Mathlib.Logic.Denumerable                                          instructions           -8.2%
+ ~Mathlib.Logic.Embedding.Basic                                      instructions           -6.8%
+ ~Mathlib.Logic.Equiv.Basic                                          instructions           -5.2%
+ ~Mathlib.Logic.Equiv.Defs                                           instructions          -11.5%
+ ~Mathlib.Logic.Equiv.Fin                                            instructions           -5.5%
+ ~Mathlib.Logic.Equiv.List                                           instructions           -8.8%
+ ~Mathlib.Logic.Equiv.TransferInstance                               instructions           -7.3%
+ ~Mathlib.Logic.Hydra                                                instructions          -11.6%
- ~Mathlib.MeasureTheory.MeasurableSpace                              instructions            8.1%
+ ~Mathlib.MeasureTheory.Measure.OuterMeasure                         instructions          -51.6%
+ ~Mathlib.ModelTheory.Encoding                                       instructions          -10.2%
+ ~Mathlib.NumberTheory.ADEInequality                                 instructions           -6.3%
+ ~Mathlib.NumberTheory.Basic                                         instructions          -42.2%
+ ~Mathlib.NumberTheory.ClassNumber.AdmissibleAbs                     instructions          -24.4%
+ ~Mathlib.NumberTheory.Fermat4                                       instructions           -7.7%
+ ~Mathlib.NumberTheory.LucasLehmer                                   instructions          -40.7%
+ ~Mathlib.NumberTheory.Padics.PadicNorm                              instructions          -14.2%
+ ~Mathlib.NumberTheory.PellMatiyasevic                               instructions           -5.2%
+ ~Mathlib.NumberTheory.Primorial                                     instructions           -6.8%
+ ~Mathlib.NumberTheory.PythagoreanTriples                            instructions          -36.7%
+ ~Mathlib.NumberTheory.Zsqrtd.Basic                                  instructions          -38.3%
- ~Mathlib.Order.Bounded                                              instructions            5.0%
+ ~Mathlib.Order.Category.DistLatCat                                  instructions          -60.4%
+ ~Mathlib.Order.Category.LatCat                                      instructions          -49.4%
+ ~Mathlib.Order.Category.LinOrdCat                                   instructions          -57.8%
+ ~Mathlib.Order.Category.NonemptyFinLinOrdCat                        instructions          -14.8%
+ ~Mathlib.Order.Category.PartOrdCat                                  instructions          -23.6%
+ ~Mathlib.Order.Category.PreordCat                                   instructions          -20.6%
+ ~Mathlib.Order.CompleteLatticeIntervals                             instructions          -14.1%
+ ~Mathlib.Order.ConditionallyCompleteLattice.Basic                   instructions           -7.7%
+ ~Mathlib.Order.ConditionallyCompleteLattice.Finset                  instructions           -5.0%
+ ~Mathlib.Order.Disjointed                                           instructions          -13.0%
+ ~Mathlib.Order.Filter.Archimedean                                   instructions          -10.9%
+ ~Mathlib.Order.Filter.AtTopBot                                      instructions           -5.4%
+ ~Mathlib.Order.Filter.Basic                                         instructions           -6.9%
+ ~Mathlib.Order.Filter.ENNReal                                       instructions           -6.0%
+ ~Mathlib.Order.Filter.Pi                                            instructions           -5.2%
+ ~Mathlib.Order.Filter.Pointwise                                     instructions          -17.5%
+ ~Mathlib.Order.Filter.Ultrafilter                                   instructions          -38.3%
+ ~Mathlib.Order.Filter.ZeroAndBoundedAtFilter                        instructions          -19.7%
+ ~Mathlib.Order.FixedPoints                                          instructions           -7.0%
+ ~Mathlib.Order.GaloisConnection                                     instructions           -6.1%
+ ~Mathlib.Order.Heyting.Basic                                        instructions           -7.1%
+ ~Mathlib.Order.Heyting.Hom                                          instructions           -7.4%
+ ~Mathlib.Order.Heyting.Regular                                      instructions          -13.4%
+ ~Mathlib.Order.Hom.CompleteLattice                                  instructions           -7.0%
+ ~Mathlib.Order.Hom.Lattice                                          instructions          -10.2%
+ ~Mathlib.Order.JordanHolder                                         instructions          -11.5%
+ ~Mathlib.Order.LatticeIntervals                                     instructions           -5.2%
+ ~Mathlib.Order.ModularLattice                                       instructions           -5.8%
+ ~Mathlib.Order.OmegaCompletePartialOrder                            instructions           -8.8%
+ ~Mathlib.Order.RelIso.Group                                         instructions          -40.2%
+ ~Mathlib.Order.SuccPred.IntervalSucc                                instructions          -11.1%
+ ~Mathlib.RepresentationTheory.Maschke                               instructions          -74.4%
+ ~Mathlib.RingTheory.Adjoin.Basic                                    instructions          -50.0%
+ ~Mathlib.RingTheory.Adjoin.Fg                                       instructions          -42.0%
+ ~Mathlib.RingTheory.Adjoin.Tower                                    instructions          -67.8%
+ ~Mathlib.RingTheory.AlgebraTower                                    instructions           -7.3%
+ ~Mathlib.RingTheory.ChainOfDivisors                                 instructions           -9.9%
+ ~Mathlib.RingTheory.Coprime.Ideal                                   instructions          -20.0%
+ ~Mathlib.RingTheory.EisensteinCriterion                             instructions          -52.8%
+ ~Mathlib.RingTheory.EuclideanDomain                                 instructions          -20.6%
+ ~Mathlib.RingTheory.FiniteType                                      instructions          -78.5%
+ ~Mathlib.RingTheory.Finiteness                                      instructions          -39.2%
+ ~Mathlib.RingTheory.Flat                                            instructions          -23.4%
+ ~Mathlib.RingTheory.FreeRing                                        instructions          -13.0%
+ ~Mathlib.RingTheory.Ideal.AssociatedPrime                           instructions          -60.3%
+ ~Mathlib.RingTheory.Ideal.Basic                                     instructions          -10.8%
+ ~Mathlib.RingTheory.Ideal.IdempotentFg                              instructions          -64.1%
+ ~Mathlib.RingTheory.Ideal.Operations                                instructions          -51.9%
+ ~Mathlib.RingTheory.Ideal.Prod                                      instructions          -60.5%
+ ~Mathlib.RingTheory.Ideal.Quotient                                  instructions          -43.0%
+ ~Mathlib.RingTheory.Ideal.QuotientOperations                        instructions          -25.6%
+ ~Mathlib.RingTheory.Localization.Basic                              instructions          -33.4%
+ ~Mathlib.RingTheory.Localization.FractionRing                       instructions          -55.8%
+ ~Mathlib.RingTheory.Localization.Ideal                              instructions          -15.1%
+ ~Mathlib.RingTheory.Localization.Integer                            instructions          -37.8%
+ ~Mathlib.RingTheory.Localization.InvSubmonoid                       instructions          -24.0%
+ ~Mathlib.RingTheory.Localization.Module                             instructions          -34.6%
+ ~Mathlib.RingTheory.Localization.NumDen                             instructions          -25.1%
+ ~Mathlib.RingTheory.Localization.Submodule                          instructions          -53.5%
+ ~Mathlib.RingTheory.Multiplicity                                    instructions           -6.4%
+ ~Mathlib.RingTheory.MvPolynomial.Basic                              instructions          -56.6%
+ ~Mathlib.RingTheory.MvPolynomial.Ideal                              instructions          -49.6%
+ ~Mathlib.RingTheory.MvPolynomial.Symmetric                          instructions          -33.9%
+ ~Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous                instructions          -16.1%
+ ~Mathlib.RingTheory.Nilpotent                                       instructions           -9.7%
+ ~Mathlib.RingTheory.Noetherian                                      instructions          -15.4%
+ ~Mathlib.RingTheory.OreLocalization.Basic                           instructions          -17.3%
+ ~Mathlib.RingTheory.Polynomial.Basic                                instructions          -63.5%
+ ~Mathlib.RingTheory.Polynomial.Chebyshev                            instructions          -26.0%
+ ~Mathlib.RingTheory.Polynomial.Content                              instructions          -28.3%
+ ~Mathlib.RingTheory.Polynomial.Eisenstein.Basic                     instructions          -26.6%
- ~Mathlib.RingTheory.Polynomial.Opposites                            instructions            6.0%
+ ~Mathlib.RingTheory.Polynomial.ScaleRoots                           instructions          -26.4%
+ ~Mathlib.RingTheory.Polynomial.Vieta                                instructions           -5.8%
+ ~Mathlib.RingTheory.Prime                                           instructions          -12.9%
+ ~Mathlib.RingTheory.PrincipalIdealDomain                            instructions          -45.6%
+ ~Mathlib.RingTheory.QuotientNilpotent                               instructions          -48.6%
+ ~Mathlib.RingTheory.ReesAlgebra                                     instructions          -70.6%
+ ~Mathlib.RingTheory.SimpleModule                                    instructions          -89.5%
+ ~Mathlib.RingTheory.Subring.Basic                                   instructions          -28.0%
+ ~Mathlib.RingTheory.Subring.Pointwise                               instructions          -12.0%
+ ~Mathlib.RingTheory.Subsemiring.Basic                               instructions           -5.6%
+ ~Mathlib.RingTheory.Valuation.Quotient                              instructions          -42.1%
- ~Mathlib.RingTheory.ZMod                                            instructions           10.2%
+ ~Mathlib.SetTheory.Cardinal.Cofinality                              instructions          -56.3%
+ ~Mathlib.SetTheory.Cardinal.Divisibility                            instructions           -6.5%
+ ~Mathlib.SetTheory.Ordinal.Arithmetic                               instructions          -44.2%
+ ~Mathlib.SetTheory.Ordinal.FixedPoint                               instructions          -44.6%
+ ~Mathlib.SetTheory.Ordinal.NaturalOps                               instructions           -7.6%
+ ~Mathlib.Topology.Algebra.Affine                                    instructions           -5.6%
+ ~Mathlib.Topology.Algebra.Algebra                                   instructions           -8.0%
+ ~Mathlib.Topology.Algebra.Field                                     instructions          -39.2%
+ ~Mathlib.Topology.Algebra.Group.Basic                               instructions          -10.5%
+ ~Mathlib.Topology.Algebra.GroupCompletion                           instructions           -8.6%
+ ~Mathlib.Topology.Algebra.GroupWithZero                             instructions          -12.7%
+ ~Mathlib.Topology.Algebra.InfiniteSum.Real                          instructions           -7.4%
+ ~Mathlib.Topology.Algebra.Localization                              instructions          -15.3%
+ ~Mathlib.Topology.Algebra.Module.Basic                              instructions          -54.6%
+ ~Mathlib.Topology.Algebra.Module.Determinant                        instructions          -63.2%
+ ~Mathlib.Topology.Algebra.Module.LinearPMap                         instructions           -6.6%
+ ~Mathlib.Topology.Algebra.Module.Multilinear                        instructions          -19.4%
+ ~Mathlib.Topology.Algebra.Module.Simple                             instructions          -21.9%
+ ~Mathlib.Topology.Algebra.Module.StrongTopology                     instructions          -74.4%
+ ~Mathlib.Topology.Algebra.Module.WeakDual                           instructions          -51.4%
+ ~Mathlib.Topology.Algebra.Nonarchimedean.Bases                      instructions          -11.5%
+ ~Mathlib.Topology.Algebra.Nonarchimedean.Basic                      instructions          -11.5%
+ ~Mathlib.Topology.Algebra.Order.Compact                             instructions           -6.2%
+ ~Mathlib.Topology.Algebra.Order.Field                               instructions          -10.8%
+ ~Mathlib.Topology.Algebra.Order.Floor                               instructions           -5.7%
+ ~Mathlib.Topology.Algebra.Order.IntermediateValue                   instructions          -16.3%
+ ~Mathlib.Topology.Algebra.Order.LeftRightLim                        instructions           -6.3%
+ ~Mathlib.Topology.Algebra.Order.LiminfLimsup                        instructions           -6.5%
+ ~Mathlib.Topology.Algebra.Polynomial                                instructions          -45.2%
+ ~Mathlib.Topology.Algebra.Ring.Basic                                instructions          -34.6%
+ ~Mathlib.Topology.Algebra.StarSubalgebra                            instructions          -57.4%
+ ~Mathlib.Topology.Algebra.UniformConvergence                        instructions          -22.7%
+ ~Mathlib.Topology.Algebra.UniformField                              instructions          -36.8%
+ ~Mathlib.Topology.Algebra.UniformGroup                              instructions           -5.8%
+ ~Mathlib.Topology.Algebra.UniformRing                               instructions          -17.9%
+ ~Mathlib.Topology.Basic                                             instructions           -6.2%
+ ~Mathlib.Topology.Category.CompHaus.Basic                           instructions          -11.2%
+ ~Mathlib.Topology.Category.Profinite.Basic                          instructions          -15.7%
+ ~Mathlib.Topology.Category.Top.Adjunctions                          instructions          -26.8%
+ ~Mathlib.Topology.Category.Top.OpenNhds                             instructions           -5.1%
- ~Mathlib.Topology.ContinuousFunction.T0Sierpinski                   instructions            7.4%
+ ~Mathlib.Topology.Filter                                            instructions           -6.1%
+ ~Mathlib.Topology.Homotopy.Basic                                    instructions           -6.1%
+ ~Mathlib.Topology.Homotopy.Equiv                                    instructions          -10.8%
+ ~Mathlib.Topology.Instances.ENNReal                                 instructions          -34.9%
+ ~Mathlib.Topology.Instances.EReal                                   instructions          -10.9%
+ ~Mathlib.Topology.Instances.Matrix                                  instructions          -22.5%
+ ~Mathlib.Topology.Instances.NNReal                                  instructions          -28.3%
+ ~Mathlib.Topology.Instances.Nat                                     instructions          -17.8%
+ ~Mathlib.Topology.Instances.Rat                                     instructions           -5.6%
+ ~Mathlib.Topology.Instances.Real                                    instructions          -13.1%
+ ~Mathlib.Topology.Instances.RealVectorSpace                         instructions          -17.3%
+ ~Mathlib.Topology.Instances.TrivSqZeroExt                           instructions           -7.5%
+ ~Mathlib.Topology.LocalHomeomorph                                   instructions          -38.2%
+ ~Mathlib.Topology.LocallyConstant.Algebra                           instructions           -6.1%
+ ~Mathlib.Topology.MetricSpace.Algebra                               instructions          -16.0%
+ ~Mathlib.Topology.MetricSpace.Basic                                 instructions           -5.9%
+ ~Mathlib.Topology.MetricSpace.CauSeqFilter                          instructions          -12.8%
+ ~Mathlib.Topology.MetricSpace.Completion                            instructions           -6.7%
+ ~Mathlib.Topology.MetricSpace.EMetricSpace                          instructions           -5.6%
+ ~Mathlib.Topology.MetricSpace.HausdorffDistance                     instructions          -11.8%
+ ~Mathlib.Topology.MetricSpace.Infsep                                instructions           -7.6%
+ ~Mathlib.Topology.MetricSpace.Isometry                              instructions           -9.0%
+ ~Mathlib.Topology.MetricSpace.Lipschitz                             instructions           -8.0%
+ ~Mathlib.Topology.MetricSpace.PiNat                                 instructions          -32.7%
+ ~Mathlib.Topology.MetricSpace.Polish                                instructions           -5.1%
- ~Mathlib.Topology.OmegaCompletePartialOrder                         instructions            7.3%
+ ~Mathlib.Topology.Order                                             instructions          -12.8%
+ ~Mathlib.Topology.PathConnected                                     instructions          -13.0%
+ ~Mathlib.Topology.Separation                                        instructions           -8.3%
+ ~Mathlib.Topology.Sequences                                         instructions           -5.8%
+ ~Mathlib.Topology.Sets.Closeds                                      instructions          -61.9%
- ~Mathlib.Topology.Sets.Compacts                                     instructions           10.0%
+ ~Mathlib.Topology.Sets.Opens                                        instructions           -7.3%
+ ~Mathlib.Topology.StoneCech                                         instructions          -11.6%
+ ~Mathlib.Topology.UniformSpace.AbsoluteValue                        instructions          -12.7%
+ ~Mathlib.Topology.UniformSpace.CompareReals                         instructions          -19.0%
+ ~Mathlib.Topology.UniformSpace.Completion                           instructions          -19.3%
+ ~Mathlib.Topology.UniformSpace.Pi                                   instructions           -9.3%
+ ~Mathlib.Topology.UniformSpace.Separation                           instructions           -7.7%
+ ~Mathlib.Topology.UniformSpace.UniformConvergenceTopology           instructions          -34.4%
+ ~Mathlib.Topology.UrysohnsLemma                                     instructions          -37.3%

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments

+1 more reviewer

@Parcly-Taxel Parcly-Taxel Parcly-Taxel left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

7 participants

@gebner @leanprover-bot @kim-em @Parcly-Taxel @Ruben-VandeVelde @mattrobball @collares