Lean pr testing 7717 by kmill · Pull Request #23445 · leanprover-community/mathlib4

kmill · 2025-03-30T05:51:23Z

kmill · 2025-03-30T05:51:42Z

!bench

leanprover-bot · 2025-03-30T06:18:46Z

Here are the benchmark results for commit 2eb925d.
There were significant changes against commit 0723456:

  Benchmark                                                                Metric         Change
  ==============================================================================================
+ ~Mathlib.Algebra.Category.ModuleCat.Algebra                              instructions   -49.4%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings                        instructions    -8.7%
+ ~Mathlib.Algebra.Category.ModuleCat.Presheaf                             instructions    -5.9%
- ~Mathlib.Algebra.Category.ModuleCat.Presheaf.Free                        instructions   318.4%
+ ~Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification              instructions   -17.6%
+ ~Mathlib.Algebra.Category.Ring.Limits                                    instructions   -27.8%
+ ~Mathlib.Algebra.Field.Basic                                             instructions   -56.0%
+ ~Mathlib.Algebra.Homology.AlternatingConst                               instructions   -37.1%
- ~Mathlib.Algebra.Module.ZLattice.Basic                                   instructions    15.8%
+ ~Mathlib.Algebra.Order.Field.Defs                                        instructions   -74.5%
+ ~Mathlib.Algebra.Quaternion                                              instructions    -7.8%
+ ~Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme                     instructions    -8.3%
+ ~Mathlib.AlgebraicGeometry.StructureSheaf                                instructions   -13.4%
+ ~Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject                 instructions   -40.4%
+ ~Mathlib.AlgebraicTopology.SimplicialObject.Basic                        instructions   -13.7%
- ~Mathlib.Analysis.CStarAlgebra.Classes                                   instructions    33.6%
- ~Mathlib.Analysis.CStarAlgebra.lpSpace                                   instructions    41.3%
+ ~Mathlib.Analysis.Normed.Affine.Isometry                                 instructions   -13.2%
+ ~Mathlib.Analysis.Quaternion                                             instructions   -28.4%
+ ~Mathlib.CategoryTheory.Adjunction.Evaluation                            instructions   -18.8%
+ ~Mathlib.CategoryTheory.Bicategory.Coherence                             instructions   -30.8%
+ ~Mathlib.CategoryTheory.Bicategory.Free                                  instructions   -56.2%
+ ~Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete               instructions   -53.3%
- ~Mathlib.CategoryTheory.Closed.FunctorToTypes                            instructions    55.5%
+ ~Mathlib.CategoryTheory.Comma.Basic                                      instructions    -8.4%
+ ~Mathlib.CategoryTheory.Comma.Over.Basic                                 instructions    -5.0%
+ ~Mathlib.CategoryTheory.Comma.StructuredArrow.Basic                      instructions    -8.3%
+ ~Mathlib.CategoryTheory.Comma.StructuredArrow.Functor                    instructions   -22.1%
+ ~Mathlib.CategoryTheory.DifferentialObject                               instructions   -18.6%
+ ~Mathlib.CategoryTheory.Elements                                         instructions   -23.1%
+ ~Mathlib.CategoryTheory.Functor.Currying                                 instructions   -13.5%
+ ~Mathlib.CategoryTheory.Functor.Trifunctor                               instructions   -13.8%
+ ~Mathlib.CategoryTheory.GradedObject.Trifunctor                          instructions   -11.0%
+ ~Mathlib.CategoryTheory.Groupoid.Subgroupoid                             instructions   -30.9%
+ ~Mathlib.CategoryTheory.Limits.ConeCategory                              instructions   -21.4%
+ ~Mathlib.CategoryTheory.Limits.Final                                     instructions    -6.3%
+ ~Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer                     instructions   -13.2%
+ ~Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor   instructions   -22.8%
+ ~Mathlib.CategoryTheory.Monoidal.Category                                instructions   -17.3%
+ ~Mathlib.CategoryTheory.Monoidal.CommMon_                                instructions   -11.6%
+ ~Mathlib.CategoryTheory.Monoidal.Comon_                                  instructions   -15.9%
+ ~Mathlib.CategoryTheory.Monoidal.Discrete                                instructions   -35.7%
+ ~Mathlib.CategoryTheory.Monoidal.Mon_                                    instructions   -14.9%
+ ~Mathlib.CategoryTheory.Preadditive.CommGrp_                             instructions   -24.9%
+ ~Mathlib.CategoryTheory.Sites.Sheaf                                      instructions   -18.2%
+ ~Mathlib.CategoryTheory.Triangulated.Opposite.Triangle                   instructions   -17.1%
+ ~Mathlib.CategoryTheory.Whiskering                                       instructions   -10.9%
- ~Mathlib.CategoryTheory.WithTerminal                                     instructions     6.3%
+ ~Mathlib.Data.ZMod.Defs                                                  instructions   -76.1%
+ ~Mathlib.FieldTheory.RatFunc.Basic                                       instructions    -6.5%
- ~Mathlib.LinearAlgebra.CliffordAlgebra.Even                              instructions    14.7%
- ~Mathlib.LinearAlgebra.Dual.Lemmas                                       instructions     5.7%
- ~Mathlib.LinearAlgebra.Eigenspace.Basic                                  instructions     9.8%
- ~Mathlib.LinearAlgebra.Goursat                                           instructions    38.7%
- ~Mathlib.LinearAlgebra.Isomorphisms                                      instructions    55.2%
+ ~Mathlib.LinearAlgebra.RootSystem.BaseChange                             instructions   -42.6%
- ~Mathlib.LinearAlgebra.TensorProduct.Graded.Internal                     instructions    74.1%
- ~Mathlib.NumberTheory.NumberField.FractionalIdeal                        instructions    36.5%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Basic                      instructions   -15.7%
- ~Mathlib.RingTheory.AdicCompletion.AsTensorProduct                       instructions    11.0%
- ~Mathlib.RingTheory.GradedAlgebra.Basic                                  instructions    23.4%
- ~Mathlib.RingTheory.Ideal.Quotient.Operations                            instructions     8.5%
+ ~Mathlib.RingTheory.IntegralClosure.IntegralRestrict                     instructions    -3.8%
+ ~Mathlib.RingTheory.Kaehler.JacobiZariski                                instructions    -7.8%
+ ~Mathlib.RingTheory.Kaehler.Polynomial                                   instructions    -7.6%
+ ~Mathlib.RingTheory.LaurentSeries                                        instructions    -7.7%
+ ~Mathlib.RingTheory.LocalRing.ResidueField.Ideal                         instructions   -11.9%
- ~Mathlib.RingTheory.SimpleModule.Basic                                   instructions    28.3%
+ ~Mathlib.SetTheory.Surreal.Multiplication                                instructions   -38.7%
+ ~Mathlib.Topology.Algebra.UniformRing                                    instructions   -33.4%
+ ~Mathlib.Topology.MetricSpace.GromovHausdorff                            instructions   -26.5%
+ ~Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts               instructions    -9.6%

github-actions · 2025-03-30T06:19:10Z

File	Instructions	%
`build`	-1653.190⬝10⁹	(-0.99%)
`lint`	+21.278⬝10⁹	(+0.28%)
`Mathlib.Algebra.Category.ModuleCat.Presheaf.Free`	+163.483⬝10⁹	(+318.43%)
`Mathlib.LinearAlgebra.TensorProduct.Graded.Internal`	+141.555⬝10⁹	(+74.08%)
`Mathlib.CategoryTheory.WithTerminal`	+23.11⬝10⁹	(+6.30%)
`Mathlib.RingTheory.AdicCompletion.AsTensorProduct`	+22.789⬝10⁹	(+11.03%)
`Mathlib.Algebra.Module.ZLattice.Basic`	+21.876⬝10⁹	(+15.75%)
`Mathlib.RingTheory.SimpleModule.Basic`	+19.3⬝10⁹	(+28.27%)

2 files, Instructions +18.0⬝10⁹

File	Instructions	%
`Mathlib.LinearAlgebra.Isomorphisms`	+18.682⬝10⁹	(+55.22%)
`Mathlib.LinearAlgebra.Dual.Lemmas`	+18.397⬝10⁹	(+5.68%)

File	Instructions	%
`Mathlib.LinearAlgebra.Goursat`	+16.345⬝10⁹	(+38.73%)
`Mathlib.RingTheory.Ideal.Quotient.Operations`	+13.436⬝10⁹	(+8.46%)

4 files, Instructions +12.0⬝10⁹

File	Instructions	%
`Mathlib.LinearAlgebra.CliffordAlgebra.Even`	+12.919⬝10⁹	(+14.66%)
`Mathlib.Analysis.CStarAlgebra.Classes`	+12.802⬝10⁹	(+33.55%)
`Mathlib.LinearAlgebra.Eigenspace.Basic`	+12.182⬝10⁹	(+9.82%)
`Mathlib.Analysis.CStarAlgebra.lpSpace`	+12.139⬝10⁹	(+41.31%)

File	Instructions	%
`Mathlib.NumberTheory.NumberField.FractionalIdeal`	+11.585⬝10⁹	(+36.47%)

2 files, Instructions +10.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.Closed.FunctorToTypes`	+10.841⬝10⁹	(+55.53%)
`Mathlib.RingTheory.GradedAlgebra.Basic`	+10.545⬝10⁹	(+23.35%)

5 files, Instructions +9.0⬝10⁹

File	Instructions	%
`Mathlib.RepresentationTheory.GroupCohomology.Functoriality`	+9.880⬝10⁹	(+5.54%)
`Mathlib.Geometry.Euclidean.Circumcenter`	+9.878⬝10⁹	(+12.52%)
`Mathlib.Geometry.Euclidean.Basic`	+9.772⬝10⁹	(+17.34%)
`Mathlib.Algebra.Order.Ring.Defs`	+9.457⬝10⁹	(+48.14%)
`Mathlib.LinearAlgebra.ExteriorPower.Basic`	+9.272⬝10⁹	(+8.08%)

File	Instructions	%
`Mathlib.RepresentationTheory.GroupCohomology.LowDegree`	+8.701⬝10⁹	(+4.99%)

9 files, Instructions +7.0⬝10⁹

File	Instructions	%
`Mathlib.LinearAlgebra.Eigenspace.Pi`	+7.852⬝10⁹	(+25.43%)
`Mathlib.LinearAlgebra.FiniteDimensional.Basic`	+7.798⬝10⁹	(+15.28%)
`Mathlib.Analysis.InnerProductSpace.PiL2`	+7.764⬝10⁹	(+3.75%)
`Mathlib.CategoryTheory.Adjunction.PartialAdjoint`	+7.419⬝10⁹	(+12.51%)
`Mathlib.CategoryTheory.Sites.SheafHom`	+7.254⬝10⁹	(+19.83%)
`Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors`	+7.212⬝10⁹	(+21.64%)
`Mathlib.RingTheory.Flat.Equalizer`	+7.175⬝10⁹	(+3.31%)
`Mathlib.Geometry.Manifold.Instances.Sphere`	+7.175⬝10⁹	(+5.43%)
`Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional`	+7.23⬝10⁹	(+16.01%)

7 files, Instructions +6.0⬝10⁹

File	Instructions	%
`Mathlib.NumberTheory.RamificationInertia.Basic`	+6.864⬝10⁹	(+3.38%)
`Mathlib.RingTheory.Flat.FaithfullyFlat.Basic`	+6.837⬝10⁹	(+9.43%)
`Mathlib.Analysis.InnerProductSpace.Projection`	+6.550⬝10⁹	(+3.47%)
`Mathlib.Algebra.Homology.ShortComplex.ModuleCat`	+6.449⬝10⁹	(+6.68%)
`Mathlib.Analysis.Normed.Ring.Basic`	+6.290⬝10⁹	(+7.72%)
`Mathlib.RingTheory.Ideal.Cotangent`	+6.59⬝10⁹	(+7.24%)
`Mathlib.RingTheory.Bialgebra.TensorProduct`	+6.30⬝10⁹	(+3.75%)

10 files, Instructions +5.0⬝10⁹

File	Instructions	%
`Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic`	+5.945⬝10⁹	(+11.06%)
`Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem`	+5.846⬝10⁹	(+22.25%)
`Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries`	+5.796⬝10⁹	(+1.94%)
`Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient`	+5.682⬝10⁹	(+36.00%)
`Mathlib.LinearAlgebra.Dimension.RankNullity`	+5.654⬝10⁹	(+18.61%)
`Mathlib.LinearAlgebra.Semisimple`	+5.495⬝10⁹	(+4.75%)
`Mathlib.Algebra.Module.ZLattice.Covolume`	+5.399⬝10⁹	(+7.76%)
`Mathlib.LinearAlgebra.LinearDisjoint`	+5.358⬝10⁹	(+5.87%)
`Mathlib.RingTheory.LocalRing.Module`	+5.157⬝10⁹	(+5.85%)
`Mathlib.Analysis.NormedSpace.HahnBanach.Extension`	+5.111⬝10⁹	(+10.90%)

14 files, Instructions +4.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.CStarAlgebra.GelfandDuality`	+4.826⬝10⁹	(+6.47%)
`Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic`	+4.736⬝10⁹	(+1.97%)
`Mathlib.Analysis.Normed.Operator.LinearIsometry`	+4.652⬝10⁹	(+2.49%)
`Mathlib.RingTheory.FiniteType`	+4.638⬝10⁹	(+9.49%)
`Mathlib.CategoryTheory.MorphismProperty.Factorization`	+4.594⬝10⁹	(+8.44%)
`Mathlib.LinearAlgebra.FreeModule.PID`	+4.580⬝10⁹	(+6.34%)
`Mathlib.Analysis.Normed.Ring.Lemmas`	+4.565⬝10⁹	(+34.65%)
`Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear`	+4.452⬝10⁹	(+2.28%)
`Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous`	+4.449⬝10⁹	(+7.76%)
`Mathlib.LinearAlgebra.Eigenspace.Zero`	+4.407⬝10⁹	(+14.79%)
`Mathlib.Algebra.Order.Ring.InjSurj`	+4.273⬝10⁹	(+21.82%)
`Mathlib.RingTheory.FiniteLength`	+4.116⬝10⁹	(+30.70%)
`Mathlib.Algebra.Category.Grp.Colimits`	+4.84⬝10⁹	(+4.09%)
`Mathlib.AlgebraicGeometry.Modules.Tilde`	+4.62⬝10⁹	(+2.74%)

16 files, Instructions +3.0⬝10⁹

File	Instructions	%
`Mathlib.Condensed.Discrete.Module`	+3.947⬝10⁹	(+3.89%)
`Mathlib.RingTheory.Smooth.StandardSmooth`	+3.918⬝10⁹	(+6.65%)
`Mathlib.Algebra.Homology.BifunctorShift`	+3.818⬝10⁹	(+4.23%)
`Aesop.Search.Expansion`	+3.785⬝10⁹	(+13.61%)
`Mathlib.Algebra.Ring.InjSurj`	+3.702⬝10⁹	(+18.14%)
`Mathlib.Algebra.Homology.TotalComplexShift`	+3.670⬝10⁹	(+5.09%)
`Mathlib.Algebra.Category.ModuleCat.Subobject`	+3.510⬝10⁹	(+27.32%)
`Mathlib.Analysis.InnerProductSpace.Adjoint`	+3.475⬝10⁹	(+1.42%)
`Mathlib.RingTheory.OreLocalization.Ring`	+3.399⬝10⁹	(+10.07%)
`Mathlib.Analysis.Normed.Module.Complemented`	+3.330⬝10⁹	(+10.39%)
`Mathlib.Topology.ContinuousMap.ZeroAtInfty`	+3.322⬝10⁹	(+6.52%)
`Mathlib.Algebra.Module.PID`	+3.237⬝10⁹	(+5.48%)
`Mathlib.Analysis.Normed.Module.Dual`	+3.147⬝10⁹	(+3.78%)
`Mathlib.Algebra.DirectSum.LinearMap`	+3.135⬝10⁹	(+9.41%)
`Mathlib.RingTheory.FractionalIdeal.Norm`	+3.121⬝10⁹	(+7.90%)
`Mathlib.Analysis.Normed.Operator.Banach`	+3.67⬝10⁹	(+2.60%)

38 files, Instructions +2.0⬝10⁹

File	Instructions	%
`Mathlib.LinearAlgebra.Basis.Submodule`	+2.966⬝10⁹	(+10.38%)
`Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm`	+2.963⬝10⁹	(+1.59%)
`Mathlib.LinearAlgebra.Eigenspace.Semisimple`	+2.936⬝10⁹	(+20.22%)
`Mathlib.LinearAlgebra.TensorProduct.RightExactness`	+2.881⬝10⁹	(+2.54%)
`Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody`	+2.863⬝10⁹	(+2.44%)
`Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno`	+2.786⬝10⁹	(+1.16%)
`Mathlib.LinearAlgebra.PerfectPairing.Restrict`	+2.768⬝10⁹	(+3.76%)
`Mathlib.Analysis.Normed.Module.FiniteDimension`	+2.721⬝10⁹	(+2.61%)
`Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation`	+2.716⬝10⁹	(+1.51%)
`Mathlib.LinearAlgebra.FiniteDimensional.Lemmas`	+2.688⬝10⁹	(+8.95%)
`Mathlib.Algebra.Category.ModuleCat.ExteriorPower`	+2.684⬝10⁹	(+14.33%)
`Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient`	+2.641⬝10⁹	(+16.44%)
`Mathlib.RingTheory.Smooth.Kaehler`	+2.636⬝10⁹	(+0.85%)
`Mathlib.Algebra.Order.Kleene`	+2.559⬝10⁹	(+17.61%)
`Mathlib.LinearAlgebra.Basis.VectorSpace`	+2.558⬝10⁹	(+10.97%)
`Mathlib.RingTheory.Flat.Basic`	+2.525⬝10⁹	(+3.65%)
`Mathlib.LinearAlgebra.AffineSpace.Restrict`	+2.511⬝10⁹	(+26.62%)
`Mathlib.FieldTheory.CardinalEmb`	+2.506⬝10⁹	(+0.82%)
`Mathlib.RingTheory.Ideal.Quotient.Index`	+2.503⬝10⁹	(+11.92%)
`Mathlib.Algebra.Ring.Pi`	+2.471⬝10⁹	(+27.22%)
`Mathlib.Order.Filter.FilterProduct`	+2.470⬝10⁹	(+19.67%)
`Mathlib.Topology.ContinuousMap.Bounded.Basic`	+2.460⬝10⁹	(+2.19%)
`Mathlib.Algebra.Field.ULift`	+2.449⬝10⁹	(+48.34%)
`Mathlib.LinearAlgebra.Projection`	+2.410⬝10⁹	(+3.54%)
`Mathlib.Topology.Algebra.Module.FiniteDimension`	+2.393⬝10⁹	(+2.09%)
`Mathlib.Analysis.Calculus.Implicit`	+2.388⬝10⁹	(+1.80%)
`Mathlib.MeasureTheory.Measure.Haar.Disintegration`	+2.383⬝10⁹	(+4.40%)
`Mathlib.LinearAlgebra.Eigenspace.Triangularizable`	+2.348⬝10⁹	(+8.90%)
`Mathlib.NumberTheory.NumberField.Units.DirichletTheorem`	+2.344⬝10⁹	(+2.53%)
`Mathlib.Analysis.Matrix`	+2.340⬝10⁹	(+4.17%)
`Mathlib.LinearAlgebra.Dimension.StrongRankCondition`	+2.330⬝10⁹	(+8.50%)
`Mathlib.Algebra.Lie.TraceForm`	+2.231⬝10⁹	(+1.23%)
`Mathlib.Order.Heyting.Regular`	+2.219⬝10⁹	(+24.83%)
`Mathlib.Analysis.Calculus.FDeriv.Analytic`	+2.186⬝10⁹	(+0.75%)
`Mathlib.Analysis.CStarAlgebra.Unitization`	+2.158⬝10⁹	(+3.78%)
`Mathlib.Analysis.CStarAlgebra.ContinuousMap`	+2.139⬝10⁹	(+6.16%)
`Mathlib.Geometry.Manifold.MFDeriv.NormedSpace`	+2.0⬝10⁹	(+0.90%)
`Mathlib.CategoryTheory.Sites.SheafCohomology.Basic`	+2.0⬝10⁹	(+19.03%)

64 files, Instructions +1.0⬝10⁹

File	Instructions	%
`Mathlib.LinearAlgebra.TensorAlgebra.Grading`	+1.957⬝10⁹	(+14.39%)
`Mathlib.LinearAlgebra.Trace`	+1.910⬝10⁹	(+2.43%)
`Mathlib.RingTheory.Artinian.Module`	+1.862⬝10⁹	(+3.78%)
`Mathlib.LinearAlgebra.FiniteDimensional.Defs`	+1.807⬝10⁹	(+11.69%)
`Mathlib.RingTheory.PiTensorProduct`	+1.754⬝10⁹	(+2.05%)
`Mathlib.LinearAlgebra.ExteriorAlgebra.Grading`	+1.733⬝10⁹	(+2.93%)
`Mathlib.Analysis.Normed.Module.Span`	+1.720⬝10⁹	(+9.30%)
`Mathlib.Algebra.Order.Pi`	+1.688⬝10⁹	(+18.04%)
`Mathlib.RingTheory.IntegralClosure.Algebra.Basic`	+1.675⬝10⁹	(+6.66%)
`Mathlib.Analysis.Analytic.ChangeOrigin`	+1.666⬝10⁹	(+1.48%)
`Mathlib.Analysis.Calculus.FDeriv.Mul`	+1.664⬝10⁹	(+0.37%)
`Mathlib.Algebra.Lie.Weights.Killing`	+1.661⬝10⁹	(+0.80%)
`Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition`	+1.649⬝10⁹	(+4.96%)
`Mathlib.Order.Filter.Germ.Basic`	+1.632⬝10⁹	(+6.55%)
`Mathlib.Algebra.Category.ModuleCat.Abelian`	+1.623⬝10⁹	(+7.31%)
`Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap`	+1.622⬝10⁹	(+20.96%)
`Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous`	+1.620⬝10⁹	(+4.38%)
`Mathlib.Algebra.Colimit.Ring`	+1.591⬝10⁹	(+1.81%)
`Mathlib.Analysis.Normed.Module.Basic`	+1.588⬝10⁹	(+2.84%)
`Mathlib.RingTheory.Ideal.Norm.AbsNorm`	+1.576⬝10⁹	(+2.56%)
`Mathlib.Data.Matrix.Mul`	+1.569⬝10⁹	(+3.09%)
`Mathlib.CategoryTheory.Localization.Trifunctor`	+1.567⬝10⁹	(+1.41%)
`Mathlib.Algebra.MonoidAlgebra.Grading`	+1.551⬝10⁹	(+4.87%)
`Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric`	+1.542⬝10⁹	(+8.07%)
`Mathlib.Algebra.Lie.Weights.RootSystem`	+1.520⬝10⁹	(+0.94%)
`Mathlib.Algebra.Category.AlgebraCat.Symmetric`	+1.519⬝10⁹	(+8.95%)
`Mathlib.LinearAlgebra.SesquilinearForm`	+1.515⬝10⁹	(+1.06%)
`Mathlib.Algebra.Category.Ring.FilteredColimits`	+1.512⬝10⁹	(+3.20%)
`Mathlib.RingTheory.Noetherian.Basic`	+1.499⬝10⁹	(+5.95%)
`Mathlib.Algebra.Ring.Opposite`	+1.485⬝10⁹	(+13.30%)
`Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable`	+1.472⬝10⁹	(+2.97%)
`Mathlib.LinearAlgebra.TensorProduct.Vanishing`	+1.437⬝10⁹	(+3.74%)
`Aesop.Search.Main`	+1.426⬝10⁹	(+1.33%)
`Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject`	+1.421⬝10⁹	(+5.83%)
`Mathlib.Analysis.InnerProductSpace.Spectrum`	+1.416⬝10⁹	(+3.43%)
`Mathlib.Algebra.Lie.LieTheorem`	+1.411⬝10⁹	(+1.82%)
`Mathlib.Analysis.InnerProductSpace.Subspace`	+1.406⬝10⁹	(+4.98%)
`Mathlib.RingTheory.HopkinsLevitzki`	+1.391⬝10⁹	(+4.57%)
`Mathlib.RingTheory.LinearDisjoint`	+1.375⬝10⁹	(+0.68%)
`Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu`	+1.366⬝10⁹	(+2.71%)
`Mathlib.Topology.ContinuousMap.Ideals`	+1.334⬝10⁹	(+2.05%)
`Mathlib.LinearAlgebra.Multilinear.DFinsupp`	+1.307⬝10⁹	(+7.85%)
`Mathlib.RingTheory.Jacobson.Semiprimary`	+1.279⬝10⁹	(+11.88%)
`Mathlib.Analysis.InnerProductSpace.Dual`	+1.252⬝10⁹	(+2.18%)
`Mathlib.LinearAlgebra.FreeModule.Int`	+1.246⬝10⁹	(+3.99%)
`Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1`	+1.236⬝10⁹	(+1.49%)
`Mathlib.Algebra.Module.Lattice`	+1.234⬝10⁹	(+4.58%)
`Mathlib.NumberTheory.ArithmeticFunction`	+1.232⬝10⁹	(+1.63%)
`Mathlib.CategoryTheory.ChosenFiniteProducts`	+1.230⬝10⁹	(+2.32%)
`Mathlib.Algebra.Order.Ring.Prod`	+1.212⬝10⁹	(+29.07%)
`Mathlib.LinearAlgebra.BilinearForm.Orthogonal`	+1.155⬝10⁹	(+2.40%)
`Mathlib.Algebra.Category.ModuleCat.Images`	+1.129⬝10⁹	(+8.44%)
`Mathlib.Algebra.Category.ModuleCat.Kernels`	+1.118⬝10⁹	(+5.24%)
`Mathlib.LinearAlgebra.LinearIndependent.Defs`	+1.93⬝10⁹	(+2.33%)
`Mathlib.CategoryTheory.MorphismProperty.OverAdjunction`	+1.86⬝10⁹	(+1.05%)
`Mathlib.Algebra.Module.Torsion`	+1.82⬝10⁹	(+1.28%)
`Mathlib.Tactic.NormNum.Pow`	+1.80⬝10⁹	(+4.99%)
`Mathlib.Analysis.Normed.Group.Constructions`	+1.62⬝10⁹	(+6.08%)
`Mathlib.Algebra.Lie.TensorProduct`	+1.44⬝10⁹	(+1.63%)
`Mathlib.Algebra.Category.Grp.LeftExactFunctor`	+1.43⬝10⁹	(+1.70%)
`Mathlib.LinearAlgebra.FreeModule.Finite.Quotient`	+1.23⬝10⁹	(+5.56%)
`Mathlib.Algebra.Field.Opposite`	+1.22⬝10⁹	(+15.89%)
`Mathlib.LinearAlgebra.Basis.Fin`	+1.6⬝10⁹	(+8.70%)
`Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra`	+1.5⬝10⁹	(+4.43%)

190 files, Instructions -2.0⬝10⁹

File	Instructions	%
`Mathlib.LinearAlgebra.Matrix.SesquilinearForm`	-1.3⬝10⁹	(-0.72%)
`Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc`	-1.6⬝10⁹	(-4.36%)
`Mathlib.SetTheory.Surreal.Basic`	-1.7⬝10⁹	(-5.35%)
`Mathlib.Algebra.Module.LinearMap.Defs`	-1.8⬝10⁹	(-1.78%)
`Mathlib.NumberTheory.LucasLehmer`	-1.8⬝10⁹	(-2.23%)
`Mathlib.Algebra.Algebra.Pi`	-1.18⬝10⁹	(-9.84%)
`Mathlib.Algebra.Ring.Subsemiring.Basic`	-1.19⬝10⁹	(-2.53%)
`Mathlib.Data.Complex.Trigonometric`	-1.19⬝10⁹	(-1.29%)
`Mathlib.Analysis.Normed.Module.Completion`	-1.22⬝10⁹	(-6.81%)
`Mathlib.Analysis.Normed.Unbundled.AlgebraNorm`	-1.32⬝10⁹	(-5.46%)
`Mathlib.RingTheory.Polynomial.Basic`	-1.37⬝10⁹	(-1.52%)
`Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks`	-1.37⬝10⁹	(-2.04%)
`Mathlib.Analysis.SpecialFunctions.Pow.Deriv`	-1.39⬝10⁹	(-0.86%)
`Mathlib.Algebra.Algebra.Basic`	-1.41⬝10⁹	(-3.21%)
`Mathlib.RingTheory.Morita.Basic`	-1.42⬝10⁹	(-5.62%)
`Mathlib.Topology.Gluing`	-1.43⬝10⁹	(-2.24%)
`Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap`	-1.44⬝10⁹	(-2.72%)
`Mathlib.Geometry.Manifold.DerivationBundle`	-1.45⬝10⁹	(-1.65%)
`Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp`	-1.46⬝10⁹	(-1.85%)
`Mathlib.RingTheory.Localization.Ideal`	-1.49⬝10⁹	(-3.26%)
`Mathlib.LinearAlgebra.Finsupp.LSum`	-1.52⬝10⁹	(-3.40%)
`Mathlib.Algebra.MvPolynomial.Basic`	-1.54⬝10⁹	(-1.69%)
`Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi`	-1.55⬝10⁹	(-3.95%)
`Mathlib.Algebra.Homology.HomologySequence`	-1.55⬝10⁹	(-1.61%)
`Mathlib.Algebra.Module.LinearMap.End`	-1.57⬝10⁹	(-3.89%)
`Mathlib.RingTheory.Algebraic.MvPolynomial`	-1.64⬝10⁹	(-3.28%)
`Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone`	-1.65⬝10⁹	(-4.59%)
`Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls`	-1.66⬝10⁹	(-1.56%)
`Mathlib.RingTheory.Ideal.Maps`	-1.66⬝10⁹	(-1.36%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral`	-1.66⬝10⁹	(-2.60%)
`Mathlib.CategoryTheory.Subobject.MonoOver`	-1.70⬝10⁹	(-0.83%)
`Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat`	-1.80⬝10⁹	(-4.55%)
`Mathlib.CategoryTheory.Limits.Presheaf`	-1.82⬝10⁹	(-1.34%)
`Mathlib.GroupTheory.Sylow`	-1.87⬝10⁹	(-2.46%)
`Mathlib.RingTheory.WittVector.Truncated`	-1.91⬝10⁹	(-5.27%)
`Mathlib.CategoryTheory.FintypeCat`	-1.92⬝10⁹	(-8.13%)
`Mathlib.Combinatorics.SimpleGraph.Finsubgraph`	-1.95⬝10⁹	(-9.19%)
`Mathlib.RingTheory.NonUnitalSubring.Basic`	-1.95⬝10⁹	(-3.58%)
`Mathlib.CategoryTheory.Sites.CoverLifting`	-1.99⬝10⁹	(-2.24%)
`Mathlib.Topology.Homotopy.Path`	-1.99⬝10⁹	(-2.66%)
`Mathlib.AlgebraicGeometry.EllipticCurve.Group`	-1.104⬝10⁹	(-0.59%)
`Mathlib.CategoryTheory.Preadditive.Mat`	-1.109⬝10⁹	(-0.98%)
`Mathlib.LinearAlgebra.Dimension.Localization`	-1.110⬝10⁹	(-1.15%)
`Mathlib.CategoryTheory.Discrete.SumsProducts`	-1.111⬝10⁹	(-2.87%)
`Mathlib.CategoryTheory.Bicategory.Modification.Oplax`	-1.115⬝10⁹	(-4.66%)
`Mathlib.CategoryTheory.Bicategory.Kan.IsKan`	-1.118⬝10⁹	(-4.68%)
`Mathlib.Algebra.Lie.Matrix`	-1.125⬝10⁹	(-4.59%)
`Mathlib.LinearAlgebra.Quotient.Basic`	-1.125⬝10⁹	(-1.96%)
`Mathlib.RingTheory.IsTensorProduct`	-1.126⬝10⁹	(-0.83%)
`Mathlib.Geometry.RingedSpace.LocallyRingedSpace`	-1.133⬝10⁹	(-1.82%)
`Mathlib.CategoryTheory.Functor.Const`	-1.138⬝10⁹	(-5.10%)
`Mathlib.Computability.AkraBazzi.AkraBazzi`	-1.139⬝10⁹	(-0.68%)
`Mathlib.Algebra.Category.ModuleCat.Adjunctions`	-1.142⬝10⁹	(-1.83%)
`Mathlib.AlgebraicGeometry.Spec`	-1.144⬝10⁹	(-1.40%)
`Mathlib.RingTheory.PowerSeries.Inverse`	-1.145⬝10⁹	(-3.49%)
`Mathlib.Topology.VectorBundle.Hom`	-1.150⬝10⁹	(-1.26%)
`Mathlib.SetTheory.Cardinal.ENat`	-1.152⬝10⁹	(-7.18%)
`Mathlib.Algebra.Category.ModuleCat.Tannaka`	-1.161⬝10⁹	(-9.83%)
`Mathlib.Analysis.Analytic.OfScalars`	-1.163⬝10⁹	(-2.11%)
`Mathlib.CategoryTheory.Monoidal.Braided.Basic`	-1.165⬝10⁹	(-1.30%)
`Mathlib.Topology.Order.Category.AlexDisc`	-1.165⬝10⁹	(-3.91%)
`Mathlib.Algebra.Category.GrpWithZero`	-1.168⬝10⁹	(-11.03%)
`Mathlib.NumberTheory.MulChar.Basic`	-1.169⬝10⁹	(-3.90%)
`Mathlib.RingTheory.WittVector.Isocrystal`	-1.185⬝10⁹	(-1.68%)
`Mathlib.RingTheory.MatrixAlgebra`	-1.187⬝10⁹	(-2.01%)
`Mathlib.Analysis.Meromorphic.Order`	-1.194⬝10⁹	(-2.70%)
`Mathlib.CategoryTheory.Category.Preorder`	-1.203⬝10⁹	(-8.35%)
`Mathlib.FieldTheory.Relrank`	-1.206⬝10⁹	(-0.98%)
`Mathlib.Algebra.Category.ModuleCat.FilteredColimits`	-1.206⬝10⁹	(-1.89%)
`Mathlib.Order.Category.BddOrd`	-1.207⬝10⁹	(-5.38%)
`Mathlib.GroupTheory.SemidirectProduct`	-1.213⬝10⁹	(-2.71%)
`Mathlib.Order.Category.Lat`	-1.232⬝10⁹	(-6.41%)
`Mathlib.RingTheory.Polynomial.Quotient`	-1.239⬝10⁹	(-2.03%)
`Mathlib.Topology.Sheaves.Presheaf`	-1.241⬝10⁹	(-1.67%)
`Mathlib.Order.Category.DistLat`	-1.248⬝10⁹	(-7.66%)
`Mathlib.Topology.FiberBundle.Constructions`	-1.249⬝10⁹	(-8.62%)
`Mathlib.Topology.ContinuousMap.Star`	-1.254⬝10⁹	(-9.06%)
`Mathlib.FieldTheory.Normal.Defs`	-1.261⬝10⁹	(-3.94%)
`Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells`	-1.261⬝10⁹	(-3.22%)
`Mathlib.CategoryTheory.Galois.Prorepresentability`	-1.271⬝10⁹	(-3.67%)
`Mathlib.NumberTheory.LSeries.HurwitzZetaEven`	-1.271⬝10⁹	(-1.72%)
`Mathlib.NumberTheory.Dioph`	-1.272⬝10⁹	(-3.51%)
`Mathlib.Algebra.TrivSqZeroExt`	-1.275⬝10⁹	(-1.00%)
`Mathlib.NumberTheory.LegendreSymbol.ZModChar`	-1.281⬝10⁹	(-9.02%)
`Mathlib.AlgebraicTopology.DoldKan.FunctorN`	-1.282⬝10⁹	(-5.99%)
`Mathlib.LinearAlgebra.CliffordAlgebra.Equivs`	-1.282⬝10⁹	(-1.59%)
`Mathlib.Order.BooleanAlgebra`	-1.287⬝10⁹	(-3.54%)
`Mathlib.RingTheory.Localization.Free`	-1.289⬝10⁹	(-3.39%)
`Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward`	-1.299⬝10⁹	(-3.28%)
`Mathlib.Condensed.TopComparison`	-1.309⬝10⁹	(-7.97%)
`Mathlib.GroupTheory.OreLocalization.Basic`	-1.310⬝10⁹	(-2.52%)
`Mathlib.SetTheory.Ordinal.Basic`	-1.319⬝10⁹	(-3.01%)
`Mathlib.Algebra.BigOperators.Pi`	-1.323⬝10⁹	(-9.00%)
`Mathlib.RingTheory.RingHom.FinitePresentation`	-1.338⬝10⁹	(-2.39%)
`Mathlib.CategoryTheory.ComposableArrows`	-1.341⬝10⁹	(-0.65%)
`Mathlib.CategoryTheory.Enriched.Ordinary.Basic`	-1.341⬝10⁹	(-8.42%)
`Mathlib.RingTheory.Jacobson.Ring`	-1.347⬝10⁹	(-1.33%)
`Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs`	-1.347⬝10⁹	(-2.32%)
`Mathlib.RingTheory.Valuation.ValuationSubring`	-1.365⬝10⁹	(-1.11%)
`Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex`	-1.380⬝10⁹	(-2.44%)
`Mathlib.CategoryTheory.GradedObject`	-1.387⬝10⁹	(-2.17%)
`Mathlib.RingTheory.Valuation.AlgebraInstances`	-1.406⬝10⁹	(-3.06%)
`Mathlib.RingTheory.MvPolynomial.Localization`	-1.407⬝10⁹	(-4.09%)
`Mathlib.FieldTheory.RatFunc.Defs`	-1.410⬝10⁹	(-6.79%)
`Mathlib.Data.Finset.Max`	-1.415⬝10⁹	(-3.61%)
`Mathlib.Algebra.Order.Group.Cone`	-1.422⬝10⁹	(-18.82%)
`Mathlib.Topology.Category.Profinite.Basic`	-1.433⬝10⁹	(-7.47%)
`Mathlib.Algebra.Homology.Functor`	-1.438⬝10⁹	(-12.24%)
`Mathlib.NumberTheory.ModularForms.Basic`	-1.442⬝10⁹	(-5.43%)
`Mathlib.RingTheory.Smooth.Locus`	-1.447⬝10⁹	(-3.58%)
`Mathlib.Order.Filter.Interval`	-1.450⬝10⁹	(-5.29%)
`Mathlib.NumberTheory.NumberField.Basic`	-1.453⬝10⁹	(-2.80%)
`Mathlib.SetTheory.Cardinal.Subfield`	-1.454⬝10⁹	(-14.49%)
`Mathlib.Algebra.Lie.Basic`	-1.459⬝10⁹	(-1.45%)
`Mathlib.Topology.Sheaves.Alexandrov`	-1.475⬝10⁹	(-4.88%)
`Mathlib.Algebra.Lie.Subalgebra`	-1.487⬝10⁹	(-2.87%)
`Mathlib.CategoryTheory.Monoidal.Mod_`	-1.489⬝10⁹	(-9.89%)
`Mathlib.Geometry.RingedSpace.OpenImmersion`	-1.496⬝10⁹	(-0.63%)
`Mathlib.AlgebraicGeometry.Cover.Open`	-1.499⬝10⁹	(-2.56%)
`Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure`	-1.503⬝10⁹	(-3.03%)
`Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs`	-1.507⬝10⁹	(-4.39%)
`Mathlib.GroupTheory.Coprod.Basic`	-1.518⬝10⁹	(-2.68%)
`Mathlib.Analysis.Fourier.AddCircle`	-1.524⬝10⁹	(-2.02%)
`Mathlib.CategoryTheory.Triangulated.Basic`	-1.533⬝10⁹	(-4.64%)
`Mathlib.CategoryTheory.Sites.Coherent.SheafComparison`	-1.545⬝10⁹	(-6.81%)
`Mathlib.RingTheory.Perfection`	-1.555⬝10⁹	(-2.84%)
`Mathlib.Order.ConditionallyCompleteLattice.Defs`	-1.565⬝10⁹	(-22.23%)
`Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities`	-1.570⬝10⁹	(-3.59%)
`Mathlib.CategoryTheory.Monoidal.Free.Coherence`	-1.578⬝10⁹	(-4.12%)
`Mathlib.RingTheory.AdicCompletion.Algebra`	-1.579⬝10⁹	(-1.67%)
`Mathlib.Geometry.Manifold.Sheaf.Smooth`	-1.581⬝10⁹	(-1.66%)
`Mathlib.Topology.Category.TopCat.Basic`	-1.584⬝10⁹	(-13.48%)
`Mathlib.RingTheory.Trace.Quotient`	-1.588⬝10⁹	(-2.48%)
`Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal`	-1.606⬝10⁹	(-1.47%)
`Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv`	-1.609⬝10⁹	(-1.33%)
`Mathlib.Algebra.Lie.DirectSum`	-1.619⬝10⁹	(-6.19%)
`Mathlib.Analysis.Normed.Affine.ContinuousAffineMap`	-1.625⬝10⁹	(-3.21%)
`Mathlib.Topology.Algebra.Module.CharacterSpace`	-1.625⬝10⁹	(-6.09%)
`Mathlib.Algebra.Module.LocalizedModule.Submodule`	-1.627⬝10⁹	(-2.01%)
`Mathlib.CategoryTheory.Idempotents.Karoubi`	-1.631⬝10⁹	(-10.02%)
`Mathlib.Analysis.NormedSpace.MStructure`	-1.636⬝10⁹	(-5.48%)
`Mathlib.Geometry.RingedSpace.PresheafedSpace`	-1.645⬝10⁹	(-1.55%)
`Mathlib.Algebra.Category.HopfAlgebraCat.Basic`	-1.654⬝10⁹	(-5.13%)
`Mathlib.LinearAlgebra.ExteriorAlgebra.Basic`	-1.655⬝10⁹	(-2.41%)
`Mathlib.Topology.LocallyConstant.Algebra`	-1.655⬝10⁹	(-4.29%)
`Mathlib.Algebra.MonoidAlgebra.Defs`	-1.656⬝10⁹	(-1.99%)
`Mathlib.Algebra.Algebra.Unitization`	-1.659⬝10⁹	(-1.56%)
`Mathlib.CategoryTheory.Localization.Construction`	-1.665⬝10⁹	(-6.29%)
`Mathlib.CategoryTheory.Category.Bipointed`	-1.670⬝10⁹	(-10.19%)
`Mathlib.RingTheory.FiniteStability`	-1.671⬝10⁹	(-3.73%)
`Mathlib.AlgebraicGeometry.Pullbacks`	-1.672⬝10⁹	(-1.21%)
`Mathlib.GroupTheory.FreeGroup.Basic`	-1.676⬝10⁹	(-4.19%)
`Mathlib.FieldTheory.MvRatFunc.Rank`	-1.680⬝10⁹	(-8.90%)
`Mathlib.RingTheory.FinitePresentation`	-1.691⬝10⁹	(-3.56%)
`Mathlib.AlgebraicTopology.SimplicialObject.Split`	-1.703⬝10⁹	(-8.94%)
`Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus`	-1.726⬝10⁹	(-4.50%)
`Mathlib.NumberTheory.NumberField.AdeleRing`	-1.732⬝10⁹	(-6.61%)
`Mathlib.Algebra.Algebra.NonUnitalHom`	-1.738⬝10⁹	(-4.29%)
`Mathlib.Topology.Algebra.ContinuousMonoidHom`	-1.748⬝10⁹	(-6.49%)
`Mathlib.CategoryTheory.MorphismProperty.Comma`	-1.750⬝10⁹	(-4.64%)
`Mathlib.CategoryTheory.Monad.EquivMon`	-1.775⬝10⁹	(-4.50%)
`Mathlib.LinearAlgebra.Basis.Defs`	-1.778⬝10⁹	(-3.26%)
`Mathlib.Algebra.Homology.ShortComplex.Preadditive`	-1.793⬝10⁹	(-1.78%)
`Mathlib.RingTheory.Generators`	-1.797⬝10⁹	(-1.58%)
`Mathlib.GroupTheory.SpecificGroups.Dihedral`	-1.799⬝10⁹	(-8.95%)
`Mathlib.Analysis.Normed.Group.SemiNormedGrp`	-1.817⬝10⁹	(-7.51%)
`Mathlib.Topology.Algebra.Algebra`	-1.823⬝10⁹	(-4.39%)
`Mathlib.CategoryTheory.Bicategory.End`	-1.824⬝10⁹	(-20.18%)
`Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Strong`	-1.853⬝10⁹	(-3.84%)
`Mathlib.CategoryTheory.Limits.ExactFunctor`	-1.854⬝10⁹	(-3.49%)
`Mathlib.AlgebraicGeometry.Scheme`	-1.855⬝10⁹	(-1.60%)
`Mathlib.Order.Category.BddDistLat`	-1.862⬝10⁹	(-5.81%)
`Mathlib.Algebra.Category.BoolRing`	-1.862⬝10⁹	(-6.88%)
`Mathlib.LinearAlgebra.InvariantBasisNumber`	-1.877⬝10⁹	(-8.65%)
`Mathlib.Algebra.Category.Semigrp.Basic`	-1.878⬝10⁹	(-8.91%)
`Mathlib.RepresentationTheory.Basic`	-1.938⬝10⁹	(-3.26%)
`Mathlib.Algebra.Category.Grp.Basic`	-1.943⬝10⁹	(-4.48%)
`Mathlib.RepresentationTheory.Invariants`	-1.943⬝10⁹	(-4.78%)
`Mathlib.Algebra.Algebra.Equiv`	-1.952⬝10⁹	(-4.81%)
`Mathlib.Algebra.Lie.Quotient`	-1.954⬝10⁹	(-8.13%)
`Mathlib.Algebra.Star.Subalgebra`	-1.957⬝10⁹	(-2.30%)
`Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda`	-1.964⬝10⁹	(-3.90%)
`Mathlib.Topology.UniformSpace.UniformConvergenceTopology`	-1.966⬝10⁹	(-4.77%)
`Mathlib.Order.CompleteBooleanAlgebra`	-1.970⬝10⁹	(-4.60%)
`Mathlib.Topology.Homotopy.HomotopyGroup`	-1.971⬝10⁹	(-2.42%)
`Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots`	-1.973⬝10⁹	(-4.48%)
`Mathlib.MeasureTheory.Function.SimpleFuncDenseLp`	-1.982⬝10⁹	(-1.64%)
`Mathlib.LinearAlgebra.CliffordAlgebra.Basic`	-1.982⬝10⁹	(-2.69%)
`Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup`	-1.986⬝10⁹	(-3.85%)
`Mathlib.CategoryTheory.Bicategory.Extension`	-1.989⬝10⁹	(-7.13%)

83 files, Instructions -3.0⬝10⁹

File	Instructions	%
`Mathlib.RingTheory.Spectrum.Prime.FreeLocus`	-2.6⬝10⁹	(-2.87%)
`Mathlib.Order.Category.CompleteLat`	-2.12⬝10⁹	(-9.91%)
`Mathlib.Topology.UniformSpace.CompactConvergence`	-2.15⬝10⁹	(-9.54%)
`Mathlib.RingTheory.IsAdjoinRoot`	-2.16⬝10⁹	(-3.54%)
`Mathlib.RingTheory.MvPowerSeries.Basic`	-2.20⬝10⁹	(-2.97%)
`Mathlib.Algebra.Ring.ULift`	-2.30⬝10⁹	(-13.02%)
`Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic`	-2.39⬝10⁹	(-4.75%)
`Mathlib.LinearAlgebra.Multilinear.Basic`	-2.45⬝10⁹	(-2.09%)
`Mathlib.MeasureTheory.Function.LpSpace.Basic`	-2.45⬝10⁹	(-1.20%)
`Mathlib.Algebra.Category.ModuleCat.Colimits`	-2.47⬝10⁹	(-8.11%)
`Mathlib.Algebra.Algebra.Subalgebra.Basic`	-2.55⬝10⁹	(-4.10%)
`Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence`	-2.56⬝10⁹	(-2.71%)
`Mathlib.CategoryTheory.Subpresheaf.Basic`	-2.58⬝10⁹	(-9.87%)
`Mathlib.Algebra.Algebra.Quasispectrum`	-2.72⬝10⁹	(-2.50%)
`Mathlib.AlgebraicGeometry.Cover.Over`	-2.76⬝10⁹	(-4.03%)
`Mathlib.CategoryTheory.Quotient.Preadditive`	-2.102⬝10⁹	(-18.99%)
`Mathlib.CategoryTheory.GuitartExact.Basic`	-2.128⬝10⁹	(-2.55%)
`Mathlib.CategoryTheory.Endofunctor.Algebra`	-2.133⬝10⁹	(-3.26%)
`Mathlib.AlgebraicGeometry.AffineSpace`	-2.169⬝10⁹	(-0.85%)
`Mathlib.CategoryTheory.Monoidal.Bimon_`	-2.193⬝10⁹	(-2.61%)
`Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes`	-2.202⬝10⁹	(-8.77%)
`Mathlib.AlgebraicTopology.DoldKan.FunctorGamma`	-2.227⬝10⁹	(-7.82%)
`Mathlib.MeasureTheory.Function.L1Space.Integrable`	-2.236⬝10⁹	(-2.67%)
`Mathlib.Order.Category.BoolAlg`	-2.244⬝10⁹	(-4.71%)
`Mathlib.CategoryTheory.Category.ULift`	-2.254⬝10⁹	(-8.72%)
`Mathlib.Analysis.Normed.Lp.LpEquiv`	-2.269⬝10⁹	(-7.73%)
`Mathlib.NumberTheory.NumberField.Completion`	-2.278⬝10⁹	(-9.57%)
`Mathlib.RingTheory.Extension`	-2.323⬝10⁹	(-1.26%)
`Mathlib.AlgebraicGeometry.Gluing`	-2.326⬝10⁹	(-4.00%)
`Mathlib.Analysis.CStarAlgebra.Multiplier`	-2.327⬝10⁹	(-1.45%)
`Mathlib.LinearAlgebra.Finsupp.VectorSpace`	-2.334⬝10⁹	(-12.73%)
`Mathlib.Order.Nucleus`	-2.353⬝10⁹	(-15.52%)
`Mathlib.LinearAlgebra.FreeProduct.Basic`	-2.357⬝10⁹	(-4.52%)
`Mathlib.CategoryTheory.Idempotents.FunctorExtension`	-2.366⬝10⁹	(-2.72%)
`Mathlib.Algebra.Category.BialgebraCat.Basic`	-2.366⬝10⁹	(-5.15%)
`Mathlib.Algebra.Homology.ShortComplex.Basic`	-2.376⬝10⁹	(-7.50%)
`Mathlib.CategoryTheory.Functor.CurryingThree`	-2.378⬝10⁹	(-1.39%)
`Mathlib.SetTheory.Cardinal.Order`	-2.394⬝10⁹	(-10.20%)
`Mathlib.RingTheory.AdicCompletion.Basic`	-2.404⬝10⁹	(-2.34%)
`Mathlib.Combinatorics.Digraph.Basic`	-2.412⬝10⁹	(-23.75%)
`Mathlib.Algebra.DirectSum.Basic`	-2.475⬝10⁹	(-6.73%)
`Mathlib.RingTheory.TensorProduct.Basic`	-2.497⬝10⁹	(-0.57%)
`Mathlib.Algebra.Module.GradedModule`	-2.523⬝10⁹	(-5.25%)
`Mathlib.Data.Matrix.Basic`	-2.525⬝10⁹	(-7.29%)
`Mathlib.CategoryTheory.Opposites`	-2.532⬝10⁹	(-5.50%)
`Mathlib.Algebra.Homology.Augment`	-2.542⬝10⁹	(-4.28%)
`Mathlib.Analysis.RCLike.Basic`	-2.567⬝10⁹	(-2.04%)
`Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex`	-2.568⬝10⁹	(-4.76%)
`Mathlib.CategoryTheory.Monoidal.End`	-2.571⬝10⁹	(-4.57%)
`Mathlib.Order.Category.Semilat`	-2.572⬝10⁹	(-10.22%)
`Mathlib.Algebra.Lie.Abelian`	-2.586⬝10⁹	(-4.98%)
`Mathlib.RingTheory.DedekindDomain.Ideal`	-2.602⬝10⁹	(-1.38%)
`Mathlib.ModelTheory.DirectLimit`	-2.615⬝10⁹	(-7.91%)
`Mathlib.NumberTheory.Padics.RingHoms`	-2.622⬝10⁹	(-6.08%)
`Mathlib.CategoryTheory.FiberedCategory.Fiber`	-2.631⬝10⁹	(-19.13%)
`Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic`	-2.633⬝10⁹	(-6.66%)
`Mathlib.Algebra.Order.Interval.Basic`	-2.668⬝10⁹	(-6.68%)
`Mathlib.CategoryTheory.Preadditive.FunctorCategory`	-2.693⬝10⁹	(-18.97%)
`Mathlib.CategoryTheory.Sums.Basic`	-2.695⬝10⁹	(-7.58%)
`Mathlib.Data.Complex.Basic`	-2.704⬝10⁹	(-7.23%)
`Mathlib.CategoryTheory.Discrete.Basic`	-2.731⬝10⁹	(-7.85%)
`Mathlib.Analysis.SpecialFunctions.Stirling`	-2.735⬝10⁹	(-6.16%)
`Mathlib.Combinatorics.SimpleGraph.Basic`	-2.748⬝10⁹	(-11.11%)
`Mathlib.Order.Category.FinBddDistLat`	-2.765⬝10⁹	(-7.76%)
`Mathlib.CategoryTheory.Functor.KanExtension.Basic`	-2.788⬝10⁹	(-2.55%)
`Mathlib.SetTheory.Cardinal.Aleph`	-2.792⬝10⁹	(-8.93%)
`Mathlib.Algebra.Colimit.DirectLimit`	-2.797⬝10⁹	(-4.07%)
`Mathlib.Algebra.Lie.Free`	-2.797⬝10⁹	(-9.92%)
`Mathlib.CategoryTheory.Action.Limits`	-2.816⬝10⁹	(-5.45%)
`Mathlib.CategoryTheory.Localization.Resolution`	-2.820⬝10⁹	(-11.55%)
`Mathlib.RingTheory.WittVector.Basic`	-2.821⬝10⁹	(-5.94%)
`Mathlib.Topology.ContinuousMap.Algebra`	-2.833⬝10⁹	(-3.64%)
`Mathlib.Algebra.Module.LocalizedModule.Basic`	-2.836⬝10⁹	(-1.48%)
`Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits`	-2.899⬝10⁹	(-2.05%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic`	-2.904⬝10⁹	(-1.59%)
`Mathlib.CategoryTheory.Functor.FunctorHom`	-2.908⬝10⁹	(-7.05%)
`Mathlib.CategoryTheory.Products.Basic`	-2.925⬝10⁹	(-3.30%)
`Mathlib.CategoryTheory.Triangulated.Functor`	-2.925⬝10⁹	(-0.98%)
`Mathlib.Geometry.Manifold.Instances.Real`	-2.929⬝10⁹	(-6.49%)
`Mathlib.CategoryTheory.Triangulated.Rotate`	-2.947⬝10⁹	(-7.99%)
`Mathlib.CategoryTheory.Linear.FunctorCategory`	-2.960⬝10⁹	(-22.50%)
`Mathlib.Algebra.MonoidAlgebra.Basic`	-2.975⬝10⁹	(-5.98%)
`Mathlib.CategoryTheory.Comma.Arrow`	-2.985⬝10⁹	(-8.41%)

63 files, Instructions -4.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.Enriched.Basic`	-3.28⬝10⁹	(-10.35%)
`Mathlib.NumberTheory.Padics.Hensel`	-3.40⬝10⁹	(-3.65%)
`Mathlib.Algebra.RingQuot`	-3.77⬝10⁹	(-8.24%)
`Mathlib.Algebra.Homology.Opposite`	-3.95⬝10⁹	(-4.43%)
`Mathlib.CategoryTheory.Monad.Adjunction`	-3.96⬝10⁹	(-4.42%)
`Mathlib.Topology.Category.TopCat.Opens`	-3.105⬝10⁹	(-5.38%)
`Mathlib.Algebra.Star.Free`	-3.108⬝10⁹	(-27.82%)
`Mathlib.CategoryTheory.Skeletal`	-3.110⬝10⁹	(-7.31%)
`Mathlib.GroupTheory.SpecificGroups.Quaternion`	-3.125⬝10⁹	(-14.58%)
`Mathlib.Algebra.Homology.LocalCohomology`	-3.142⬝10⁹	(-12.51%)
`Mathlib.Topology.Category.LightProfinite.Basic`	-3.155⬝10⁹	(-8.95%)
`Mathlib.CategoryTheory.Monad.Algebra`	-3.156⬝10⁹	(-5.65%)
`Mathlib.LinearAlgebra.CliffordAlgebra.Contraction`	-3.166⬝10⁹	(-2.66%)
`Mathlib.CategoryTheory.Limits.Shapes.Types`	-3.173⬝10⁹	(-6.05%)
`Mathlib.AlgebraicGeometry.AffineScheme`	-3.186⬝10⁹	(-1.40%)
`Mathlib.CategoryTheory.Abelian.Images`	-3.209⬝10⁹	(-9.35%)
`Mathlib.Topology.ContinuousMap.ContinuousMapZero`	-3.229⬝10⁹	(-5.30%)
`Mathlib.Algebra.Homology.ShortComplex.SnakeLemma`	-3.232⬝10⁹	(-3.24%)
`Mathlib.Algebra.Homology.HomologicalComplexLimits`	-3.235⬝10⁹	(-8.17%)
`Mathlib.LinearAlgebra.Pi`	-3.242⬝10⁹	(-6.26%)
`Mathlib.FieldTheory.SeparableDegree`	-3.243⬝10⁹	(-2.05%)
`Mathlib.RingTheory.Presentation`	-3.245⬝10⁹	(-4.07%)
`Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory`	-3.260⬝10⁹	(-2.21%)
`Mathlib.Algebra.Category.Ring.Colimits`	-3.285⬝10⁹	(-10.64%)
`Mathlib.Algebra.Order.Group.PiLex`	-3.295⬝10⁹	(-35.21%)
`Mathlib.Algebra.Module.Injective`	-3.295⬝10⁹	(-6.59%)
`Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor`	-3.299⬝10⁹	(-3.13%)
`Mathlib.CategoryTheory.Grothendieck`	-3.303⬝10⁹	(-1.52%)
`Mathlib.MeasureTheory.Integral.BochnerL1`	-3.319⬝10⁹	(-3.49%)
`Mathlib.FieldTheory.PurelyInseparable.Exponent`	-3.362⬝10⁹	(-12.93%)
`Mathlib.RingTheory.Bialgebra.Hom`	-3.370⬝10⁹	(-7.45%)
`Mathlib.SetTheory.Ordinal.Family`	-3.404⬝10⁹	(-8.67%)
`Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat`	-3.411⬝10⁹	(-6.11%)
`Mathlib.Algebra.FreeAlgebra`	-3.429⬝10⁹	(-11.79%)
`Mathlib.RingTheory.Ideal.Quotient.Basic`	-3.469⬝10⁹	(-10.71%)
`Mathlib.FieldTheory.LinearDisjoint`	-3.487⬝10⁹	(-1.76%)
`Mathlib.AlgebraicTopology.CechNerve`	-3.498⬝10⁹	(-1.84%)
`Mathlib.FieldTheory.PerfectClosure`	-3.509⬝10⁹	(-9.01%)
`Mathlib.Algebra.Homology.Linear`	-3.510⬝10⁹	(-14.92%)
`Mathlib.LinearAlgebra.Prod`	-3.534⬝10⁹	(-4.66%)
`Mathlib.Algebra.Category.MonCat.Limits`	-3.562⬝10⁹	(-7.22%)
`Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts`	-3.564⬝10⁹	(-9.55%)
`Mathlib.Algebra.Homology.Additive`	-3.630⬝10⁹	(-5.12%)
`Mathlib.FieldTheory.IsPerfectClosure`	-3.660⬝10⁹	(-7.67%)
`Mathlib.CategoryTheory.Subobject.Types`	-3.692⬝10⁹	(-7.14%)
`Mathlib.Algebra.Category.Ring.Basic`	-3.699⬝10⁹	(-7.31%)
`Mathlib.Algebra.Homology.HomologicalBicomplex`	-3.706⬝10⁹	(-8.66%)
`Mathlib.CategoryTheory.MorphismProperty.Concrete`	-3.723⬝10⁹	(-28.17%)
`Mathlib.Geometry.Manifold.Algebra.SmoothFunctions`	-3.740⬝10⁹	(-6.91%)
`Mathlib.Algebra.Category.MonCat.Basic`	-3.746⬝10⁹	(-6.01%)
`Mathlib.LinearAlgebra.TensorAlgebra.Basic`	-3.763⬝10⁹	(-9.40%)
`Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives`	-3.791⬝10⁹	(-4.64%)
`Mathlib.Algebra.Module.Equiv.Basic`	-3.819⬝10⁹	(-9.02%)
`Mathlib.Combinatorics.Additive.VerySmallDoubling`	-3.822⬝10⁹	(-7.36%)
`Mathlib.Algebra.GCDMonoid.Basic`	-3.847⬝10⁹	(-5.70%)
`Mathlib.LinearAlgebra.LinearPMap`	-3.874⬝10⁹	(-4.01%)
`Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap`	-3.931⬝10⁹	(-3.61%)
`Mathlib.Algebra.Lie.Submodule`	-3.944⬝10⁹	(-2.84%)
`Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity`	-3.947⬝10⁹	(-1.60%)
`Mathlib.Algebra.Group.Submonoid.Membership`	-3.979⬝10⁹	(-15.85%)
`Mathlib.Algebra.Category.Ring.Under.Limits`	-3.987⬝10⁹	(-3.31%)
`Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup`	-3.988⬝10⁹	(-7.09%)
`Mathlib.GroupTheory.MonoidLocalization.Order`	-3.998⬝10⁹	(-22.61%)

38 files, Instructions -5.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.Comma.Presheaf.Basic`	-4.10⬝10⁹	(-2.64%)
`Mathlib.Algebra.Group.Hom.Instances`	-4.11⬝10⁹	(-19.78%)
`Mathlib.FieldTheory.Galois.Profinite`	-4.85⬝10⁹	(-2.80%)
`Mathlib.Data.Real.Basic`	-4.145⬝10⁹	(-11.28%)
`Mathlib.Topology.Algebra.Nonarchimedean.Bases`	-4.151⬝10⁹	(-21.17%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique`	-4.161⬝10⁹	(-2.38%)
`Mathlib.Condensed.Discrete.LocallyConstant`	-4.162⬝10⁹	(-5.24%)
`Mathlib.Algebra.Homology.ShortComplex.Linear`	-4.180⬝10⁹	(-7.53%)
`Mathlib.AlgebraicGeometry.Sites.Representability`	-4.184⬝10⁹	(-14.58%)
`Mathlib.Algebra.Module.Presentation.Differentials`	-4.192⬝10⁹	(-5.84%)
`Mathlib.CategoryTheory.Shift.SingleFunctors`	-4.304⬝10⁹	(-11.10%)
`Mathlib.Algebra.Algebra.NonUnitalSubalgebra`	-4.318⬝10⁹	(-4.80%)
`Mathlib.RingTheory.ClassGroup`	-4.336⬝10⁹	(-3.68%)
`Mathlib.CategoryTheory.Limits.Shapes.Reflexive`	-4.380⬝10⁹	(-6.00%)
`Mathlib.Data.Num.Lemmas`	-4.405⬝10⁹	(-4.95%)
`Mathlib.CategoryTheory.Monoidal.Grp_`	-4.412⬝10⁹	(-12.66%)
`Mathlib.Algebra.Category.AlgebraCat.Basic`	-4.449⬝10⁹	(-9.88%)
`Mathlib.AlgebraicGeometry.IdealSheaf`	-4.458⬝10⁹	(-1.45%)
`Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify`	-4.464⬝10⁹	(-4.73%)
`Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf`	-4.481⬝10⁹	(-5.06%)
`Mathlib.CategoryTheory.Limits.Cones`	-4.488⬝10⁹	(-1.46%)
`Mathlib.CategoryTheory.Monoidal.CommGrp_`	-4.490⬝10⁹	(-19.75%)
`Mathlib.Order.Category.BddLat`	-4.503⬝10⁹	(-10.81%)
`Mathlib.RingTheory.NoetherNormalization`	-4.529⬝10⁹	(-4.44%)
`Mathlib.Algebra.Category.Ring.Adjunctions`	-4.530⬝10⁹	(-2.82%)
`Mathlib.RingTheory.HahnSeries.Summable`	-4.586⬝10⁹	(-5.98%)
`Mathlib.CategoryTheory.Idempotents.FunctorCategories`	-4.651⬝10⁹	(-13.27%)
`Mathlib.RingTheory.AlgebraicIndependent.Adjoin`	-4.661⬝10⁹	(-8.81%)
`Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax`	-4.671⬝10⁹	(-5.65%)
`Mathlib.Algebra.Category.Grp.Limits`	-4.704⬝10⁹	(-7.10%)
`Mathlib.NumberTheory.Zsqrtd.Basic`	-4.738⬝10⁹	(-8.71%)
`Mathlib.CategoryTheory.Action.Basic`	-4.775⬝10⁹	(-9.27%)
`Mathlib.AlgebraicTopology.SimplicialNerve`	-4.791⬝10⁹	(-3.90%)
`Mathlib.Algebra.Order.Ring.Idempotent`	-4.907⬝10⁹	(-20.41%)
`Mathlib.Combinatorics.Enumerative.IncidenceAlgebra`	-4.921⬝10⁹	(-7.53%)
`Mathlib.CategoryTheory.GlueData`	-4.972⬝10⁹	(-6.21%)
`Mathlib.CategoryTheory.Monoidal.Opposite`	-4.990⬝10⁹	(-12.98%)
`Mathlib.RingTheory.Unramified.Field`	-4.999⬝10⁹	(-7.06%)

29 files, Instructions -6.0⬝10⁹

File	Instructions	%
`Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover`	-5.0⬝10⁹	(-5.93%)
`Mathlib.LinearAlgebra.PiTensorProduct`	-5.2⬝10⁹	(-3.32%)
`Mathlib.Algebra.Homology.HomotopyCategory.HomComplex`	-5.7⬝10⁹	(-5.52%)
`Mathlib.Algebra.Algebra.Subalgebra.Directed`	-5.80⬝10⁹	(-30.10%)
`Mathlib.CategoryTheory.FiberedCategory.BasedCategory`	-5.81⬝10⁹	(-12.54%)
`Mathlib.RingTheory.CotangentLocalizationAway`	-5.92⬝10⁹	(-5.44%)
`Mathlib.Order.Category.FinBoolAlg`	-5.92⬝10⁹	(-10.93%)
`Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization`	-5.140⬝10⁹	(-3.44%)
`Mathlib.Topology.Order.Category.FrameAdjunction`	-5.142⬝10⁹	(-18.18%)
`Mathlib.RingTheory.RingHom.Locally`	-5.165⬝10⁹	(-4.11%)
`Mathlib.CategoryTheory.Sums.Associator`	-5.210⬝10⁹	(-5.84%)
`Mathlib.RepresentationTheory.Rep`	-5.218⬝10⁹	(-3.82%)
`Mathlib.CategoryTheory.Category.Pairwise`	-5.349⬝10⁹	(-31.78%)
`Mathlib.RingTheory.Ideal.Norm.RelNorm`	-5.362⬝10⁹	(-3.67%)
`Mathlib.CategoryTheory.GradedObject.Monoidal`	-5.513⬝10⁹	(-5.87%)
`Mathlib.Order.Interval.Set.Basic`	-5.523⬝10⁹	(-5.44%)
`Mathlib.CategoryTheory.Monad.Products`	-5.524⬝10⁹	(-9.23%)
`Mathlib.CategoryTheory.Limits.Constructions.Filtered`	-5.528⬝10⁹	(-6.60%)
`Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks`	-5.530⬝10⁹	(-4.31%)
`Mathlib.CategoryTheory.Limits.Shapes.Grothendieck`	-5.552⬝10⁹	(-6.31%)
`Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_`	-5.569⬝10⁹	(-17.87%)
`Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts`	-5.571⬝10⁹	(-5.34%)
`Mathlib.RingTheory.Valuation.ValuationRing`	-5.598⬝10⁹	(-12.88%)
`Mathlib.CategoryTheory.Pi.Basic`	-5.653⬝10⁹	(-5.82%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order`	-5.716⬝10⁹	(-2.86%)
`Mathlib.CategoryTheory.Limits.Constructions.Over.Products`	-5.784⬝10⁹	(-7.39%)
`Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic`	-5.815⬝10⁹	(-6.08%)
`Mathlib.GroupTheory.MonoidLocalization.Basic`	-5.816⬝10⁹	(-6.65%)
`Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence`	-5.856⬝10⁹	(-5.77%)

16 files, Instructions -7.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.Bicategory.SingleObj`	-6.130⬝10⁹	(-31.69%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances`	-6.146⬝10⁹	(-2.56%)
`Mathlib.Algebra.Category.BialgebraCat.Monoidal`	-6.190⬝10⁹	(-4.62%)
`Mathlib.CategoryTheory.Comma.Over.Pullback`	-6.194⬝10⁹	(-6.90%)
`Mathlib.Analysis.Normed.Field.Basic`	-6.208⬝10⁹	(-12.00%)
`Mathlib.Algebra.Star.NonUnitalSubalgebra`	-6.272⬝10⁹	(-3.67%)
`Mathlib.CategoryTheory.Monoidal.Center`	-6.306⬝10⁹	(-9.63%)
`Mathlib.CategoryTheory.Linear.Yoneda`	-6.443⬝10⁹	(-9.40%)
`Mathlib.Analysis.Normed.Algebra.QuaternionExponential`	-6.493⬝10⁹	(-19.73%)
`Mathlib.CategoryTheory.Preadditive.EndoFunctor`	-6.535⬝10⁹	(-30.27%)
`Mathlib.CategoryTheory.Functor.Category`	-6.568⬝10⁹	(-21.59%)
`Mathlib.CategoryTheory.Preadditive.EilenbergMoore`	-6.653⬝10⁹	(-29.99%)
`Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts`	-6.765⬝10⁹	(-5.00%)
`Mathlib.CategoryTheory.Subpresheaf.Subobject`	-6.839⬝10⁹	(-13.96%)
`Mathlib.CategoryTheory.Category.Cat`	-6.945⬝10⁹	(-27.17%)
`Mathlib.RingTheory.DedekindDomain.Different`	-6.951⬝10⁹	(-2.60%)

15 files, Instructions -8.0⬝10⁹

File	Instructions	%
`Mathlib.Topology.Sheaves.CommRingCat`	-7.5⬝10⁹	(-10.66%)
`Mathlib.CategoryTheory.Triangulated.TriangleShift`	-7.55⬝10⁹	(-4.87%)
`Mathlib.CategoryTheory.Subobject.Lattice`	-7.104⬝10⁹	(-5.15%)
`Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing`	-7.130⬝10⁹	(-8.52%)
`Mathlib.CategoryTheory.Functor.KanExtension.Pointwise`	-7.235⬝10⁹	(-10.02%)
`Mathlib.CategoryTheory.Limits.Shapes.Products`	-7.361⬝10⁹	(-6.30%)
`Mathlib.CategoryTheory.Category.Cat.Limit`	-7.363⬝10⁹	(-13.96%)
`Mathlib.LinearAlgebra.RootSystem.Hom`	-7.457⬝10⁹	(-6.53%)
`Mathlib.Algebra.Category.ModuleCat.Basic`	-7.676⬝10⁹	(-9.27%)
`Mathlib.Algebra.Homology.Bifunctor`	-7.770⬝10⁹	(-7.05%)
`Mathlib.LinearAlgebra.Matrix.ToLin`	-7.835⬝10⁹	(-5.51%)
`Mathlib.CategoryTheory.Monoidal.Internal.Module`	-7.901⬝10⁹	(-5.41%)
`Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings`	-7.966⬝10⁹	(-27.67%)
`Mathlib.CategoryTheory.Preadditive.Yoneda.Basic`	-7.974⬝10⁹	(-11.10%)
`Mathlib.RingTheory.Spectrum.Prime.Polynomial`	-7.977⬝10⁹	(-5.46%)

6 files, Instructions -9.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.Yoneda`	-8.172⬝10⁹	(-7.33%)
`Mathlib.Algebra.Field.Subfield.Basic`	-8.447⬝10⁹	(-24.26%)
`Mathlib.Analysis.CStarAlgebra.ApproximateUnit`	-8.467⬝10⁹	(-5.32%)
`Mathlib.CategoryTheory.Quotient.Linear`	-8.608⬝10⁹	(-44.95%)
`Mathlib.CategoryTheory.Limits.Shapes.Biproducts`	-8.662⬝10⁹	(-5.94%)
`Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings`	-8.924⬝10⁹	(-11.88%)

5 files, Instructions -10.0⬝10⁹

File	Instructions	%
`Mathlib.Algebra.Category.AlgebraCat.Limits`	-9.575⬝10⁹	(-15.89%)
`Mathlib.CategoryTheory.Square`	-9.646⬝10⁹	(-12.92%)
`Mathlib.NumberTheory.NumberField.FinitePlaces`	-9.655⬝10⁹	(-9.26%)
`Mathlib.RingTheory.DedekindDomain.AdicValuation`	-9.667⬝10⁹	(-9.80%)
`Mathlib.CategoryTheory.GradedObject.Bifunctor`	-9.813⬝10⁹	(-13.74%)

4 files, Instructions -11.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.DifferentialObject`	-10.273⬝10⁹	(-18.58%)
`Mathlib.CategoryTheory.Preadditive.CommGrp_`	-10.476⬝10⁹	(-24.85%)
`Mathlib.CategoryTheory.Groupoid.Subgroupoid`	-10.555⬝10⁹	(-30.89%)
`Mathlib.CategoryTheory.Monoidal.Comon_`	-10.791⬝10⁹	(-15.89%)

5 files, Instructions -12.0⬝10⁹

File	Instructions	%
`Mathlib.RingTheory.IntegralClosure.IntegralRestrict`	-11.8⬝10⁹	(-3.77%)
`Mathlib.Topology.Algebra.UniformRing`	-11.151⬝10⁹	(-33.38%)
`Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts`	-11.176⬝10⁹	(-9.57%)
`Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer`	-11.453⬝10⁹	(-13.21%)
`Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor`	-11.899⬝10⁹	(-22.78%)

6 files, Instructions -13.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.Monoidal.CommMon_`	-12.36⬝10⁹	(-11.58%)
`Mathlib.Algebra.Category.ModuleCat.Algebra`	-12.93⬝10⁹	(-49.35%)
`Mathlib.SetTheory.Surreal.Multiplication`	-12.344⬝10⁹	(-38.72%)
`Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification`	-12.373⬝10⁹	(-17.60%)
`Mathlib.CategoryTheory.Comma.StructuredArrow.Functor`	-12.481⬝10⁹	(-22.07%)
`Mathlib.Algebra.Category.ModuleCat.Presheaf`	-12.908⬝10⁹	(-5.86%)

3 files, Instructions -14.0⬝10⁹

File	Instructions	%
`Mathlib.RingTheory.LocalRing.ResidueField.Ideal`	-13.245⬝10⁹	(-11.94%)
`Mathlib.CategoryTheory.Limits.Final`	-13.403⬝10⁹	(-6.33%)
`Mathlib.Analysis.Quaternion`	-13.913⬝10⁹	(-28.41%)

3 files, Instructions -15.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.Normed.Affine.Isometry`	-14.96⬝10⁹	(-13.18%)
`Mathlib.CategoryTheory.Functor.Currying`	-14.460⬝10⁹	(-13.45%)
`Mathlib.CategoryTheory.Monoidal.Discrete`	-14.750⬝10⁹	(-35.68%)

6 files, Instructions -16.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.Adjunction.Evaluation`	-15.151⬝10⁹	(-18.77%)
`Mathlib.CategoryTheory.Sites.Sheaf`	-15.277⬝10⁹	(-18.18%)
`Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject`	-15.328⬝10⁹	(-40.41%)
`Mathlib.CategoryTheory.Comma.Over.Basic`	-15.465⬝10⁹	(-4.97%)
`Mathlib.RepresentationTheory.GroupCohomology.Basic`	-15.781⬝10⁹	(-15.66%)
`Mathlib.FieldTheory.RatFunc.Basic`	-15.838⬝10⁹	(-6.47%)

3 files, Instructions -17.0⬝10⁹

File	Instructions	%
`Mathlib.RingTheory.Kaehler.Polynomial`	-16.64⬝10⁹	(-7.60%)
`Mathlib.CategoryTheory.Elements`	-16.407⬝10⁹	(-23.07%)
`Mathlib.CategoryTheory.Comma.Basic`	-16.823⬝10⁹	(-8.40%)

2 files, Instructions -18.0⬝10⁹

File	Instructions	%
`Mathlib.Algebra.Quaternion`	-17.207⬝10⁹	(-7.76%)
`Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme`	-17.707⬝10⁹	(-8.26%)

File	Instructions	%
`Mathlib.CategoryTheory.Limits.ConeCategory`	-18.487⬝10⁹	(-21.44%)

2 files, Instructions -20.0⬝10⁹

File	Instructions	%
`Mathlib.RingTheory.LaurentSeries`	-19.495⬝10⁹	(-7.67%)
`Mathlib.CategoryTheory.Monoidal.Category`	-19.861⬝10⁹	(-17.28%)

File	Instructions	%
`Mathlib.CategoryTheory.Monoidal.Mon_`	-21.470⬝10⁹	(-14.85%)

3 files, Instructions -23.0⬝10⁹

File	Instructions	%
`Mathlib.Data.ZMod.Defs`	-22.85⬝10⁹	(-76.07%)
`Mathlib.AlgebraicGeometry.StructureSheaf`	-22.275⬝10⁹	(-13.37%)
`Mathlib.Algebra.Homology.AlternatingConst`	-22.375⬝10⁹	(-37.07%)

2 files, Instructions -24.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.Functor.Trifunctor`	-23.3⬝10⁹	(-13.83%)
`Mathlib.CategoryTheory.Triangulated.Opposite.Triangle`	-23.145⬝10⁹	(-17.05%)

File	Instructions	%
`Mathlib.Topology.MetricSpace.GromovHausdorff`	-25.428⬝10⁹	(-26.50%)
`Mathlib.Algebra.Category.ModuleCat.ChangeOfRings`	-26.628⬝10⁹	(-8.73%)

4 files, Instructions -28.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.Comma.StructuredArrow.Basic`	-27.421⬝10⁹	(-8.29%)
`Mathlib.CategoryTheory.GradedObject.Trifunctor`	-27.621⬝10⁹	(-11.00%)
`Mathlib.Algebra.Field.Basic`	-27.680⬝10⁹	(-56.04%)
`Mathlib.CategoryTheory.Whiskering`	-27.849⬝10⁹	(-10.89%)

File	Instructions	%
`Mathlib.LinearAlgebra.RootSystem.BaseChange`	-29.378⬝10⁹	(-42.55%)
`Mathlib.AlgebraicTopology.SimplicialObject.Basic`	-30.813⬝10⁹	(-13.71%)

3 files, Instructions -39.0⬝10⁹

File	Instructions	%
`Mathlib.Algebra.Category.Ring.Limits`	-38.0⬝10⁹	(-27.76%)
`Mathlib.Algebra.Order.Field.Defs`	-38.600⬝10⁹	(-74.49%)
`Mathlib.CategoryTheory.Bicategory.Coherence`	-38.895⬝10⁹	(-30.75%)

File	Instructions	%
`Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete`	-50.871⬝10⁹	(-53.27%)
`Mathlib.RingTheory.Kaehler.JacobiZariski`	-55.522⬝10⁹	(-7.76%)
`Mathlib.CategoryTheory.Bicategory.Free`	-65.444⬝10⁹	(-56.21%)
CI run

leanprover-community-mathlib4-bot and others added 14 commits March 29, 2025 09:11

Update lean-toolchain for testing leanprover/lean4#7717

dfa8eea

Trigger CI for leanprover/lean4#7717

1b41f85

Trigger CI for leanprover/lean4#7717

c62c2e1

fixes

41c9a6c

fixes

3bbcdbd

Trigger CI for leanprover/lean4#7717

0c9882a

fixes

4b43ef5

fixes

3470841

fixes

9bc016f

fixes

28f5b3d

got through all of mathlib

3495ca3

missing space

ef61e41

fix tests

75dcd77

Trigger CI for leanprover/lean4#7717

2eb925d

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 30, 2025

leanprover-community-mathlib4-bot added 2 commits March 30, 2025 07:28

Trigger CI for leanprover/lean4#7717

9d97d61

Trigger CI for leanprover/lean4#7717

a00f0c4

This was referenced Mar 30, 2025

Porting notes: additional beta_reduction necessary #12129

Open

feat: structure instance notation elaboration improvements leanprover/lean4#7717

Merged

kim-em merged commit 90c315e into nightly-testing Mar 31, 2025
6 checks passed

Vierkantor mentioned this pull request Apr 1, 2025

[Merged by Bors] - chore(LinearAlgebra/LinearPMap): process porting notes #23538

Closed

YaelDillies deleted the lean-pr-testing-7717 branch August 15, 2025 17:07

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Lean pr testing 7717#23445

Lean pr testing 7717#23445
kim-em merged 16 commits intonightly-testingfrom
lean-pr-testing-7717

kmill commented Mar 30, 2025

Uh oh!

kmill commented Mar 30, 2025

Uh oh!

leanprover-bot commented Mar 30, 2025

Uh oh!

github-actions bot commented Mar 30, 2025

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

kmill commented Mar 30, 2025

Uh oh!

kmill commented Mar 30, 2025

Uh oh!

leanprover-bot commented Mar 30, 2025

Uh oh!

github-actions bot commented Mar 30, 2025

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants