[Merged by Bors] - refactor(Data/FunLike): use unbundled inheritance from FunLike #8386

Vierkantor · 2023-11-13T14:06:48Z

The FunLike hierarchy is very big and gets scanned through each time we need a coercion (via the CoeFun instance). It looks like unbundled inheritance suits Lean 4 better here. The only class that still extends FunLike is EquivLike, since that has a custom coe_injective' field that is easier to implement. All other classes should take FunLike or EquivLike as a parameter.

Zulip thread

Important changes

Previously, morphism classes would be Type-valued and extend FunLike:

/-- `MyHomClass F A B` states that `F` is a type of `MyClass.op`-preserving morphisms.
You should extend this class when you extend `MyHom`. -/
class MyHomClass (F : Type*) (A B : outParam <| Type*) [MyClass A] [MyClass B]
  extends FunLike F A B :=
(map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y))

After this PR, they should be Prop-valued and take FunLike as a parameter:

/-- `MyHomClass F A B` states that `F` is a type of `MyClass.op`-preserving morphisms.
You should extend this class when you extend `MyHom`. -/
class MyHomClass (F : Type*) (A B : outParam <| Type*) [MyClass A] [MyClass B]
  [FunLike F A B] : Prop :=
(map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y))

(Note that A B stay marked as outParam even though they are not purely required to be so due to the FunLike parameter already filling them in. This is required to see through type synonyms, which is important in the category theory library. Also, I think keeping them as outParam is slightly faster.)

Similarly, MyEquivClass should take EquivLike as a parameter.

As a result, every mention of [MyHomClass F A B] should become [FunLike F A B] [MyHomClass F A B].

Remaining issues

Slower (failing) search

While overall this gives some great speedups, there are some cases that are noticeably slower. In particular, a failing application of a lemma such as map_mul is more expensive. This is due to suboptimal processing of arguments. For example:

variable [FunLike F M N] [Mul M] [Mul N] (f : F) (x : M) (y : M)

theorem map_mul [MulHomClass F M N] : f (x * y) = f x * f y

example [AddHomClass F A B] : f (x * y) = f x * f y := map_mul f _ _

Before this PR, applying map_mul f gives the goals [Mul ?M] [Mul ?N] [MulHomClass F ?M ?N]. Since M and N are out_params, [MulHomClass F ?M ?N] is synthesized first, supplies values for ?M and ?N and then the Mul M and Mul N instances can be found.

After this PR, the goals become [FunLike F ?M ?N] [Mul ?M] [Mul ?N] [MulHomClass F ?M ?N]. Now [FunLike F ?M ?N] is synthesized first, supplies values for ?M and ?N and then the Mul M and Mul N instances can be found, before trying MulHomClass F M N which fails. Since the Mul hierarchy is very big, this can be slow to fail, especially when there is no such Mul instance.

A long-term but harder to achieve solution would be to specify the order in which instance goals get solved. For example, we'd like to change the arguments to map_mul to look like [FunLike F M N] [Mul M] [Mul N] [highPriority <| MulHomClass F M N] because MulHomClass fails or succeeds much faster than the others.

As a consequence, the simpNF linter is much slower since by design it tries and fails to apply many map_ lemmas. The same issue occurs a few times in existing calls to simp [map_mul], where map_mul is tried "too soon" and fails. Thanks to the speedup of leanprover/lean4#2478 the impact is very limited, only in files that already were close to the timeout.

`simp` not firing sometimes

This affects map_smulₛₗ and related definitions. For simp lemmas Lean apparently uses a slightly different mechanism to find instances, so that rw can find every argument to map_smulₛₗ successfully but simp can't: leanprover/lean4#3701.

Missing instances due to unification failing

Especially in the category theory library, we might sometimes have a type A which is also accessible as a synonym (Bundled A hA).1. Instance synthesis doesn't always work if we have f : A →* B but x * y : (Bundled A hA).1 or vice versa. This seems to be mostly fixed by keeping A B as outParams in MulHomClass F A B. (Presumably because Lean will do a definitional check A =?= (Bundled A hA).1 instead of using the syntax in the discrimination tree.)

Workaround for issues

The timeouts can be worked around for now by specifying which map_mul we mean, either as map_mul f for some explicit f, or as e.g. MonoidHomClass.map_mul.

map_smulₛₗ not firing as simp lemma can be worked around by going back to the pre-FunLike situation and making LinearMap.map_smulₛₗ a simp lemma instead of the generic map_smulₛₗ. Writing simp [map_smulₛₗ _] also works.

depends on: [Merged by Bors] - chore(*): rename FunLike to DFunLike #9785
depends on: [Merged by Bors] - refactor(*): abbreviation for non-dependent FunLike #9833

Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean

Vierkantor · 2023-12-06T16:01:45Z

We can ignore linting failures when benchmarking, right?

!bench

leanprover-bot · 2023-12-06T16:31:34Z

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

Vierkantor · 2023-12-06T16:35:44Z

Very well. Time for some lint fixing :(

Vierkantor · 2023-12-11T12:52:47Z

!bench

leanprover-bot · 2023-12-11T13:15:19Z

Here are the benchmark results for commit 1234b55.
There were significant changes against commit 7be3f99:

  Benchmark                                                             Metric                Change
  ==================================================================================================
+ build                                                                 instructions          -15.8%
+ build                                                                 tactic execution       -6.3%
+ build                                                                 task-clock            -14.2%
+ build                                                                 type checking          -5.0%
+ build                                                                 typeclass inference   -33.3%
+ build                                                                 wall-clock            -11.6%
- lint                                                                  instructions           12.1%
- lint                                                                  wall-clock             25.1%
+ ~Mathlib.Algebra.Algebra.Basic                                        instructions          -34.8%
+ ~Mathlib.Algebra.Algebra.Equiv                                        instructions          -61.2%
+ ~Mathlib.Algebra.Algebra.Hom                                          instructions          -65.2%
+ ~Mathlib.Algebra.Algebra.NonUnitalSubalgebra                          instructions           -5.7%
+ ~Mathlib.Algebra.Algebra.Spectrum                                     instructions          -31.2%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Basic                             instructions          -54.8%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Pointwise                         instructions          -64.6%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Tower                             instructions          -47.3%
+ ~Mathlib.Algebra.Algebra.Tower                                        instructions          -36.9%
+ ~Mathlib.Algebra.BigOperators.Basic                                   instructions          -11.1%
+ ~Mathlib.Algebra.BigOperators.Finsupp                                 instructions          -15.3%
+ ~Mathlib.Algebra.Category.AlgebraCat.Monoidal                         instructions           -4.9%
+ ~Mathlib.Algebra.Category.FGModuleCat.Basic                           instructions          -55.3%
+ ~Mathlib.Algebra.Category.ModuleCat.Adjunctions                       instructions          -45.3%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings                     instructions          -13.8%
+ ~Mathlib.Algebra.Category.ModuleCat.FilteredColimits                  instructions          -24.5%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic                    instructions          -44.9%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed                   instructions          -42.5%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric                instructions          -70.7%
+ ~Mathlib.Algebra.Category.Ring.Constructions                          instructions          -40.3%
+ ~Mathlib.Algebra.CharP.Basic                                          instructions          -41.8%
+ ~Mathlib.Algebra.CubicDiscriminant                                    instructions          -62.3%
+ ~Mathlib.Algebra.DirectLimit                                          instructions          -45.1%
+ ~Mathlib.Algebra.DirectSum.Algebra                                    instructions          -40.1%
+ ~Mathlib.Algebra.DirectSum.Basic                                      instructions          -35.8%
+ ~Mathlib.Algebra.DirectSum.Internal                                   instructions          -26.2%
+ ~Mathlib.Algebra.DirectSum.Module                                     instructions          -21.0%
+ ~Mathlib.Algebra.DirectSum.Ring                                       instructions          -37.1%
+ ~Mathlib.Algebra.DualNumber                                           instructions          -24.0%
+ ~Mathlib.Algebra.DualQuaternion                                       instructions          -38.9%
+ ~Mathlib.Algebra.FreeAlgebra                                          instructions          -57.3%
+ ~Mathlib.Algebra.Group.UniqueProds                                    instructions          -29.7%
+ ~Mathlib.Algebra.Homology.Homotopy                                    instructions          -34.4%
+ ~Mathlib.Algebra.Homology.HomotopyCategory.Shift                      instructions          -34.6%
+ ~Mathlib.Algebra.Homology.ModuleCat                                   instructions          -27.0%
+ ~Mathlib.Algebra.Jordan.Basic                                         instructions          -82.1%
+ ~Mathlib.Algebra.Lie.Abelian                                          instructions          -15.5%
+ ~Mathlib.Algebra.Lie.Basic                                            instructions          -12.7%
+ ~Mathlib.Algebra.Lie.DirectSum                                        instructions          -21.3%
+ ~Mathlib.Algebra.Lie.Matrix                                           instructions          -24.9%
+ ~Mathlib.Algebra.Lie.Nilpotent                                        instructions          -23.0%
+ ~Mathlib.Algebra.Lie.OfAssociative                                    instructions          -23.2%
+ ~Mathlib.Algebra.Lie.SkewAdjoint                                      instructions          -17.1%
+ ~Mathlib.Algebra.Lie.Subalgebra                                       instructions          -17.3%
+ ~Mathlib.Algebra.Lie.Weights.Basic                                    instructions           -9.3%
+ ~Mathlib.Algebra.Module.GradedModule                                  instructions          -26.4%
+ ~Mathlib.Algebra.Module.LocalizedModule                               instructions           -8.4%
+ ~Mathlib.Algebra.Module.Submodule.Map                                 instructions          -34.4%
+ ~Mathlib.Algebra.Module.Zlattice                                      instructions          -16.1%
+ ~Mathlib.Algebra.MonoidAlgebra.Basic                                  instructions          -32.5%
+ ~Mathlib.Algebra.MonoidAlgebra.Grading                                instructions          -38.0%
+ ~Mathlib.Algebra.Polynomial.BigOperators                              instructions          -19.8%
+ ~Mathlib.Algebra.Quaternion                                           instructions          -23.3%
+ ~Mathlib.Algebra.Ring.CentroidHom                                     instructions          -14.8%
+ ~Mathlib.Algebra.RingQuot                                             instructions          -35.9%
+ ~Mathlib.Algebra.Star.NonUnitalSubalgebra                             instructions          -10.6%
+ ~Mathlib.Algebra.Star.StarAlgHom                                      instructions          -47.0%
+ ~Mathlib.Algebra.Star.Subalgebra                                      instructions          -20.8%
+ ~Mathlib.Algebra.TrivSqZeroExt                                        instructions          -11.4%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Affine                       instructions          -38.7%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Group                        instructions          -49.2%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass                  instructions          -27.9%
- ~Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated                   instructions           46.9%
+ ~Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties                instructions           -6.2%
+ ~Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic                        instructions          -24.6%
+ ~Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme                  instructions          -24.3%
- ~Mathlib.AlgebraicGeometry.Properties                                 instructions           33.4%
+ ~Mathlib.AlgebraicGeometry.Pullbacks                                  instructions           -9.6%
+ ~Mathlib.AlgebraicGeometry.StructureSheaf                             instructions          -27.2%
+ ~Mathlib.AlgebraicTopology.DoldKan.PInfty                             instructions          -40.1%
+ ~Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject              instructions          -31.2%
+ ~Mathlib.AlgebraicTopology.ExtraDegeneracy                            instructions          -22.6%
+ ~Mathlib.Analysis.Analytic.Composition                                instructions           -7.7%
+ ~Mathlib.Analysis.BoxIntegral.Basic                                   instructions          -26.8%
+ ~Mathlib.Analysis.BoxIntegral.Box.Basic                               instructions          -66.0%
+ ~Mathlib.Analysis.BoxIntegral.DivergenceTheorem                       instructions          -59.4%
+ ~Mathlib.Analysis.BoxIntegral.Integrability                           instructions          -32.3%
+ ~Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension               instructions          -14.7%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic                             instructions           -6.0%
+ ~Mathlib.Analysis.Calculus.ContDiff.Bounds                            instructions          -14.3%
+ ~Mathlib.Analysis.Calculus.ContDiff.Defs                              instructions           -3.0%
+ ~Mathlib.Analysis.Calculus.FDeriv.Basic                               instructions          -23.0%
+ ~Mathlib.Analysis.Calculus.FDeriv.Mul                                 instructions          -18.5%
+ ~Mathlib.Analysis.Calculus.Implicit                                   instructions          -40.8%
+ ~Mathlib.Analysis.Complex.AbsMax                                      instructions          -48.6%
+ ~Mathlib.Analysis.Complex.Basic                                       instructions          -51.1%
+ ~Mathlib.Analysis.Complex.Isometry                                    instructions          -19.1%
+ ~Mathlib.Analysis.Complex.Liouville                                   instructions          -45.6%
- ~Mathlib.Analysis.Complex.RealDeriv                                   instructions           23.1%
+ ~Mathlib.Analysis.Complex.UpperHalfPlane.Basic                        instructions          -30.4%
+ ~Mathlib.Analysis.Convex.Combination                                  instructions          -20.9%
+ ~Mathlib.Analysis.Convex.Hull                                         instructions          -64.6%
+ ~Mathlib.Analysis.Convex.SimplicialComplex.Basic                      instructions          -36.5%
+ ~Mathlib.Analysis.Convolution                                         instructions          -13.1%
+ ~Mathlib.Analysis.Fourier.AddCircle                                   instructions          -15.7%
+ ~Mathlib.Analysis.Fourier.FourierTransform                            instructions          -33.4%
+ ~Mathlib.Analysis.Fourier.RiemannLebesgueLemma                        instructions          -34.6%
+ ~Mathlib.Analysis.InnerProductSpace.Adjoint                           instructions          -34.9%
+ ~Mathlib.Analysis.InnerProductSpace.Basic                             instructions          -35.3%
+ ~Mathlib.Analysis.InnerProductSpace.PiL2                              instructions          -11.8%
+ ~Mathlib.Analysis.InnerProductSpace.Projection                        instructions           -9.3%
+ ~Mathlib.Analysis.InnerProductSpace.Spectrum                          instructions          -28.3%
+ ~Mathlib.Analysis.InnerProductSpace.l2Space                           instructions          -10.9%
+ ~Mathlib.Analysis.Normed.Field.Basic                                  instructions          -21.1%
+ ~Mathlib.Analysis.Normed.Group.Basic                                  instructions          -16.0%
+ ~Mathlib.Analysis.Normed.Group.Hom                                    instructions          -21.2%
+ ~Mathlib.Analysis.Normed.Group.Quotient                               instructions          -19.8%
+ ~Mathlib.Analysis.Normed.Group.SemiNormedGroupCat                     instructions          -45.5%
+ ~Mathlib.Analysis.Normed.Group.SemiNormedGroupCat.Kernels             instructions          -44.3%
+ ~Mathlib.Analysis.NormedSpace.AffineIsometry                          instructions          -42.6%
+ ~Mathlib.Analysis.NormedSpace.Banach                                  instructions          -25.0%
+ ~Mathlib.Analysis.NormedSpace.Basic                                   instructions          -23.3%
+ ~Mathlib.Analysis.NormedSpace.Exponential                             instructions          -22.3%
+ ~Mathlib.Analysis.NormedSpace.Extend                                  instructions          -28.7%
+ ~Mathlib.Analysis.NormedSpace.HahnBanach.Extension                    instructions          -18.7%
+ ~Mathlib.Analysis.NormedSpace.LinearIsometry                          instructions          -10.9%
+ ~Mathlib.Analysis.NormedSpace.MazurUlam                               instructions          -69.7%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic                       instructions          -18.8%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry                       instructions           -6.0%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm                            instructions           -9.9%
+ ~Mathlib.Analysis.NormedSpace.Pointwise                               instructions          -54.5%
+ ~Mathlib.Analysis.NormedSpace.Spectrum                                instructions          -33.3%
+ ~Mathlib.Analysis.NormedSpace.Star.GelfandDuality                     instructions          -18.7%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier                         instructions           -5.1%
+ ~Mathlib.Analysis.NormedSpace.Star.Unitization                        instructions          -24.1%
+ ~Mathlib.Analysis.NormedSpace.Units                                   instructions          -59.4%
+ ~Mathlib.Analysis.NormedSpace.WeakDual                                instructions          -50.6%
+ ~Mathlib.Analysis.SpecialFunctions.Integrals                          instructions          -34.9%
+ ~Mathlib.Analysis.SpecialFunctions.Log.Basic                          instructions          -36.7%
+ ~Mathlib.Analysis.SpecialFunctions.Log.Deriv                          instructions          -44.8%
+ ~Mathlib.Analysis.SpecialFunctions.Pow.Complex                        instructions          -53.9%
+ ~Mathlib.Analysis.SpecialFunctions.Pow.Continuity                     instructions          -23.7%
+ ~Mathlib.Analysis.SpecialFunctions.Stirling                           instructions          -33.8%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan               instructions          -33.8%
+ ~Mathlib.Analysis.SpecificLimits.Basic                                instructions          -42.5%
+ ~Mathlib.Analysis.SpecificLimits.Normed                               instructions          -67.4%
+ ~Mathlib.CategoryTheory.Abelian.Pseudoelements                        instructions          -46.1%
+ ~Mathlib.CategoryTheory.Extensive                                     instructions          -17.8%
+ ~Mathlib.CategoryTheory.Monoidal.Bimod                                instructions          -10.0%
+ ~Mathlib.CategoryTheory.Monoidal.Braided                              instructions          -50.8%
+ ~Mathlib.CategoryTheory.Monoidal.Discrete                             instructions          -17.2%
+ ~Mathlib.CategoryTheory.Monoidal.Internal.Module                      instructions          -17.0%
+ ~Mathlib.CategoryTheory.Monoidal.Linear                               instructions          -57.5%
+ ~Mathlib.CategoryTheory.Monoidal.Mon_                                 instructions           -8.4%
+ ~Mathlib.CategoryTheory.Monoidal.Preadditive                          instructions          -66.6%
+ ~Mathlib.CategoryTheory.Monoidal.Rigid.Basic                          instructions          -32.3%
+ ~Mathlib.Combinatorics.Additive.Behrend                               instructions          -28.7%
+ ~Mathlib.Combinatorics.SimpleGraph.Basic                              instructions          -40.9%
+ ~Mathlib.Combinatorics.SimpleGraph.Coloring                           instructions          -61.7%
+ ~Mathlib.Combinatorics.SimpleGraph.Connectivity                       instructions          -33.1%
+ ~Mathlib.Combinatorics.SimpleGraph.Regularity.Bound                   instructions          -58.5%
+ ~Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk                   instructions          -49.9%
+ ~Mathlib.Combinatorics.SimpleGraph.Regularity.Increment               instructions          -32.2%
+ ~Mathlib.Computability.AkraBazzi.AkraBazzi                            instructions          -10.5%
+ ~Mathlib.Computability.PartrecCode                                    instructions          -12.4%
+ ~Mathlib.Computability.TMToPartrec                                    instructions          -14.2%
+ ~Mathlib.Data.Complex.Abs                                             instructions          -60.7%
+ ~Mathlib.Data.Complex.Basic                                           instructions          -26.7%
+ ~Mathlib.Data.Complex.Exponential                                     instructions          -16.3%
+ ~Mathlib.Data.DFinsupp.Basic                                          instructions          -15.5%
+ ~Mathlib.Data.DFinsupp.Multiset                                       instructions          -54.8%
+ ~Mathlib.Data.Finset.Basic                                            instructions          -12.7%
+ ~Mathlib.Data.Finsupp.Basic                                           instructions          -15.0%
+ ~Mathlib.Data.Finsupp.Defs                                            instructions          -29.5%
+ ~Mathlib.Data.Finsupp.Multiset                                        instructions          -56.8%
+ ~Mathlib.Data.IsROrC.Basic                                            instructions          -79.0%
+ ~Mathlib.Data.Matrix.Basic                                            instructions          -37.5%
+ ~Mathlib.Data.Matrix.ColumnRowPartitioned                             instructions          -62.9%
+ ~Mathlib.Data.Matrix.Kronecker                                        instructions          -21.1%
+ ~Mathlib.Data.Matrix.Notation                                         instructions          -26.9%
+ ~Mathlib.Data.Matrix.Rank                                             instructions          -32.7%
+ ~Mathlib.Data.MvPolynomial.Basic                                      instructions          -64.9%
+ ~Mathlib.Data.MvPolynomial.CommRing                                   instructions          -53.4%
+ ~Mathlib.Data.MvPolynomial.Equiv                                      instructions          -57.1%
+ ~Mathlib.Data.MvPolynomial.Expand                                     instructions          -60.7%
+ ~Mathlib.Data.MvPolynomial.Monad                                      instructions          -73.8%
+ ~Mathlib.Data.MvPolynomial.Rename                                     instructions          -70.2%
+ ~Mathlib.Data.MvPolynomial.Variables                                  instructions          -59.4%
+ ~Mathlib.Data.Num.Lemmas                                              instructions          -20.1%
+ ~Mathlib.Data.Polynomial.AlgebraMap                                   instructions          -70.8%
+ ~Mathlib.Data.Polynomial.Basic                                        instructions          -36.6%
+ ~Mathlib.Data.Polynomial.Coeff                                        instructions          -44.1%
+ ~Mathlib.Data.Polynomial.Degree.Definitions                           instructions          -65.3%
+ ~Mathlib.Data.Polynomial.Degree.Lemmas                                instructions          -50.9%
+ ~Mathlib.Data.Polynomial.Derivative                                   instructions          -23.7%
+ ~Mathlib.Data.Polynomial.Div                                          instructions          -45.9%
+ ~Mathlib.Data.Polynomial.EraseLead                                    instructions          -60.2%
+ ~Mathlib.Data.Polynomial.Eval                                         instructions          -43.8%
+ ~Mathlib.Data.Polynomial.FieldDivision                                instructions          -63.9%
+ ~Mathlib.Data.Polynomial.HasseDeriv                                   instructions          -31.9%
+ ~Mathlib.Data.Polynomial.Inductions                                   instructions          -51.6%
+ ~Mathlib.Data.Polynomial.Laurent                                      instructions          -71.3%
+ ~Mathlib.Data.Polynomial.Module                                       instructions          -16.6%
+ ~Mathlib.Data.Polynomial.Monic                                        instructions          -48.5%
+ ~Mathlib.Data.Polynomial.Reverse                                      instructions          -51.6%
+ ~Mathlib.Data.Polynomial.RingDivision                                 instructions          -66.5%
+ ~Mathlib.Data.Polynomial.Splits                                       instructions          -50.3%
+ ~Mathlib.Data.Polynomial.UnitTrinomial                                instructions          -64.3%
+ ~Mathlib.Data.QPF.Multivariate.Constructions.Cofix                    instructions          -49.8%
+ ~Mathlib.Data.ZMod.Basic                                              instructions          -43.9%
+ ~Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber             instructions          -74.1%
+ ~Mathlib.Dynamics.Ergodic.Ergodic                                     instructions          -65.7%
+ ~Mathlib.Dynamics.Ergodic.MeasurePreserving                           instructions          -53.8%
+ ~Mathlib.FieldTheory.AbelRuffini                                      instructions          -50.8%
+ ~Mathlib.FieldTheory.Adjoin                                           instructions          -24.3%
+ ~Mathlib.FieldTheory.ChevalleyWarning                                 instructions          -52.5%
+ ~Mathlib.FieldTheory.Finite.Basic                                     instructions          -45.1%
+ ~Mathlib.FieldTheory.IntermediateField                                instructions          -13.7%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure                     instructions          -29.9%
+ ~Mathlib.FieldTheory.IsAlgClosed.Basic                                instructions          -34.4%
+ ~Mathlib.FieldTheory.IsAlgClosed.Spectrum                             instructions          -47.0%
+ ~Mathlib.FieldTheory.KrullTopology                                    instructions          -36.0%
+ ~Mathlib.FieldTheory.Laurent                                          instructions          -59.5%
+ ~Mathlib.FieldTheory.Minpoly.Field                                    instructions          -60.2%
+ ~Mathlib.FieldTheory.Normal                                           instructions          -25.5%
+ ~Mathlib.FieldTheory.Perfect                                          instructions          -49.0%
+ ~Mathlib.FieldTheory.PerfectClosure                                   instructions          -52.3%
+ ~Mathlib.FieldTheory.PolynomialGaloisGroup                            instructions          -34.2%
+ ~Mathlib.FieldTheory.PrimitiveElement                                 instructions          -27.6%
+ ~Mathlib.FieldTheory.RatFunc                                          instructions          -38.3%
+ ~Mathlib.FieldTheory.Separable                                        instructions          -61.8%
+ ~Mathlib.FieldTheory.SplittingField.Construction                      instructions          -27.0%
+ ~Mathlib.Geometry.Euclidean.Basic                                     instructions          -16.5%
+ ~Mathlib.Geometry.Euclidean.Circumcenter                              instructions          -12.7%
+ ~Mathlib.Geometry.Euclidean.MongePoint                                instructions           -8.3%
+ ~Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation            instructions          -11.1%
+ ~Mathlib.Geometry.Manifold.ContMDiff.NormedSpace                      instructions           -6.6%
+ ~Mathlib.Geometry.Manifold.Diffeomorph                                instructions          -50.7%
+ ~Mathlib.Geometry.Manifold.Sheaf.Smooth                               instructions          -13.9%
+ ~Mathlib.Geometry.Manifold.VectorBundle.Tangent                       instructions          -25.8%
+ ~Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing                  instructions           -2.6%
+ ~Mathlib.GroupTheory.Abelianization                                   instructions          -41.5%
+ ~Mathlib.GroupTheory.Coprod.Basic                                     instructions          -50.1%
+ ~Mathlib.GroupTheory.CoprodI                                          instructions          -34.1%
+ ~Mathlib.GroupTheory.FreeAbelianGroup                                 instructions          -34.9%
+ ~Mathlib.GroupTheory.FreeAbelianGroupFinsupp                          instructions          -46.4%
+ ~Mathlib.GroupTheory.HNNExtension                                     instructions          -26.9%
+ ~Mathlib.GroupTheory.MonoidLocalization                               instructions          -50.2%
+ ~Mathlib.GroupTheory.NoncommPiCoprod                                  instructions          -45.6%
- ~Mathlib.GroupTheory.Perm.Fin                                         instructions           66.5%
+ ~Mathlib.GroupTheory.Perm.Sign                                        instructions          -35.9%
+ ~Mathlib.GroupTheory.PushoutI                                         instructions          -39.6%
+ ~Mathlib.GroupTheory.QuotientGroup                                    instructions          -29.2%
+ ~Mathlib.GroupTheory.Sylow                                            instructions          -49.1%
+ ~Mathlib.GroupTheory.Transfer                                         instructions          -31.9%
+ ~Mathlib.LinearAlgebra.AffineSpace.AffineEquiv                        instructions          -16.0%
+ ~Mathlib.LinearAlgebra.Alternating.Basic                              instructions          -18.6%
+ ~Mathlib.LinearAlgebra.Alternating.DomCoprod                          instructions          -20.7%
+ ~Mathlib.LinearAlgebra.Basic                                          instructions          -28.0%
+ ~Mathlib.LinearAlgebra.Basis                                          instructions          -20.9%
+ ~Mathlib.LinearAlgebra.BilinearForm.Hom                               instructions          -25.2%
+ ~Mathlib.LinearAlgebra.BilinearForm.Orthogonal                        instructions          -43.7%
+ ~Mathlib.LinearAlgebra.BilinearForm.Properties                        instructions          -34.6%
+ ~Mathlib.LinearAlgebra.Charpoly.ToMatrix                              instructions          -69.8%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange                     instructions          -13.1%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Basic                          instructions          -31.7%
- ~Mathlib.LinearAlgebra.CliffordAlgebra.Contraction                    instructions           13.7%
- ~Mathlib.LinearAlgebra.CliffordAlgebra.Equivs                         instructions           28.2%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Even                           instructions          -11.4%
- ~Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv                      instructions            9.6%
+ ~Mathlib.LinearAlgebra.Contraction                                    instructions          -37.5%
+ ~Mathlib.LinearAlgebra.DFinsupp                                       instructions          -34.2%
+ ~Mathlib.LinearAlgebra.Determinant                                    instructions          -51.5%
+ ~Mathlib.LinearAlgebra.Dimension                                      instructions          -16.9%
+ ~Mathlib.LinearAlgebra.Dual                                           instructions          -17.9%
+ ~Mathlib.LinearAlgebra.Eigenspace.Basic                               instructions          -27.8%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Basic                          instructions          -18.2%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Grading                        instructions          -21.3%
+ ~Mathlib.LinearAlgebra.FiniteDimensional                              instructions          -14.1%
+ ~Mathlib.LinearAlgebra.Finsupp                                        instructions          -16.7%
+ ~Mathlib.LinearAlgebra.FinsuppVectorSpace                             instructions          -63.1%
+ ~Mathlib.LinearAlgebra.Lagrange                                       instructions          -34.8%
+ ~Mathlib.LinearAlgebra.LinearIndependent                              instructions          -24.7%
+ ~Mathlib.LinearAlgebra.Matrix.Basis                                   instructions          -62.5%
+ ~Mathlib.LinearAlgebra.Matrix.BilinearForm                            instructions          -66.7%
+ ~Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff                          instructions          -27.9%
+ ~Mathlib.LinearAlgebra.Matrix.Determinant                             instructions          -50.6%
+ ~Mathlib.LinearAlgebra.Matrix.Diagonal                                instructions          -42.7%
+ ~Mathlib.LinearAlgebra.Matrix.DotProduct                              instructions          -50.1%
+ ~Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup                      instructions          -59.4%
+ ~Mathlib.LinearAlgebra.Matrix.Hermitian                               instructions          -44.5%
+ ~Mathlib.LinearAlgebra.Matrix.NonsingularInverse                      instructions          -33.4%
+ ~Mathlib.LinearAlgebra.Matrix.Polynomial                              instructions          -56.1%
+ ~Mathlib.LinearAlgebra.Matrix.Reindex                                 instructions          -65.8%
+ ~Mathlib.LinearAlgebra.Matrix.SchurComplement                         instructions          -50.7%
+ ~Mathlib.LinearAlgebra.Matrix.SesquilinearForm                        instructions          -67.5%
+ ~Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup                      instructions          -37.0%
+ ~Mathlib.LinearAlgebra.Matrix.Spectrum                                instructions          -20.9%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin                                   instructions          -57.9%
+ ~Mathlib.LinearAlgebra.Matrix.ToLinearEquiv                           instructions          -35.5%
+ ~Mathlib.LinearAlgebra.Orientation                                    instructions          -13.7%
+ ~Mathlib.LinearAlgebra.PiTensorProduct                                instructions          -30.5%
+ ~Mathlib.LinearAlgebra.QuadraticForm.Basic                            instructions          -15.8%
+ ~Mathlib.LinearAlgebra.QuadraticForm.Complex                          instructions          -35.0%
+ ~Mathlib.LinearAlgebra.QuadraticForm.Dual                             instructions          -26.0%
+ ~Mathlib.LinearAlgebra.QuadraticForm.Real                             instructions          -54.2%
+ ~Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries         instructions          -13.0%
+ ~Mathlib.LinearAlgebra.Span                                           instructions          -18.9%
+ ~Mathlib.LinearAlgebra.TensorAlgebra.Basic                            instructions          -33.5%
+ ~Mathlib.LinearAlgebra.TensorAlgebra.Grading                          instructions          -26.3%
+ ~Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower                    instructions          -36.6%
+ ~Mathlib.LinearAlgebra.TensorPower                                    instructions          -29.1%
+ ~Mathlib.LinearAlgebra.TensorProduct                                  instructions           -9.7%
+ ~Mathlib.LinearAlgebra.TensorProduct.Matrix                           instructions          -37.3%
+ ~Mathlib.LinearAlgebra.TensorProduct.Tower                            instructions           -6.3%
+ ~Mathlib.MeasureTheory.Constructions.BorelSpace.Basic                 instructions          -13.1%
+ ~Mathlib.MeasureTheory.Constructions.Pi                               instructions          -87.1%
+ ~Mathlib.MeasureTheory.Constructions.Polish                           instructions          -36.4%
+ ~Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable   instructions          -31.9%
+ ~Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2      instructions          -50.4%
+ ~Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique         instructions          -49.6%
+ ~Mathlib.MeasureTheory.Function.Jacobian                              instructions          -22.7%
+ ~Mathlib.MeasureTheory.Function.L1Space                               instructions          -10.7%
+ ~Mathlib.MeasureTheory.Function.LpSpace                               instructions          -11.4%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp                     instructions          -35.8%
+ ~Mathlib.MeasureTheory.Function.SpecialFunctions.IsROrC               instructions          -57.4%
+ ~Mathlib.MeasureTheory.Group.Measure                                  instructions          -46.7%
+ ~Mathlib.MeasureTheory.Integral.DivergenceTheorem                     instructions          -57.7%
+ ~Mathlib.MeasureTheory.Integral.Lebesgue                              instructions          -36.6%
+ ~Mathlib.MeasureTheory.Integral.Marginal                              instructions          -38.2%
+ ~Mathlib.MeasureTheory.Integral.SetIntegral                           instructions          -13.9%
+ ~Mathlib.MeasureTheory.Integral.SetToL1                               instructions           -7.3%
+ ~Mathlib.MeasureTheory.MeasurableSpace.Basic                          instructions          -51.6%
+ ~Mathlib.MeasureTheory.Measure.Hausdorff                              instructions          -25.0%
+ ~Mathlib.MeasureTheory.Measure.Lebesgue.Basic                         instructions          -63.9%
+ ~Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar                        instructions          -41.2%
+ ~Mathlib.MeasureTheory.Measure.MeasureSpace                           instructions          -20.8%
+ ~Mathlib.MeasureTheory.Measure.Restrict                               instructions          -37.8%
+ ~Mathlib.ModelTheory.ElementaryMaps                                   instructions          -31.9%
+ ~Mathlib.ModelTheory.Satisfiability                                   instructions          -50.1%
+ ~Mathlib.ModelTheory.Semantics                                        instructions          -33.4%
+ ~Mathlib.ModelTheory.Substructures                                    instructions          -61.9%
- ~Mathlib.NumberTheory.ArithmeticFunction                              instructions           12.6%
+ ~Mathlib.NumberTheory.Bernoulli                                       instructions          -24.0%
+ ~Mathlib.NumberTheory.ClassNumber.Finite                              instructions          -42.8%
+ ~Mathlib.NumberTheory.Cyclotomic.Basic                                instructions          -14.1%
+ ~Mathlib.NumberTheory.Cyclotomic.Discriminant                         instructions          -34.4%
+ ~Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots                       instructions          -42.6%
+ ~Mathlib.NumberTheory.Cyclotomic.Rat                                  instructions          -11.3%
+ ~Mathlib.NumberTheory.Dioph                                           instructions          -24.5%
+ ~Mathlib.NumberTheory.DiophantineApproximation                        instructions          -21.8%
+ ~Mathlib.NumberTheory.DirichletCharacter.Basic                        instructions          -52.8%
+ ~Mathlib.NumberTheory.EulerProduct.Basic                              instructions          -45.4%
+ ~Mathlib.NumberTheory.KummerDedekind                                  instructions          -23.0%
- ~Mathlib.NumberTheory.LSeries                                         instructions           66.8%
+ ~Mathlib.NumberTheory.LegendreSymbol.MulCharacter                     instructions          -42.3%
+ ~Mathlib.NumberTheory.Modular                                         instructions          -12.4%
- ~Mathlib.NumberTheory.ModularForms.Basic                              instructions           49.2%
+ ~Mathlib.NumberTheory.ModularForms.SlashActions                       instructions          -16.9%
- ~Mathlib.NumberTheory.ModularForms.SlashInvariantForms                instructions           34.2%
+ ~Mathlib.NumberTheory.Multiplicity                                    instructions          -41.3%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding                  instructions          -19.7%
+ ~Mathlib.NumberTheory.NumberField.Embeddings                          instructions          -47.9%
+ ~Mathlib.NumberTheory.NumberField.Norm                                instructions          -39.4%
+ ~Mathlib.NumberTheory.NumberField.Units                               instructions          -20.6%
+ ~Mathlib.NumberTheory.Padics.PadicIntegers                            instructions          -20.7%
+ ~Mathlib.NumberTheory.Padics.RingHoms                                 instructions          -32.1%
+ ~Mathlib.NumberTheory.RamificationInertia                             instructions           -7.9%
+ ~Mathlib.NumberTheory.Rayleigh                                        instructions          -60.4%
+ ~Mathlib.NumberTheory.ZetaFunction                                    instructions          -34.1%
+ ~Mathlib.NumberTheory.Zsqrtd.Basic                                    instructions          -10.6%
+ ~Mathlib.NumberTheory.Zsqrtd.GaussianInt                              instructions          -30.9%
+ ~Mathlib.Order.SupClosed                                              instructions          -55.6%
+ ~Mathlib.Probability.Kernel.CondCdf                                   instructions          -33.6%
+ ~Mathlib.Probability.StrongLaw                                        instructions          -48.7%
+ ~Mathlib.RepresentationTheory.Action.Basic                            instructions          -68.4%
+ ~Mathlib.RepresentationTheory.Action.Limits                           instructions          -35.1%
+ ~Mathlib.RepresentationTheory.Action.Monoidal                         instructions          -12.2%
+ ~Mathlib.RepresentationTheory.Basic                                   instructions          -45.3%
+ ~Mathlib.RepresentationTheory.FdRep                                   instructions          -33.4%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Basic                   instructions          -13.2%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Hilbert90               instructions          -60.0%
+ ~Mathlib.RepresentationTheory.GroupCohomology.LowDegree               instructions          -23.9%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Resolution              instructions          -28.6%
+ ~Mathlib.RepresentationTheory.Rep                                     instructions          -37.8%
+ ~Mathlib.RingTheory.Adjoin.Basic                                      instructions          -51.2%
+ ~Mathlib.RingTheory.Adjoin.FG                                         instructions          -52.5%
+ ~Mathlib.RingTheory.AdjoinRoot                                        instructions          -59.0%
+ ~Mathlib.RingTheory.Algebraic                                         instructions          -50.6%
+ ~Mathlib.RingTheory.AlgebraicIndependent                              instructions          -44.6%
+ ~Mathlib.RingTheory.ClassGroup                                        instructions          -57.1%
+ ~Mathlib.RingTheory.DedekindDomain.AdicValuation                      instructions          -31.0%
+ ~Mathlib.RingTheory.DedekindDomain.Ideal                              instructions          -16.4%
+ ~Mathlib.RingTheory.DedekindDomain.IntegralClosure                    instructions          -20.8%
+ ~Mathlib.RingTheory.DedekindDomain.SelmerGroup                        instructions          -48.6%
+ ~Mathlib.RingTheory.Derivation.ToSquareZero                           instructions          -42.4%
+ ~Mathlib.RingTheory.DiscreteValuationRing.Basic                       instructions          -46.3%
+ ~Mathlib.RingTheory.Discriminant                                      instructions          -21.8%
+ ~Mathlib.RingTheory.Etale                                             instructions          -16.0%
+ ~Mathlib.RingTheory.FinitePresentation                                instructions          -51.5%
+ ~Mathlib.RingTheory.FiniteType                                        instructions          -49.9%
+ ~Mathlib.RingTheory.Finiteness                                        instructions          -12.8%
+ ~Mathlib.RingTheory.FractionalIdeal                                   instructions          -23.3%
+ ~Mathlib.RingTheory.FreeCommRing                                      instructions          -35.3%
+ ~Mathlib.RingTheory.GradedAlgebra.Basic                               instructions          -18.2%
+ ~Mathlib.RingTheory.GradedAlgebra.Radical                             instructions          -44.7%
+ ~Mathlib.RingTheory.HahnSeries                                        instructions          -43.9%
+ ~Mathlib.RingTheory.Ideal.LocalRing                                   instructions          -49.6%
+ ~Mathlib.RingTheory.Ideal.Norm                                        instructions          -42.8%
+ ~Mathlib.RingTheory.Ideal.Operations                                  instructions          -28.1%
+ ~Mathlib.RingTheory.Ideal.Over                                        instructions          -24.9%
+ ~Mathlib.RingTheory.Ideal.Quotient                                    instructions          -37.6%
+ ~Mathlib.RingTheory.Ideal.QuotientOperations                          instructions          -59.1%
+ ~Mathlib.RingTheory.IntegralClosure                                   instructions          -32.1%
+ ~Mathlib.RingTheory.IntegralDomain                                    instructions          -63.7%
+ ~Mathlib.RingTheory.IsAdjoinRoot                                      instructions          -48.3%
+ ~Mathlib.RingTheory.IsTensorProduct                                   instructions          -16.9%
+ ~Mathlib.RingTheory.Jacobson                                          instructions          -19.8%
+ ~Mathlib.RingTheory.Kaehler                                           instructions          -19.0%
+ ~Mathlib.RingTheory.LocalProperties                                   instructions          -31.1%
+ ~Mathlib.RingTheory.Localization.Away.Basic                           instructions          -42.9%
+ ~Mathlib.RingTheory.Localization.Basic                                instructions          -48.3%
+ ~Mathlib.RingTheory.Localization.FractionRing                         instructions          -37.4%
+ ~Mathlib.RingTheory.Localization.Ideal                                instructions          -40.5%
+ ~Mathlib.RingTheory.Localization.Integral                             instructions          -35.3%
+ ~Mathlib.RingTheory.Localization.LocalizationLocalization             instructions          -37.1%
+ ~Mathlib.RingTheory.MatrixAlgebra                                     instructions          -23.0%
+ ~Mathlib.RingTheory.MvPolynomial.Homogeneous                          instructions          -39.5%
+ ~Mathlib.RingTheory.MvPolynomial.Tower                                instructions          -59.2%
+ ~Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous                  instructions          -56.6%
+ ~Mathlib.RingTheory.NonUnitalSubring.Basic                            instructions          -26.4%
+ ~Mathlib.RingTheory.NonUnitalSubsemiring.Basic                        instructions          -27.3%
+ ~Mathlib.RingTheory.Norm                                              instructions          -39.9%
+ ~Mathlib.RingTheory.Nullstellensatz                                   instructions          -34.0%
+ ~Mathlib.RingTheory.OreLocalization.Basic                             instructions          -37.8%
+ ~Mathlib.RingTheory.Perfection                                        instructions          -73.5%
+ ~Mathlib.RingTheory.Polynomial.Basic                                  instructions          -25.9%
+ ~Mathlib.RingTheory.Polynomial.Content                                instructions          -52.5%
+ ~Mathlib.RingTheory.Polynomial.Cyclotomic.Basic                       instructions          -34.7%
+ ~Mathlib.RingTheory.Polynomial.Dickson                                instructions          -41.7%
+ ~Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral                  instructions          -20.7%
+ ~Mathlib.RingTheory.Polynomial.GaussLemma                             instructions          -42.8%
+ ~Mathlib.RingTheory.Polynomial.Quotient                               instructions          -30.4%
+ ~Mathlib.RingTheory.Polynomial.ScaleRoots                             instructions          -55.7%
+ ~Mathlib.RingTheory.Polynomial.Tower                                  instructions          -63.1%
+ ~Mathlib.RingTheory.Polynomial.Vieta                                  instructions          -74.9%
+ ~Mathlib.RingTheory.PolynomialAlgebra                                 instructions          -41.4%
+ ~Mathlib.RingTheory.PowerBasis                                        instructions          -52.3%
+ ~Mathlib.RingTheory.PowerSeries.Basic                                 instructions          -39.4%
+ ~Mathlib.RingTheory.PowerSeries.WellKnown                             instructions          -44.9%
+ ~Mathlib.RingTheory.RingHomProperties                                 instructions          -33.1%
+ ~Mathlib.RingTheory.RootsOfUnity.Basic                                instructions          -44.8%
+ ~Mathlib.RingTheory.Subring.Basic                                     instructions          -14.8%
+ ~Mathlib.RingTheory.Subsemiring.Basic                                 instructions          -18.2%
+ ~Mathlib.RingTheory.TensorProduct                                     instructions          -23.0%
+ ~Mathlib.RingTheory.Trace                                             instructions          -31.2%
+ ~Mathlib.RingTheory.UniqueFactorizationDomain                         instructions          -22.4%
+ ~Mathlib.RingTheory.Valuation.Basic                                   instructions          -82.4%
+ ~Mathlib.RingTheory.Valuation.Integers                                instructions          -77.0%
+ ~Mathlib.RingTheory.Valuation.ValuationRing                           instructions          -39.3%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring                        instructions          -29.4%
+ ~Mathlib.RingTheory.WittVector.Basic                                  instructions          -41.6%
+ ~Mathlib.RingTheory.WittVector.Compare                                instructions          -50.2%
+ ~Mathlib.RingTheory.WittVector.DiscreteValuationRing                  instructions          -52.4%
+ ~Mathlib.RingTheory.WittVector.Frobenius                              instructions          -46.0%
+ ~Mathlib.RingTheory.WittVector.FrobeniusFractionField                 instructions          -25.2%
+ ~Mathlib.RingTheory.WittVector.Identities                             instructions          -61.4%
+ ~Mathlib.RingTheory.WittVector.IsPoly                                 instructions          -44.3%
+ ~Mathlib.RingTheory.WittVector.Isocrystal                             instructions          -18.9%
+ ~Mathlib.RingTheory.WittVector.MulCoeff                               instructions          -33.8%
+ ~Mathlib.RingTheory.WittVector.StructurePolynomial                    instructions          -75.3%
+ ~Mathlib.RingTheory.WittVector.Teichmuller                            instructions          -42.8%
+ ~Mathlib.RingTheory.WittVector.Truncated                              instructions          -35.6%
+ ~Mathlib.RingTheory.WittVector.Verschiebung                           instructions          -63.6%
+ ~Mathlib.RingTheory.WittVector.WittPolynomial                         instructions          -36.9%
+ ~Mathlib.SetTheory.Cardinal.Basic                                     instructions          -36.4%
+ ~Mathlib.Topology.Algebra.Module.Basic                                instructions          -14.3%
+ ~Mathlib.Topology.Algebra.Module.FiniteDimension                      instructions          -15.8%
+ ~Mathlib.Topology.Algebra.UniformGroup                                instructions          -43.0%
+ ~Mathlib.Topology.Algebra.UniformRing                                 instructions          -21.0%
+ ~Mathlib.Topology.Algebra.Valuation                                   instructions          -76.8%
+ ~Mathlib.Topology.Algebra.ValuedField                                 instructions          -76.7%
+ ~Mathlib.Topology.Bornology.Constructions                             instructions          -61.7%
+ ~Mathlib.Topology.Category.Profinite.Nobeling                         instructions          -12.5%
+ ~Mathlib.Topology.Connected.PathConnected                             instructions          -19.6%
+ ~Mathlib.Topology.Constructions                                       instructions          -39.1%
+ ~Mathlib.Topology.ContinuousFunction.Algebra                          instructions          -19.8%
+ ~Mathlib.Topology.ContinuousFunction.Bounded                          instructions          -30.3%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass                 instructions          -13.3%
+ ~Mathlib.Topology.ContinuousFunction.Units                            instructions          -53.6%
+ ~Mathlib.Topology.ContinuousOn                                        instructions          -29.9%
+ ~Mathlib.Topology.Homotopy.HomotopyGroup                              instructions          -10.7%
+ ~Mathlib.Topology.Homotopy.Path                                       instructions          -13.9%
+ ~Mathlib.Topology.Instances.Complex                                   instructions          -32.8%
+ ~Mathlib.Topology.MetricSpace.GromovHausdorff                         instructions          -11.2%
+ ~Mathlib.Topology.MetricSpace.HausdorffDistance                       instructions          -45.2%
+ ~Mathlib.Topology.MetricSpace.Isometry                                instructions          -75.7%
+ ~Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections        instructions           -8.2%
- ~Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing                 instructions           40.9%
+ ~Mathlib.Topology.UniformSpace.Equiv                                  instructions          -60.7%

mattrobball · 2024-02-05T16:56:24Z

That I don't know yet!

Vierkantor · 2024-02-05T16:59:09Z

I should start cooking dinner soon. Could you take over for me for the next 2-3 hours? Or should I hope for the best and kick this PR on the queue?

mattrobball · 2024-02-05T17:04:26Z

I can kick it. If there are any serious issues, I will wait.

mattrobball · 2024-02-05T17:23:43Z

Mathlib, Archive, and Counterexamples all build and it lints. I am going to bump the priority to over 9000.

mattrobball · 2024-02-05T17:57:27Z

bors merge p=9001

mathlib-bors · 2024-02-05T17:57:39Z

👎 Rejected by label

mattrobball · 2024-02-05T17:58:11Z

bors merge p=9001

mathlib-bors · 2024-02-05T17:58:18Z

👎 Rejected by label

mattrobball · 2024-02-05T17:59:46Z

This isn’t blocked by anything. The label should have been removed.

bors merge p=9001

The FunLike hierarchy is very big and gets scanned through each time we need a coercion (via the `CoeFun` instance). It looks like unbundled inheritance suits Lean 4 better here. The only class that still extends `FunLike` is `EquivLike`, since that has a custom `coe_injective'` field that is easier to implement. All other classes should take `FunLike` or `EquivLike` as a parameter. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60example.20.28p.20.3A.20P.29.20.3A.20Q.20.3A.3D.20p.60.20takes.200.2E25s.20to.20fail!) ## Important changes Previously, morphism classes would be `Type`-valued and extend `FunLike`: ```lean /-- `MyHomClass F A B` states that `F` is a type of `MyClass.op`-preserving morphisms. You should extend this class when you extend `MyHom`. -/ class MyHomClass (F : Type*) (A B : outParam <| Type*) [MyClass A] [MyClass B] extends FunLike F A B := (map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y)) ``` After this PR, they should be `Prop`-valued and take `FunLike` as a parameter: ```lean /-- `MyHomClass F A B` states that `F` is a type of `MyClass.op`-preserving morphisms. You should extend this class when you extend `MyHom`. -/ class MyHomClass (F : Type*) (A B : outParam <| Type*) [MyClass A] [MyClass B] [FunLike F A B] : Prop := (map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y)) ``` (Note that `A B` stay marked as `outParam` even though they are not purely required to be so due to the `FunLike` parameter already filling them in. This is required to see through type synonyms, which is important in the category theory library. Also, I think keeping them as `outParam` is slightly faster.) Similarly, `MyEquivClass` should take `EquivLike` as a parameter. As a result, every mention of `[MyHomClass F A B]` should become `[FunLike F A B] [MyHomClass F A B]`. ## Remaining issues ### Slower (failing) search While overall this gives some great speedups, there are some cases that are noticeably slower. In particular, a *failing* application of a lemma such as `map_mul` is more expensive. This is due to suboptimal processing of arguments. For example: ```lean variable [FunLike F M N] [Mul M] [Mul N] (f : F) (x : M) (y : M) theorem map_mul [MulHomClass F M N] : f (x * y) = f x * f y example [AddHomClass F A B] : f (x * y) = f x * f y := map_mul f _ _ ``` Before this PR, applying `map_mul f` gives the goals `[Mul ?M] [Mul ?N] [MulHomClass F ?M ?N]`. Since `M` and `N` are `out_param`s, `[MulHomClass F ?M ?N]` is synthesized first, supplies values for `?M` and `?N` and then the `Mul M` and `Mul N` instances can be found. After this PR, the goals become `[FunLike F ?M ?N] [Mul ?M] [Mul ?N] [MulHomClass F ?M ?N]`. Now `[FunLike F ?M ?N]` is synthesized first, supplies values for `?M` and `?N` and then the `Mul M` and `Mul N` instances can be found, before trying `MulHomClass F M N` which *fails*. Since the `Mul` hierarchy is very big, this can be slow to fail, especially when there is no such `Mul` instance. A long-term but harder to achieve solution would be to specify the order in which instance goals get solved. For example, we'd like to change the arguments to `map_mul` to look like `[FunLike F M N] [Mul M] [Mul N] [highPriority <| MulHomClass F M N]` because `MulHomClass` fails or succeeds much faster than the others. As a consequence, the `simpNF` linter is much slower since by design it tries and fails to apply many `map_` lemmas. The same issue occurs a few times in existing calls to `simp [map_mul]`, where `map_mul` is tried "too soon" and fails. Thanks to the speedup of leanprover/lean4#2478 the impact is very limited, only in files that already were close to the timeout. ### `simp` not firing sometimes This affects `map_smulₛₗ` and related definitions. For `simp` lemmas Lean apparently uses a slightly different mechanism to find instances, so that `rw` can find every argument to `map_smulₛₗ` successfully but `simp` can't: leanprover/lean4#3701. ### Missing instances due to unification failing Especially in the category theory library, we might sometimes have a type `A` which is also accessible as a synonym `(Bundled A hA).1`. Instance synthesis doesn't always work if we have `f : A →* B` but `x * y : (Bundled A hA).1` or vice versa. This seems to be mostly fixed by keeping `A B` as `outParam`s in `MulHomClass F A B`. (Presumably because Lean will do a definitional check `A =?= (Bundled A hA).1` instead of using the syntax in the discrimination tree.) ## Workaround for issues The timeouts can be worked around for now by specifying which `map_mul` we mean, either as `map_mul f` for some explicit `f`, or as e.g. `MonoidHomClass.map_mul`. `map_smulₛₗ` not firing as `simp` lemma can be worked around by going back to the pre-FunLike situation and making `LinearMap.map_smulₛₗ` a `simp` lemma instead of the generic `map_smulₛₗ`. Writing `simp [map_smulₛₗ _]` also works. Co-authored-by: Matthew Ballard <[email protected]> Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Anne Baanen <[email protected]>

leanprover-community-mathlib4-bot · 2024-02-05T18:22:46Z

This PR/issue depends on:

~~[Merged by Bors] - chore(*): rename FunLike to DFunLike #9785~~
~~[Merged by Bors] - refactor(*): abbreviation for non-dependent FunLike #9833~~
By Dependent Issues (🤖). Happy coding!

mathlib-bors · 2024-02-05T18:23:35Z

Pull request successfully merged into master.

Build succeeded:

The FunLike hierarchy is very big and gets scanned through each time we need a coercion (via the `CoeFun` instance). It looks like unbundled inheritance suits Lean 4 better here. The only class that still extends `FunLike` is `EquivLike`, since that has a custom `coe_injective'` field that is easier to implement. All other classes should take `FunLike` or `EquivLike` as a parameter. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60example.20.28p.20.3A.20P.29.20.3A.20Q.20.3A.3D.20p.60.20takes.200.2E25s.20to.20fail!) ## Important changes Previously, morphism classes would be `Type`-valued and extend `FunLike`: ```lean /-- `MyHomClass F A B` states that `F` is a type of `MyClass.op`-preserving morphisms. You should extend this class when you extend `MyHom`. -/ class MyHomClass (F : Type*) (A B : outParam <| Type*) [MyClass A] [MyClass B] extends FunLike F A B := (map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y)) ``` After this PR, they should be `Prop`-valued and take `FunLike` as a parameter: ```lean /-- `MyHomClass F A B` states that `F` is a type of `MyClass.op`-preserving morphisms. You should extend this class when you extend `MyHom`. -/ class MyHomClass (F : Type*) (A B : outParam <| Type*) [MyClass A] [MyClass B] [FunLike F A B] : Prop := (map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y)) ``` (Note that `A B` stay marked as `outParam` even though they are not purely required to be so due to the `FunLike` parameter already filling them in. This is required to see through type synonyms, which is important in the category theory library. Also, I think keeping them as `outParam` is slightly faster.) Similarly, `MyEquivClass` should take `EquivLike` as a parameter. As a result, every mention of `[MyHomClass F A B]` should become `[FunLike F A B] [MyHomClass F A B]`. ## Remaining issues ### Slower (failing) search While overall this gives some great speedups, there are some cases that are noticeably slower. In particular, a *failing* application of a lemma such as `map_mul` is more expensive. This is due to suboptimal processing of arguments. For example: ```lean variable [FunLike F M N] [Mul M] [Mul N] (f : F) (x : M) (y : M) theorem map_mul [MulHomClass F M N] : f (x * y) = f x * f y example [AddHomClass F A B] : f (x * y) = f x * f y := map_mul f _ _ ``` Before this PR, applying `map_mul f` gives the goals `[Mul ?M] [Mul ?N] [MulHomClass F ?M ?N]`. Since `M` and `N` are `out_param`s, `[MulHomClass F ?M ?N]` is synthesized first, supplies values for `?M` and `?N` and then the `Mul M` and `Mul N` instances can be found. After this PR, the goals become `[FunLike F ?M ?N] [Mul ?M] [Mul ?N] [MulHomClass F ?M ?N]`. Now `[FunLike F ?M ?N]` is synthesized first, supplies values for `?M` and `?N` and then the `Mul M` and `Mul N` instances can be found, before trying `MulHomClass F M N` which *fails*. Since the `Mul` hierarchy is very big, this can be slow to fail, especially when there is no such `Mul` instance. A long-term but harder to achieve solution would be to specify the order in which instance goals get solved. For example, we'd like to change the arguments to `map_mul` to look like `[FunLike F M N] [Mul M] [Mul N] [highPriority <| MulHomClass F M N]` because `MulHomClass` fails or succeeds much faster than the others. As a consequence, the `simpNF` linter is much slower since by design it tries and fails to apply many `map_` lemmas. The same issue occurs a few times in existing calls to `simp [map_mul]`, where `map_mul` is tried "too soon" and fails. Thanks to the speedup of leanprover/lean4#2478 the impact is very limited, only in files that already were close to the timeout. ### `simp` not firing sometimes This affects `map_smulₛₗ` and related definitions. For `simp` lemmas Lean apparently uses a slightly different mechanism to find instances, so that `rw` can find every argument to `map_smulₛₗ` successfully but `simp` can't: leanprover/lean4#3701. ### Missing instances due to unification failing Especially in the category theory library, we might sometimes have a type `A` which is also accessible as a synonym `(Bundled A hA).1`. Instance synthesis doesn't always work if we have `f : A →* B` but `x * y : (Bundled A hA).1` or vice versa. This seems to be mostly fixed by keeping `A B` as `outParam`s in `MulHomClass F A B`. (Presumably because Lean will do a definitional check `A =?= (Bundled A hA).1` instead of using the syntax in the discrimination tree.) ## Workaround for issues The timeouts can be worked around for now by specifying which `map_mul` we mean, either as `map_mul f` for some explicit `f`, or as e.g. `MonoidHomClass.map_mul`. `map_smulₛₗ` not firing as `simp` lemma can be worked around by going back to the pre-FunLike situation and making `LinearMap.map_smulₛₗ` a `simp` lemma instead of the generic `map_smulₛₗ`. Writing `simp [map_smulₛₗ _]` also works. Co-authored-by: Matthew Ballard <[email protected]> Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Anne Baanen <[email protected]>

@Vierkantor

Fully update the module docstrings (in particular, the examples given therein) after #8386. This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301. Co-authored-by: @Vierkantor Co-authored-by: Vierkantor <[email protected]>

@Vierkantor

Fully update the module docstrings (in particular, the examples given therein) after #8386. This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301. Co-authored-by: @Vierkantor Co-authored-by: Vierkantor <[email protected]>

@Vierkantor

Fully update the module docstrings (in particular, the examples given therein) after #8386. This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301. Co-authored-by: @Vierkantor Co-authored-by: Vierkantor <[email protected]>

@Vierkantor

Fully update the module docstrings (in particular, the examples given therein) after #8386. This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301. Co-authored-by: @Vierkantor Co-authored-by: Vierkantor <[email protected]>

@Vierkantor

Fully update the module docstrings (in particular, the examples given therein) after #8386. This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301. Co-authored-by: @Vierkantor Co-authored-by: Vierkantor <[email protected]>

@Vierkantor

Fully update the module docstrings (in particular, the examples given therein) after #8386. This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301. Co-authored-by: @Vierkantor Co-authored-by: Vierkantor <[email protected]>

@Vierkantor

Fully update the module docstrings (in particular, the examples given therein) after #8386. This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301. Co-authored-by: @Vierkantor Co-authored-by: Vierkantor <[email protected]>

Vierkantor added the WIP Work in progress label Nov 13, 2023

github-actions bot reviewed Nov 13, 2023

View reviewed changes

Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean Outdated Show resolved Hide resolved

Vierkantor force-pushed the unbundled-FunLike branch 3 times, most recently from d55c9bc to d54859d Compare November 20, 2023 18:18

Vierkantor force-pushed the unbundled-FunLike branch 3 times, most recently from 79e30f2 to b47ee0f Compare November 27, 2023 17:49

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 29, 2023

Vierkantor force-pushed the unbundled-FunLike branch from 485e90d to 377b006 Compare December 1, 2023 16:38

leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Dec 1, 2023

Vierkantor force-pushed the unbundled-FunLike branch from 377b006 to e9d204f Compare December 6, 2023 10:53

leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Dec 6, 2023

Vierkantor force-pushed the unbundled-FunLike branch from c485120 to b71c141 Compare December 6, 2023 17:22

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 6, 2023

Vierkantor force-pushed the unbundled-FunLike branch from b71c141 to a20114c Compare December 8, 2023 16:18

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 11, 2023

Vierkantor force-pushed the unbundled-FunLike branch from a20114c to 1234b55 Compare December 11, 2023 11:47

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 11, 2023

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 13, 2023

Vierkantor force-pushed the unbundled-FunLike branch from c9faf41 to fcb0306 Compare December 20, 2023 11:04

github-actions bot added the ready-to-merge This PR has been sent to bors. label Feb 5, 2024

mattrobball removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Feb 5, 2024

leanprover-community-mathlib4-bot added blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) labels Feb 5, 2024

mathlib-bors bot changed the title ~~refactor(Data/FunLike): use unbundled inheritance from FunLike~~ [Merged by Bors] - refactor(Data/FunLike): use unbundled inheritance from FunLike Feb 5, 2024

mathlib-bors bot closed this Feb 5, 2024

mathlib-bors bot deleted the unbundled-FunLike branch February 5, 2024 18:23

PatrickMassot mentioned this pull request Feb 5, 2024

FunLike update avigad/mathematics_in_lean_source#179

Open

grunweg mentioned this pull request Mar 18, 2024

[Merged by Bors] - chore(Data/Funlike): update examples and replace Lean 3 syntax #11409

Closed

kim-em mentioned this pull request Jun 26, 2024

feat: weaken CoeFun -> CoeOut instance to -> CoeOTC leanprover/lean4#2869

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(Data/FunLike): use unbundled inheritance from FunLike #8386

[Merged by Bors] - refactor(Data/FunLike): use unbundled inheritance from FunLike #8386

Vierkantor commented Nov 13, 2023 •

edited by mattrobball

Loading

Vierkantor commented Dec 6, 2023

leanprover-bot commented Dec 6, 2023

Vierkantor commented Dec 6, 2023

Vierkantor commented Dec 11, 2023

leanprover-bot commented Dec 11, 2023

mattrobball commented Feb 5, 2024

Vierkantor commented Feb 5, 2024

mattrobball commented Feb 5, 2024

mattrobball commented Feb 5, 2024

mattrobball commented Feb 5, 2024

mathlib-bors bot commented Feb 5, 2024

mattrobball commented Feb 5, 2024

mathlib-bors bot commented Feb 5, 2024

mattrobball commented Feb 5, 2024

leanprover-community-mathlib4-bot commented Feb 5, 2024

mathlib-bors bot commented Feb 5, 2024

[Merged by Bors] - refactor(Data/FunLike): use unbundled inheritance from FunLike #8386

[Merged by Bors] - refactor(Data/FunLike): use unbundled inheritance from FunLike #8386

Conversation

Vierkantor commented Nov 13, 2023 • edited by mattrobball Loading

Important changes

Remaining issues

Slower (failing) search

simp not firing sometimes

Missing instances due to unification failing

Workaround for issues

Vierkantor commented Dec 6, 2023

leanprover-bot commented Dec 6, 2023

Vierkantor commented Dec 6, 2023

Vierkantor commented Dec 11, 2023

leanprover-bot commented Dec 11, 2023

mattrobball commented Feb 5, 2024

Vierkantor commented Feb 5, 2024

mattrobball commented Feb 5, 2024

mattrobball commented Feb 5, 2024

mattrobball commented Feb 5, 2024

mathlib-bors bot commented Feb 5, 2024

mattrobball commented Feb 5, 2024

mathlib-bors bot commented Feb 5, 2024

mattrobball commented Feb 5, 2024

leanprover-community-mathlib4-bot commented Feb 5, 2024

mathlib-bors bot commented Feb 5, 2024

Vierkantor commented Nov 13, 2023 •

edited by mattrobball

Loading

`simp` not firing sometimes