perf: TRY disabling ALL syntax style linters, see what the effect is #19551

grunweg · 2024-11-27T21:43:32Z

Opening for comparison with #19547: this PR disables all syntax style linters (the five linters rewritten in that PR, and two more). Let's see if these linters have any significant effect whatsoever.

Once CI is complete, help benchmarking this is welcome.

github-actions · 2024-11-27T21:44:21Z

PR summary 3a4fded931

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

grunweg · 2024-11-27T22:30:26Z

!bench

grunweg · 2024-11-27T22:30:40Z

(I presume failing tests don't prevent benchmarking.)

leanprover-bot · 2024-11-27T23:25:47Z

Here are the benchmark results for commit 3a4fded.
There were significant changes against commit b5fb043:

  Benchmark   Metric           Change
  ===================================
+ build       interpretation   -11.0%

adomani · 2024-11-28T07:39:32Z

Locally, the bot says

File	Instructions	%
`build`	-2926.129⬝10⁹	(-2.06%)

589 files, Instructions -2.0⬝10⁹

File	Instructions	%
`Mathlib.AlgebraicTopology.SimplicialSet.Basic`	-1.1⬝10⁹	(-1.78%)
`Mathlib.Topology.ContinuousMap.CompactlySupported`	-1.2⬝10⁹	(-2.44%)
`Mathlib.ModelTheory.Order`	-1.2⬝10⁹	(-4.32%)
`Mathlib.LinearAlgebra.Matrix.PosDef`	-1.3⬝10⁹	(-1.48%)
`Mathlib.Topology.Order.LowerUpperTopology`	-1.3⬝10⁹	(-7.86%)
`Mathlib.LinearAlgebra.FreeModule.PID`	-1.4⬝10⁹	(-1.50%)
`Mathlib.Analysis.NormedSpace.Multilinear.Curry`	-1.4⬝10⁹	(-0.48%)
`Mathlib.Analysis.Complex.UpperHalfPlane.Basic`	-1.4⬝10⁹	(-1.40%)
`Mathlib.Analysis.Calculus.FDeriv.Equiv`	-1.6⬝10⁹	(-1.24%)
`Mathlib.Combinatorics.Enumerative.DyckWord`	-1.7⬝10⁹	(-4.18%)
`Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated`	-1.9⬝10⁹	(-0.40%)
`Mathlib.Data.Matrix.Notation`	-1.12⬝10⁹	(-2.94%)
`Mathlib.CategoryTheory.Sites.Grothendieck`	-1.12⬝10⁹	(-4.77%)
`Mathlib.Algebra.Group.Subgroup.Map`	-1.12⬝10⁹	(-3.99%)
`Mathlib.Algebra.CharP.Lemmas`	-1.13⬝10⁹	(-3.89%)
`Mathlib.Topology.MetricSpace.GromovHausdorffRealized`	-1.13⬝10⁹	(-3.29%)
`Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1`	-1.13⬝10⁹	(-1.23%)
`Mathlib.LinearAlgebra.BilinearMap`	-1.13⬝10⁹	(-1.93%)
`Mathlib.Analysis.InnerProductSpace.TwoDim`	-1.15⬝10⁹	(-0.71%)
`Mathlib.Tactic.Abel`	-1.15⬝10⁹	(-3.46%)
`Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol`	-1.16⬝10⁹	(-3.53%)
`Mathlib.CategoryTheory.Limits.Creates`	-1.17⬝10⁹	(-4.41%)
`Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated`	-1.17⬝10⁹	(-7.84%)
`Mathlib.Order.Ideal`	-1.18⬝10⁹	(-7.42%)
`Mathlib.CategoryTheory.GradedObject`	-1.18⬝10⁹	(-1.81%)
`Mathlib.Algebra.Group.Pi.Basic`	-1.18⬝10⁹	(-8.07%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order`	-1.19⬝10⁹	(-0.42%)
`Mathlib.CategoryTheory.WithTerminal`	-1.19⬝10⁹	(-0.93%)
`Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties`	-1.20⬝10⁹	(-1.42%)
`Mathlib.Algebra.Algebra.Spectrum`	-1.20⬝10⁹	(-2.50%)
`Mathlib.LinearAlgebra.BilinearForm.Properties`	-1.21⬝10⁹	(-1.34%)
`Mathlib.AlgebraicGeometry.RationalMap`	-1.21⬝10⁹	(-1.46%)
`Mathlib.Analysis.Normed.Operator.Banach`	-1.21⬝10⁹	(-1.03%)
`Mathlib.Analysis.LocallyConvex.Bounded`	-1.22⬝10⁹	(-2.45%)
`Mathlib.LinearAlgebra.Finsupp.LinearCombination`	-1.23⬝10⁹	(-3.53%)
`Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable`	-1.24⬝10⁹	(-1.04%)
`Mathlib.FieldTheory.IsPerfectClosure`	-1.25⬝10⁹	(-2.16%)
`Mathlib.Algebra.Quandle`	-1.27⬝10⁹	(-5.52%)
`Mathlib.Analysis.Analytic.Inverse`	-1.29⬝10⁹	(-0.81%)
`Mathlib.Analysis.Calculus.FDeriv.Prod`	-1.29⬝10⁹	(-1.04%)
`Mathlib.Analysis.SpecialFunctions.Exp`	-1.31⬝10⁹	(-3.73%)
`Mathlib.RingTheory.Coprime.Basic`	-1.31⬝10⁹	(-4.56%)
`Mathlib.Topology.EMetricSpace.Lipschitz`	-1.32⬝10⁹	(-4.91%)
`Mathlib.Combinatorics.Configuration`	-1.32⬝10⁹	(-4.07%)
`Mathlib.MeasureTheory.Constructions.BorelSpace.Real`	-1.33⬝10⁹	(-4.98%)
`Mathlib.MeasureTheory.Integral.Prod`	-1.34⬝10⁹	(-2.74%)
`Mathlib.GroupTheory.FreeAbelianGroup`	-1.34⬝10⁹	(-2.59%)
`Mathlib.LinearAlgebra.AffineSpace.AffineEquiv`	-1.34⬝10⁹	(-1.65%)
`Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous`	-1.35⬝10⁹	(-3.11%)
`Mathlib.Tactic.Positivity.Basic`	-1.36⬝10⁹	(-1.81%)
`Mathlib.GroupTheory.GroupAction.Blocks`	-1.36⬝10⁹	(-2.41%)
`Mathlib.ModelTheory.LanguageMap`	-1.37⬝10⁹	(-7.94%)
`Mathlib.Geometry.Manifold.Diffeomorph`	-1.38⬝10⁹	(-2.37%)
`Mathlib.Algebra.Tropical.Basic`	-1.38⬝10⁹	(-6.91%)
`Mathlib.Data.NNRat.Defs`	-1.38⬝10⁹	(-6.98%)
`Mathlib.Analysis.SpecialFunctions.Gamma.Beta`	-1.39⬝10⁹	(-2.26%)
`Mathlib.Data.List.Permutation`	-1.39⬝10⁹	(-7.23%)
`Mathlib.CategoryTheory.ChosenFiniteProducts`	-1.40⬝10⁹	(-2.90%)
`Mathlib.Order.Closure`	-1.43⬝10⁹	(-8.17%)
`Mathlib.CategoryTheory.Monoidal.Opposite`	-1.44⬝10⁹	(-3.09%)
`Mathlib.Analysis.SpecialFunctions.Pow.Continuity`	-1.44⬝10⁹	(-1.90%)
`Mathlib.NumberTheory.Padics.RingHoms`	-1.45⬝10⁹	(-2.20%)
`Mathlib.Algebra.AddConstMap.Basic`	-1.46⬝10⁹	(-2.65%)
`Mathlib.LinearAlgebra.Dimension.Finite`	-1.46⬝10⁹	(-1.79%)
`Mathlib.Data.Num.Basic`	-1.47⬝10⁹	(-17.23%)
`Mathlib.CategoryTheory.Sites.ConcreteSheafification`	-1.47⬝10⁹	(-2.40%)
`Mathlib.RingTheory.Artinian`	-1.49⬝10⁹	(-1.65%)
`Mathlib.LinearAlgebra.Basis.Basic`	-1.50⬝10⁹	(-1.87%)
`Mathlib.Algebra.Group.Subgroup.Ker`	-1.51⬝10⁹	(-4.09%)
`Mathlib.ModelTheory.DirectLimit`	-1.52⬝10⁹	(-3.26%)
`Mathlib.SetTheory.Surreal.Multiplication`	-1.54⬝10⁹	(-3.33%)
`Mathlib.NumberTheory.MulChar.Basic`	-1.55⬝10⁹	(-3.65%)
`Mathlib.Algebra.Homology.HomotopyCofiber`	-1.55⬝10⁹	(-2.14%)
`Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback`	-1.57⬝10⁹	(-3.14%)
`Mathlib.CategoryTheory.Opposites`	-1.57⬝10⁹	(-2.45%)
`Mathlib.Order.Filter.Ultrafilter`	-1.58⬝10⁹	(-7.78%)
`Mathlib.Topology.MetricSpace.Infsep`	-1.58⬝10⁹	(-5.76%)
`Mathlib.Analysis.FunctionalSpaces.SobolevInequality`	-1.60⬝10⁹	(-0.81%)
`Mathlib.CategoryTheory.Monad.Limits`	-1.62⬝10⁹	(-2.73%)
`Mathlib.Probability.Kernel.RadonNikodym`	-1.64⬝10⁹	(-3.89%)
`Mathlib.Geometry.Manifold.Algebra.Monoid`	-1.64⬝10⁹	(-3.12%)
`Mathlib.Algebra.BigOperators.Expect`	-1.64⬝10⁹	(-3.01%)
`Mathlib.Algebra.Algebra.Basic`	-1.68⬝10⁹	(-3.85%)
`Mathlib.Algebra.Module.Equiv.Defs`	-1.70⬝10⁹	(-3.01%)
`Mathlib.Algebra.Algebra.Hom`	-1.72⬝10⁹	(-4.75%)
`Mathlib.GroupTheory.Coset.Basic`	-1.73⬝10⁹	(-2.50%)
`Mathlib.RingTheory.PrincipalIdealDomain`	-1.75⬝10⁹	(-4.51%)
`Mathlib.Analysis.InnerProductSpace.Adjoint`	-1.76⬝10⁹	(-0.50%)
`Mathlib.LinearAlgebra.TensorProduct.Tower`	-1.76⬝10⁹	(-0.96%)
`Mathlib.CategoryTheory.Subobject.Basic`	-1.80⬝10⁹	(-2.13%)
`Mathlib.Topology.Algebra.InfiniteSum.NatInt`	-1.80⬝10⁹	(-4.71%)
`Mathlib.Order.Heyting.Hom`	-1.81⬝10⁹	(-6.18%)
`Mathlib.Analysis.Calculus.LineDeriv.Basic`	-1.81⬝10⁹	(-1.94%)
`Mathlib.Topology.Algebra.OpenSubgroup`	-1.83⬝10⁹	(-4.00%)
`Mathlib.CategoryTheory.Sites.IsSheafFor`	-1.85⬝10⁹	(-5.39%)
`Mathlib`	-1.86⬝10⁹	(-9.29%)
`Mathlib.FieldTheory.KummerExtension`	-1.86⬝10⁹	(-0.93%)
`Mathlib.MeasureTheory.Measure.LevyProkhorovMetric`	-1.89⬝10⁹	(-2.04%)
`Mathlib.Topology.Algebra.ConstMulAction`	-1.90⬝10⁹	(-3.36%)
`Mathlib.AlgebraicGeometry.EllipticCurve.Group`	-1.90⬝10⁹	(-0.59%)
`Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift`	-1.90⬝10⁹	(-1.16%)
`Mathlib.Data.List.MinMax`	-1.90⬝10⁹	(-5.82%)
`Mathlib.Dynamics.TopologicalEntropy.CoverEntropy`	-1.91⬝10⁹	(-3.88%)
`Mathlib.NumberTheory.PythagoreanTriples`	-1.91⬝10⁹	(-2.05%)
`Mathlib.Analysis.Calculus.Deriv.Mul`	-1.92⬝10⁹	(-0.92%)
`Mathlib.Order.SuccPred.Archimedean`	-1.92⬝10⁹	(-6.72%)
`Mathlib.CategoryTheory.GradedObject.Trifunctor`	-1.92⬝10⁹	(-0.47%)
`Mathlib.MeasureTheory.Decomposition.RadonNikodym`	-1.94⬝10⁹	(-4.83%)
`Mathlib.LinearAlgebra.Determinant`	-1.94⬝10⁹	(-1.39%)
`Mathlib.Algebra.Group.Units.Basic`	-1.98⬝10⁹	(-6.38%)
`Mathlib.Data.QPF.Univariate.Basic`	-1.100⬝10⁹	(-9.25%)
`Mathlib.Data.DFinsupp.BigOperators`	-1.100⬝10⁹	(-3.10%)
`Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable`	-1.102⬝10⁹	(-2.14%)
`Mathlib.Algebra.Algebra.Quasispectrum`	-1.103⬝10⁹	(-1.57%)
`Mathlib.Data.List.Sort`	-1.104⬝10⁹	(-7.79%)
`Mathlib.Topology.Sheaves.Stalks`	-1.105⬝10⁹	(-1.07%)
`Mathlib.Data.List.Chain`	-1.105⬝10⁹	(-5.36%)
`Mathlib.Topology.Order.Compact`	-1.106⬝10⁹	(-3.74%)
`Mathlib.Data.Sign`	-1.106⬝10⁹	(-3.18%)
`Mathlib.CategoryTheory.Monoidal.Rigid.Basic`	-1.108⬝10⁹	(-2.27%)
`Mathlib.Topology.MetricSpace.Bounded`	-1.109⬝10⁹	(-4.81%)
`Mathlib.Algebra.Group.Subgroup.Lattice`	-1.109⬝10⁹	(-4.43%)
`Mathlib.RepresentationTheory.Rep`	-1.110⬝10⁹	(-0.98%)
`Mathlib.Geometry.Euclidean.MongePoint`	-1.114⬝10⁹	(-1.26%)
`Mathlib.Order.Sublattice`	-1.114⬝10⁹	(-5.23%)
`Mathlib.RingTheory.PrimeSpectrum`	-1.117⬝10⁹	(-4.24%)
`Mathlib.GroupTheory.GroupAction.Defs`	-1.118⬝10⁹	(-5.35%)
`Mathlib.Algebra.Group.Opposite`	-1.119⬝10⁹	(-5.49%)
`Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers`	-1.119⬝10⁹	(-3.10%)
`Mathlib.Tactic.Simps.Basic`	-1.120⬝10⁹	(-3.46%)
`Mathlib.LinearAlgebra.Dimension.Constructions`	-1.121⬝10⁹	(-1.41%)
`Mathlib.RingTheory.Derivation.Basic`	-1.122⬝10⁹	(-1.30%)
`Mathlib.Data.Real.Sqrt`	-1.122⬝10⁹	(-4.10%)
`Mathlib.NumberTheory.LSeries.HurwitzZetaOdd`	-1.124⬝10⁹	(-2.23%)
`Mathlib.Topology.Algebra.UniformGroup.Defs`	-1.125⬝10⁹	(-2.64%)
`Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots`	-1.126⬝10⁹	(-1.72%)
`Mathlib.Algebra.CubicDiscriminant`	-1.127⬝10⁹	(-3.64%)
`Mathlib.CategoryTheory.Iso`	-1.129⬝10⁹	(-8.21%)
`Mathlib.FieldTheory.Finite.Basic`	-1.129⬝10⁹	(-3.61%)
`Mathlib.Algebra.DirectSum.Ring`	-1.131⬝10⁹	(-1.99%)
`Mathlib.NumberTheory.Cyclotomic.Rat`	-1.131⬝10⁹	(-0.91%)
`Mathlib.Algebra.Polynomial.Splits`	-1.131⬝10⁹	(-2.61%)
`Mathlib.CategoryTheory.Adjunction.Basic`	-1.132⬝10⁹	(-2.14%)
`Mathlib.Algebra.Ring.Parity`	-1.132⬝10⁹	(-7.29%)
`Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone`	-1.133⬝10⁹	(-1.09%)
`Mathlib.Topology.PartitionOfUnity`	-1.135⬝10⁹	(-4.98%)
`Mathlib.CategoryTheory.Comma.Presheaf.Basic`	-1.136⬝10⁹	(-0.81%)
`Mathlib.Combinatorics.SimpleGraph.Maps`	-1.139⬝10⁹	(-7.67%)
`Mathlib.CategoryTheory.Equivalence`	-1.139⬝10⁹	(-2.12%)
`Mathlib.Tactic.ToAdditive.Frontend`	-1.140⬝10⁹	(-3.33%)
`Mathlib.Algebra.Lie.Weights.Killing`	-1.142⬝10⁹	(-0.54%)
`Mathlib.Order.SupIndep`	-1.145⬝10⁹	(-6.64%)
`Mathlib.GroupTheory.Exponent`	-1.146⬝10⁹	(-4.29%)
`Mathlib.Order.Bounds.Image`	-1.147⬝10⁹	(-10.91%)
`Mathlib.FieldTheory.Relrank`	-1.147⬝10⁹	(-0.46%)
`Mathlib.Analysis.SpecialFunctions.Log.Base`	-1.148⬝10⁹	(-4.24%)
`Mathlib.SetTheory.Ordinal.Exponential`	-1.149⬝10⁹	(-7.04%)
`Mathlib.Algebra.MonoidAlgebra.Basic`	-1.150⬝10⁹	(-2.43%)
`Mathlib.Algebra.Star.Basic`	-1.152⬝10⁹	(-7.11%)
`Mathlib.Topology.Homotopy.Basic`	-1.152⬝10⁹	(-2.57%)
`Mathlib.Combinatorics.Colex`	-1.152⬝10⁹	(-4.08%)
`Mathlib.RingTheory.DedekindDomain.Different`	-1.153⬝10⁹	(-0.51%)
`Mathlib.MeasureTheory.Integral.DominatedConvergence`	-1.154⬝10⁹	(-2.61%)
`Mathlib.Data.Rat.Defs`	-1.155⬝10⁹	(-9.57%)
`Mathlib.Analysis.Normed.Module.Basic`	-1.155⬝10⁹	(-2.53%)
`Mathlib.CategoryTheory.Adjunction.Mates`	-1.164⬝10⁹	(-1.45%)
`Mathlib.RingTheory.AdicCompletion.Basic`	-1.167⬝10⁹	(-1.43%)
`Mathlib.NumberTheory.Pell`	-1.167⬝10⁹	(-2.55%)
`Mathlib.MeasureTheory.MeasurableSpace.Defs`	-1.168⬝10⁹	(-8.92%)
`Mathlib.Probability.Martingale.Basic`	-1.168⬝10⁹	(-3.42%)
`Mathlib.RingTheory.Adjoin.Basic`	-1.169⬝10⁹	(-3.19%)
`Mathlib.RingTheory.Polynomial.Cyclotomic.Basic`	-1.174⬝10⁹	(-2.56%)
`Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal`	-1.177⬝10⁹	(-4.36%)
`Mathlib.MeasureTheory.Measure.Lebesgue.Basic`	-1.178⬝10⁹	(-2.72%)
`Mathlib.GroupTheory.PushoutI`	-1.178⬝10⁹	(-1.39%)
`Mathlib.Algebra.MonoidAlgebra.Degree`	-1.179⬝10⁹	(-2.12%)
`Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic`	-1.179⬝10⁹	(-2.00%)
`Mathlib.CategoryTheory.Limits.Shapes.Reflexive`	-1.181⬝10⁹	(-1.87%)
`Mathlib.Data.Matrix.Kronecker`	-1.186⬝10⁹	(-2.40%)
`Mathlib.CategoryTheory.Functor.KanExtension.Basic`	-1.187⬝10⁹	(-1.12%)
`Mathlib.Algebra.GroupWithZero.Units.Basic`	-1.188⬝10⁹	(-8.12%)
`Mathlib.Data.Finset.Max`	-1.189⬝10⁹	(-6.68%)
`Mathlib.Logic.Equiv.TransferInstance`	-1.190⬝10⁹	(-3.48%)
`Mathlib.MeasureTheory.Integral.CircleIntegral`	-1.190⬝10⁹	(-1.70%)
`Mathlib.Algebra.Ring.CentroidHom`	-1.192⬝10⁹	(-2.20%)
`Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody`	-1.193⬝10⁹	(-0.75%)
`Mathlib.Analysis.CStarAlgebra.Multiplier`	-1.193⬝10⁹	(-0.72%)
`Mathlib.Topology.MetricSpace.Gluing`	-1.194⬝10⁹	(-5.36%)
`Mathlib.RingTheory.IsAdjoinRoot`	-1.195⬝10⁹	(-2.15%)
`Mathlib.Topology.Sets.Compacts`	-1.195⬝10⁹	(-8.26%)
`Mathlib.RingTheory.Regular.RegularSequence`	-1.196⬝10⁹	(-1.48%)
`Mathlib.MeasureTheory.Measure.Haar.Basic`	-1.197⬝10⁹	(-3.33%)
`Mathlib.RingTheory.HahnSeries.Summable`	-1.198⬝10⁹	(-1.88%)
`Mathlib.Order.CompactlyGenerated.Basic`	-1.198⬝10⁹	(-5.84%)
`Mathlib.Topology.Order.LocalExtr`	-1.198⬝10⁹	(-6.61%)
`Mathlib.Algebra.Group.Subgroup.Pointwise`	-1.199⬝10⁹	(-3.11%)
`Mathlib.Algebra.Group.AddChar`	-1.201⬝10⁹	(-5.26%)
`Mathlib.LinearAlgebra.DFinsupp`	-1.201⬝10⁹	(-2.19%)
`Mathlib.GroupTheory.HNNExtension`	-1.202⬝10⁹	(-1.12%)
`Mathlib.AlgebraicGeometry.Pullbacks`	-1.202⬝10⁹	(-0.94%)
`Mathlib.Algebra.Polynomial.Monic`	-1.203⬝10⁹	(-4.29%)
`Mathlib.Topology.UniformSpace.Completion`	-1.204⬝10⁹	(-6.92%)
`Mathlib.RingTheory.Localization.Away.Basic`	-1.208⬝10⁹	(-2.04%)
`Mathlib.Topology.Algebra.Module.StrongTopology`	-1.211⬝10⁹	(-1.14%)
`Mathlib.Analysis.Normed.Module.FiniteDimension`	-1.212⬝10⁹	(-1.18%)
`Mathlib.Analysis.Analytic.CPolynomial`	-1.212⬝10⁹	(-0.90%)
`Mathlib.CategoryTheory.Triangulated.Pretriangulated`	-1.216⬝10⁹	(-2.70%)
`Mathlib.Topology.Algebra.Module.Multilinear.Basic`	-1.217⬝10⁹	(-2.48%)
`Mathlib.Algebra.Ring.Hom.Defs`	-1.218⬝10⁹	(-6.61%)
`Mathlib.LinearAlgebra.Span.Defs`	-1.219⬝10⁹	(-4.78%)
`Mathlib.Analysis.Matrix`	-1.219⬝10⁹	(-2.23%)
`Mathlib.Algebra.RingQuot`	-1.219⬝10⁹	(-3.47%)
`Mathlib.CategoryTheory.GradedObject.Monoidal`	-1.220⬝10⁹	(-1.34%)
`Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass`	-1.227⬝10⁹	(-2.36%)
`Mathlib.Analysis.Convex.Cone.Basic`	-1.228⬝10⁹	(-3.96%)
`Mathlib.Data.Nat.Factorization.Basic`	-1.229⬝10⁹	(-4.98%)
`Mathlib.CategoryTheory.Monoidal.Mon_`	-1.229⬝10⁹	(-0.79%)
`Mathlib.Analysis.Convex.Gauge`	-1.230⬝10⁹	(-2.11%)
`Mathlib.Order.Interval.Set.Image`	-1.230⬝10⁹	(-11.02%)
`Mathlib.Logic.Encodable.Basic`	-1.231⬝10⁹	(-11.39%)
`Mathlib.GroupTheory.Perm.Sign`	-1.234⬝10⁹	(-3.83%)
`Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms`	-1.234⬝10⁹	(-6.93%)
`Mathlib.Order.Partition.Finpartition`	-1.236⬝10⁹	(-5.12%)
`Mathlib.CategoryTheory.Sites.Sheaf`	-1.237⬝10⁹	(-1.54%)
`Mathlib.Geometry.Manifold.VectorBundle.Basic`	-1.238⬝10⁹	(-2.14%)
`Mathlib.NumberTheory.LucasLehmer`	-1.239⬝10⁹	(-2.61%)
`Mathlib.Topology.LocallyConstant.Basic`	-1.241⬝10⁹	(-8.29%)
`Mathlib.Topology.FiberBundle.Basic`	-1.243⬝10⁹	(-6.32%)
`Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet`	-1.245⬝10⁹	(-3.84%)
`Mathlib.CategoryTheory.Abelian.Basic`	-1.245⬝10⁹	(-2.72%)
`Mathlib.RingTheory.Ideal.Over`	-1.246⬝10⁹	(-1.52%)
`Mathlib.Data.PFunctor.Univariate.M`	-1.246⬝10⁹	(-8.22%)
`Mathlib.MeasureTheory.Function.AEEqOfIntegral`	-1.246⬝10⁹	(-3.67%)
`Mathlib.Topology.Instances.AddCircle`	-1.247⬝10⁹	(-2.51%)
`Mathlib.Analysis.SpecialFunctions.Log.Basic`	-1.249⬝10⁹	(-4.15%)
`Mathlib.Topology.ContinuousMap.ZeroAtInfty`	-1.249⬝10⁹	(-2.75%)
`Mathlib.Algebra.Order.Interval.Basic`	-1.250⬝10⁹	(-3.54%)
`Mathlib.Order.Filter.Prod`	-1.250⬝10⁹	(-7.11%)
`Mathlib.Topology.MetricSpace.Thickening`	-1.252⬝10⁹	(-5.29%)
`Mathlib.Data.PFun`	-1.253⬝10⁹	(-8.80%)
`Mathlib.Algebra.BigOperators.Finsupp`	-1.255⬝10⁹	(-4.02%)
`Mathlib.Topology.Compactification.OnePoint`	-1.257⬝10⁹	(-8.04%)
`Mathlib.NumberTheory.Padics.PadicVal.Basic`	-1.258⬝10⁹	(-4.84%)
`Mathlib.Deprecated.Subgroup`	-1.258⬝10⁹	(-4.66%)
`Mathlib.Data.Real.Irrational`	-1.259⬝10⁹	(-7.21%)
`Mathlib.Analysis.Normed.Algebra.Exponential`	-1.259⬝10⁹	(-2.19%)
`Mathlib.RingTheory.FractionalIdeal.Basic`	-1.261⬝10⁹	(-2.02%)
`Mathlib.GroupTheory.Index`	-1.264⬝10⁹	(-4.41%)
`Mathlib.Algebra.Order.BigOperators.Group.Finset`	-1.267⬝10⁹	(-5.20%)
`Mathlib.LinearAlgebra.Matrix.Transvection`	-1.268⬝10⁹	(-2.86%)
`Mathlib.MeasureTheory.Measure.FiniteMeasure`	-1.272⬝10⁹	(-2.14%)
`Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries`	-1.273⬝10⁹	(-0.66%)
`Mathlib.Algebra.Group.Units.Defs`	-1.273⬝10⁹	(-7.51%)
`Mathlib.Data.Set.Pointwise.SMul`	-1.274⬝10⁹	(-3.28%)
`Mathlib.Topology.Algebra.Module.Alternating.Basic`	-1.276⬝10⁹	(-2.21%)
`Mathlib.NumberTheory.Padics.PadicIntegers`	-1.277⬝10⁹	(-1.92%)
`Mathlib.Order.Interval.Basic`	-1.278⬝10⁹	(-6.35%)
`Mathlib.Data.Sym.Basic`	-1.280⬝10⁹	(-8.01%)
`Mathlib.LinearAlgebra.Lagrange`	-1.281⬝10⁹	(-3.11%)
`Mathlib.MeasureTheory.Measure.WithDensity`	-1.282⬝10⁹	(-4.62%)
`Mathlib.NumberTheory.Cyclotomic.Basic`	-1.283⬝10⁹	(-1.51%)
`Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms`	-1.285⬝10⁹	(-2.40%)
`Mathlib.Algebra.Module.ZLattice.Basic`	-1.285⬝10⁹	(-0.80%)
`Mathlib.Analysis.Complex.PhragmenLindelof`	-1.285⬝10⁹	(-2.53%)
`Mathlib.RingTheory.Perfection`	-1.286⬝10⁹	(-1.85%)
`Mathlib.Computability.AkraBazzi.GrowsPolynomially`	-1.287⬝10⁹	(-2.30%)
`Mathlib.Dynamics.PeriodicPts`	-1.290⬝10⁹	(-8.14%)
`Mathlib.LinearAlgebra.Span.Basic`	-1.293⬝10⁹	(-3.64%)
`Mathlib.Probability.Kernel.Disintegration.CDFToKernel`	-1.294⬝10⁹	(-4.33%)
`Mathlib.Algebra.Polynomial.Degree.Definitions`	-1.295⬝10⁹	(-6.18%)
`Mathlib.Algebra.Order.Monovary`	-1.296⬝10⁹	(-2.61%)
`Mathlib.Data.Finset.NAry`	-1.297⬝10⁹	(-6.97%)
`Mathlib.CategoryTheory.Groupoid.Subgroupoid`	-1.300⬝10⁹	(-4.89%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances`	-1.303⬝10⁹	(-0.36%)
`Mathlib.MeasureTheory.Constructions.BorelSpace.Basic`	-1.303⬝10⁹	(-6.45%)
`Mathlib.MeasureTheory.Function.LocallyIntegrable`	-1.303⬝10⁹	(-3.89%)
`Mathlib.Analysis.Convex.Combination`	-1.305⬝10⁹	(-1.10%)
`Mathlib.Algebra.Field.Subfield.Basic`	-1.305⬝10⁹	(-3.73%)
`Mathlib.Tactic.NormNum.Basic`	-1.307⬝10⁹	(-2.73%)
`Mathlib.Data.Real.Basic`	-1.308⬝10⁹	(-3.27%)
`Mathlib.Topology.Order.IntermediateValue`	-1.312⬝10⁹	(-2.61%)
`Mathlib.Probability.Martingale.Upcrossing`	-1.316⬝10⁹	(-3.72%)
`Mathlib.Logic.Equiv.Set`	-1.318⬝10⁹	(-7.43%)
`Mathlib.GroupTheory.Congruence.Defs`	-1.318⬝10⁹	(-4.59%)
`Mathlib.Data.List.Rotate`	-1.318⬝10⁹	(-9.54%)
`Mathlib.Topology.MetricSpace.Isometry`	-1.322⬝10⁹	(-6.29%)
`Mathlib.Algebra.GradedMonoid`	-1.323⬝10⁹	(-8.61%)
`Mathlib.AlgebraicGeometry.OpenImmersion`	-1.323⬝10⁹	(-1.86%)
`Mathlib.LinearAlgebra.Matrix.SesquilinearForm`	-1.324⬝10⁹	(-1.04%)
`Mathlib.LinearAlgebra.Pi`	-1.327⬝10⁹	(-2.86%)
`Mathlib.Algebra.Group.Equiv.Basic`	-1.327⬝10⁹	(-6.31%)
`Mathlib.Order.BoundedOrder.Basic`	-1.327⬝10⁹	(-13.86%)
`Mathlib.Analysis.Calculus.Deriv.Basic`	-1.330⬝10⁹	(-2.49%)
`Mathlib.GroupTheory.Perm.Cycle.Type`	-1.332⬝10⁹	(-5.12%)
`Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle`	-1.332⬝10⁹	(-1.99%)
`Mathlib.RingTheory.AlgebraicIndependent`	-1.332⬝10⁹	(-0.97%)
`Mathlib.Order.Filter.Extr`	-1.336⬝10⁹	(-10.27%)
`Mathlib.Algebra.Group.UniqueProds.Basic`	-1.337⬝10⁹	(-3.26%)
`Mathlib.Algebra.Polynomial.FieldDivision`	-1.338⬝10⁹	(-2.78%)
`Mathlib.MeasureTheory.PiSystem`	-1.339⬝10⁹	(-7.50%)
`Mathlib.GroupTheory.OreLocalization.Basic`	-1.341⬝10⁹	(-2.66%)
`Mathlib.Algebra.Homology.ShortComplex.Preadditive`	-1.341⬝10⁹	(-1.35%)
`Mathlib.LinearAlgebra.Ray`	-1.344⬝10⁹	(-2.12%)
`Mathlib.Algebra.Module.Equiv.Basic`	-1.346⬝10⁹	(-3.49%)
`Mathlib.Geometry.Manifold.LocalInvariantProperties`	-1.347⬝10⁹	(-6.05%)
`Mathlib.CategoryTheory.Limits.VanKampen`	-1.347⬝10⁹	(-2.06%)
`Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme`	-1.354⬝10⁹	(-0.62%)
`Mathlib.Algebra.GeomSum`	-1.356⬝10⁹	(-2.58%)
`Mathlib.GroupTheory.Perm.Basic`	-1.359⬝10⁹	(-8.45%)
`Mathlib.Algebra.Homology.ShortComplex.PreservesHomology`	-1.359⬝10⁹	(-2.64%)
`Mathlib.Data.ENNReal.Real`	-1.360⬝10⁹	(-4.80%)
`Mathlib.RingTheory.FiniteType`	-1.361⬝10⁹	(-1.60%)
`Mathlib.Data.ENNReal.Operations`	-1.361⬝10⁹	(-3.19%)
`Mathlib.RingTheory.Jacobson`	-1.362⬝10⁹	(-1.48%)
`Mathlib.MeasureTheory.MeasurableSpace.Embedding`	-1.364⬝10⁹	(-5.70%)
`Mathlib.Analysis.Normed.Lp.ProdLp`	-1.365⬝10⁹	(-3.00%)
`Mathlib.Topology.Algebra.InfiniteSum.Basic`	-1.365⬝10⁹	(-4.42%)
`Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional`	-1.366⬝10⁹	(-2.90%)
`Mathlib.Data.Finmap`	-1.368⬝10⁹	(-8.75%)
`Mathlib.Analysis.Convex.Segment`	-1.372⬝10⁹	(-2.20%)
`Mathlib.Data.Ordmap.Ordnode`	-1.376⬝10⁹	(-9.31%)
`Mathlib.GroupTheory.Perm.Cycle.Factors`	-1.377⬝10⁹	(-5.47%)
`Mathlib.Algebra.Polynomial.Derivative`	-1.378⬝10⁹	(-2.80%)
`Mathlib.Topology.Algebra.Algebra`	-1.378⬝10⁹	(-3.65%)
`Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic`	-1.378⬝10⁹	(-1.60%)
`Mathlib.MeasureTheory.Measure.Haar.Unique`	-1.378⬝10⁹	(-1.88%)
`Mathlib.RingTheory.Kaehler.Basic`	-1.379⬝10⁹	(-0.38%)
`Mathlib.Algebra.Periodic`	-1.379⬝10⁹	(-3.65%)
`Mathlib.Geometry.Euclidean.Angle.Oriented.Affine`	-1.380⬝10⁹	(-1.88%)
`Mathlib.Algebra.Group.Subgroup.Defs`	-1.380⬝10⁹	(-5.24%)
`Mathlib.Topology.Algebra.Order.LiminfLimsup`	-1.382⬝10⁹	(-4.03%)
`Mathlib.Order.SupClosed`	-1.383⬝10⁹	(-5.98%)
`Mathlib.Order.KrullDimension`	-1.383⬝10⁹	(-2.62%)
`Mathlib.Geometry.Manifold.PartitionOfUnity`	-1.384⬝10⁹	(-2.92%)
`Mathlib.Algebra.Group.Submonoid.Membership`	-1.385⬝10⁹	(-4.54%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric`	-1.387⬝10⁹	(-0.78%)
`Mathlib.Algebra.Homology.HomotopyCategory.MappingCone`	-1.388⬝10⁹	(-1.67%)
`Mathlib.Geometry.Euclidean.Circumcenter`	-1.388⬝10⁹	(-1.36%)
`Mathlib.Algebra.Category.Ring.Basic`	-1.392⬝10⁹	(-3.97%)
`Mathlib.Topology.UniformSpace.UniformEmbedding`	-1.395⬝10⁹	(-7.17%)
`Mathlib.Data.Matrix.Basic`	-1.396⬝10⁹	(-4.15%)
`Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions`	-1.396⬝10⁹	(-1.26%)
`Mathlib.Algebra.Star.SelfAdjoint`	-1.398⬝10⁹	(-4.94%)
`Mathlib.Algebra.Lie.Subalgebra`	-1.399⬝10⁹	(-2.80%)
`Mathlib.Algebra.Lie.Weights.Basic`	-1.401⬝10⁹	(-1.08%)
`Mathlib.CategoryTheory.Subobject.Lattice`	-1.403⬝10⁹	(-1.08%)
`Mathlib.Analysis.Fourier.FourierTransformDeriv`	-1.407⬝10⁹	(-0.33%)
`Mathlib.Analysis.Calculus.FDeriv.Analytic`	-1.409⬝10⁹	(-0.53%)
`Mathlib.Algebra.Homology.BifunctorAssociator`	-1.410⬝10⁹	(-0.73%)
`Mathlib.GroupTheory.Nilpotent`	-1.410⬝10⁹	(-3.11%)
`Mathlib.Algebra.Group.Subsemigroup.Operations`	-1.411⬝10⁹	(-5.23%)
`Mathlib.CategoryTheory.Limits.Types`	-1.411⬝10⁹	(-3.29%)
`Mathlib.GroupTheory.Perm.Support`	-1.413⬝10⁹	(-7.46%)
`Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization`	-1.413⬝10⁹	(-1.07%)
`Mathlib.Combinatorics.SimpleGraph.Clique`	-1.414⬝10⁹	(-4.76%)
`Mathlib.Algebra.Homology.Homotopy`	-1.417⬝10⁹	(-1.88%)
`Mathlib.SetTheory.Cardinal.Aleph`	-1.419⬝10⁹	(-5.00%)
`Mathlib.LinearAlgebra.FiniteDimensional.Defs`	-1.421⬝10⁹	(-2.12%)
`Mathlib.Analysis.SpecialFunctions.Complex.Arg`	-1.423⬝10⁹	(-3.06%)
`Mathlib.CategoryTheory.Shift.Basic`	-1.424⬝10⁹	(-2.02%)
`Mathlib.Order.ConditionallyCompleteLattice.Indexed`	-1.424⬝10⁹	(-6.28%)
`Mathlib.Analysis.BoxIntegral.Basic`	-1.426⬝10⁹	(-1.65%)
`Mathlib.MeasureTheory.Covering.Differentiation`	-1.426⬝10⁹	(-2.59%)
`Mathlib.AlgebraicGeometry.Restrict`	-1.428⬝10⁹	(-1.19%)
`Mathlib.Analysis.Normed.Affine.Isometry`	-1.430⬝10⁹	(-2.32%)
`Mathlib.MeasureTheory.Integral.IntegrableOn`	-1.431⬝10⁹	(-5.48%)
`Mathlib.Topology.FiberBundle.Trivialization`	-1.431⬝10⁹	(-6.45%)
`Mathlib.GroupTheory.GroupAction.Hom`	-1.434⬝10⁹	(-3.33%)
`Mathlib.Algebra.Category.ModuleCat.ChangeOfRings`	-1.434⬝10⁹	(-0.40%)
`Mathlib.Algebra.Polynomial.AlgebraMap`	-1.435⬝10⁹	(-2.84%)
`Mathlib.GroupTheory.SpecificGroups.Cyclic`	-1.436⬝10⁹	(-2.95%)
`Mathlib.Analysis.BoxIntegral.Partition.Basic`	-1.437⬝10⁹	(-5.24%)
`Mathlib.Geometry.Manifold.ContMDiff.Defs`	-1.439⬝10⁹	(-3.67%)
`Mathlib.Topology.EMetricSpace.Defs`	-1.442⬝10⁹	(-4.28%)
`Mathlib.SetTheory.Ordinal.FixedPoint`	-1.451⬝10⁹	(-8.75%)
`Mathlib.NumberTheory.RamificationInertia.Basic`	-1.453⬝10⁹	(-0.73%)
`Mathlib.Order.InitialSeg`	-1.459⬝10⁹	(-8.59%)
`Mathlib.Topology.MetricSpace.HausdorffDistance`	-1.463⬝10⁹	(-5.50%)
`Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer`	-1.464⬝10⁹	(-1.74%)
`Mathlib.Analysis.SpecificLimits.Basic`	-1.465⬝10⁹	(-2.90%)
`Mathlib.GroupTheory.Coprod.Basic`	-1.466⬝10⁹	(-2.45%)
`Mathlib.Tactic.FunProp.RefinedDiscrTree`	-1.466⬝10⁹	(-2.52%)
`Mathlib.Probability.Kernel.Disintegration.Density`	-1.474⬝10⁹	(-1.16%)
`Mathlib.Algebra.Group.Submonoid.Pointwise`	-1.474⬝10⁹	(-4.31%)
`Mathlib.Data.TypeVec`	-1.475⬝10⁹	(-5.59%)
`Mathlib.MeasureTheory.Group.Measure`	-1.477⬝10⁹	(-2.53%)
`Mathlib.LinearAlgebra.Matrix.Determinant.Basic`	-1.479⬝10⁹	(-1.72%)
`Mathlib.Topology.Connected.Basic`	-1.482⬝10⁹	(-9.06%)
`Mathlib.FieldTheory.Separable`	-1.484⬝10⁹	(-3.20%)
`Mathlib.FieldTheory.SeparableDegree`	-1.487⬝10⁹	(-0.75%)
`Mathlib.Analysis.SpecialFunctions.Pow.Deriv`	-1.488⬝10⁹	(-0.97%)
`Mathlib.SetTheory.Ordinal.NaturalOps`	-1.491⬝10⁹	(-3.77%)
`Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots`	-1.494⬝10⁹	(-3.21%)
`Mathlib.Order.Hom.Bounded`	-1.495⬝10⁹	(-8.46%)
`Mathlib.CategoryTheory.Yoneda`	-1.498⬝10⁹	(-1.38%)
`Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno`	-1.498⬝10⁹	(-0.82%)
`Mathlib.Order.BooleanAlgebra`	-1.500⬝10⁹	(-4.68%)
`Mathlib.Data.Sum.Order`	-1.502⬝10⁹	(-7.11%)
`Mathlib.Algebra.Module.Submodule.Map`	-1.502⬝10⁹	(-3.72%)
`Mathlib.GroupTheory.Complement`	-1.505⬝10⁹	(-2.61%)
`Mathlib.Order.RelIso.Basic`	-1.508⬝10⁹	(-10.14%)
`Mathlib.Analysis.Convex.Deriv`	-1.508⬝10⁹	(-3.04%)
`Mathlib.RingTheory.NonUnitalSubsemiring.Basic`	-1.509⬝10⁹	(-5.32%)
`Mathlib.Algebra.Free`	-1.511⬝10⁹	(-5.59%)
`Mathlib.Data.Matroid.Map`	-1.512⬝10⁹	(-7.67%)
`Mathlib.Topology.Compactness.Lindelof`	-1.513⬝10⁹	(-8.70%)
`Mathlib.Data.Nat.PartENat`	-1.513⬝10⁹	(-6.94%)
`Mathlib.RingTheory.Valuation.ValuationSubring`	-1.516⬝10⁹	(-1.08%)
`Mathlib.Algebra.Algebra.Operations`	-1.517⬝10⁹	(-1.79%)
`Mathlib.RingTheory.AdjoinRoot`	-1.517⬝10⁹	(-1.09%)
`Mathlib.Algebra.Lie.Nilpotent`	-1.519⬝10⁹	(-2.28%)
`Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar`	-1.521⬝10⁹	(-1.40%)
`Mathlib.RingTheory.Multiplicity`	-1.523⬝10⁹	(-3.40%)
`Mathlib.Combinatorics.Enumerative.IncidenceAlgebra`	-1.529⬝10⁹	(-2.58%)
`Mathlib.NumberTheory.LSeries.HurwitzZetaEven`	-1.530⬝10⁹	(-2.36%)
`Mathlib.Algebra.Group.Prod`	-1.530⬝10⁹	(-5.83%)
`Mathlib.MeasureTheory.Constructions.Polish.Basic`	-1.531⬝10⁹	(-6.09%)
`Mathlib.Data.Stream.Init`	-1.537⬝10⁹	(-11.58%)
`Mathlib.FieldTheory.IntermediateField.Basic`	-1.539⬝10⁹	(-1.16%)
`Mathlib.Order.RelSeries`	-1.541⬝10⁹	(-3.52%)
`Mathlib.Logic.Relation`	-1.542⬝10⁹	(-15.81%)
`Mathlib.Data.List.Sigma`	-1.543⬝10⁹	(-7.09%)
`Mathlib.Data.Sym.Sym2`	-1.544⬝10⁹	(-6.31%)
`Mathlib.Algebra.Algebra.Equiv`	-1.546⬝10⁹	(-3.63%)
`Mathlib.GroupTheory.Sylow`	-1.549⬝10⁹	(-3.25%)
`Mathlib.Algebra.Order.Ring.Unbundled.Basic`	-1.549⬝10⁹	(-3.47%)
`Mathlib.Algebra.Order.Monoid.Unbundled.WithTop`	-1.550⬝10⁹	(-9.03%)
`Mathlib.Topology.MetricSpace.PiNat`	-1.551⬝10⁹	(-4.17%)
`Mathlib.Analysis.Calculus.FDeriv.Add`	-1.552⬝10⁹	(-1.90%)
`Mathlib.Combinatorics.Enumerative.Composition`	-1.554⬝10⁹	(-4.98%)
`Mathlib.AlgebraicGeometry.Scheme`	-1.556⬝10⁹	(-1.48%)
`Mathlib.Data.Nat.Digits`	-1.557⬝10⁹	(-4.83%)
`Mathlib.RingTheory.NonUnitalSubring.Basic`	-1.560⬝10⁹	(-5.29%)
`Mathlib.Probability.StrongLaw`	-1.561⬝10⁹	(-1.92%)
`Mathlib.Order.SymmDiff`	-1.567⬝10⁹	(-6.61%)
`Mathlib.Order.Cover`	-1.567⬝10⁹	(-10.04%)
`Mathlib.ModelTheory.Basic`	-1.568⬝10⁹	(-7.20%)
`Mathlib.NumberTheory.FLT.Three`	-1.568⬝10⁹	(-1.22%)
`Mathlib.LinearAlgebra.Matrix.NonsingularInverse`	-1.569⬝10⁹	(-2.88%)
`Mathlib.RingTheory.HahnSeries.Multiplication`	-1.570⬝10⁹	(-1.81%)
`Mathlib.Data.Finset.Basic`	-1.571⬝10⁹	(-8.78%)
`Mathlib.CategoryTheory.Limits.Cones`	-1.573⬝10⁹	(-0.59%)
`Mathlib.Algebra.Polynomial.Roots`	-1.573⬝10⁹	(-3.52%)
`Mathlib.Probability.Independence.Conditional`	-1.575⬝10⁹	(-5.81%)
`Mathlib.LinearAlgebra.SesquilinearForm`	-1.582⬝10⁹	(-1.87%)
`Mathlib.Algebra.Polynomial.Div`	-1.583⬝10⁹	(-3.35%)
`Mathlib.Data.Finset.Insert`	-1.583⬝10⁹	(-11.29%)
`Mathlib.ModelTheory.Syntax`	-1.590⬝10⁹	(-6.28%)
`Mathlib.Analysis.Normed.Group.Seminorm`	-1.594⬝10⁹	(-4.75%)
`Mathlib.Algebra.Order.Hom.Monoid`	-1.605⬝10⁹	(-4.75%)
`Mathlib.Topology.Order.Basic`	-1.608⬝10⁹	(-4.04%)
`Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex`	-1.608⬝10⁹	(-2.98%)
`Mathlib.Analysis.Convex.Basic`	-1.611⬝10⁹	(-3.39%)
`Mathlib.Analysis.Complex.Basic`	-1.612⬝10⁹	(-2.52%)
`Mathlib.MeasureTheory.Integral.Average`	-1.612⬝10⁹	(-2.73%)
`Mathlib.Data.Matroid.Closure`	-1.613⬝10⁹	(-3.17%)
`Mathlib.RingTheory.MvPowerSeries.Basic`	-1.617⬝10⁹	(-2.40%)
`Mathlib.NumberTheory.Dioph`	-1.619⬝10⁹	(-4.41%)
`Mathlib.Analysis.SpecialFunctions.Integrals`	-1.619⬝10⁹	(-1.89%)
`Mathlib.Data.Vector.Basic`	-1.622⬝10⁹	(-8.38%)
`Mathlib.AlgebraicTopology.SimplicialObject`	-1.622⬝10⁹	(-0.82%)
`Mathlib.CategoryTheory.Sites.Sieves`	-1.623⬝10⁹	(-5.53%)
`Mathlib.Algebra.Ring.Equiv`	-1.631⬝10⁹	(-5.85%)
`Mathlib.CategoryTheory.Filtered.Basic`	-1.631⬝10⁹	(-6.33%)
`Mathlib.Order.Disjoint`	-1.632⬝10⁹	(-10.45%)
`Mathlib.Topology.MetricSpace.GromovHausdorff`	-1.635⬝10⁹	(-1.67%)
`Mathlib.CategoryTheory.Generator`	-1.638⬝10⁹	(-7.04%)
`Mathlib.Algebra.Algebra.Unitization`	-1.640⬝10⁹	(-1.65%)
`Mathlib.Algebra.Polynomial.Degree.Operations`	-1.644⬝10⁹	(-5.33%)
`Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber`	-1.646⬝10⁹	(-4.44%)
`Mathlib.RepresentationTheory.GroupCohomology.LowDegree`	-1.656⬝10⁹	(-1.22%)
`Mathlib.Data.Quot`	-1.656⬝10⁹	(-13.62%)
`Mathlib.Data.Int.Defs`	-1.657⬝10⁹	(-8.72%)
`Mathlib.Analysis.Normed.Group.Hom`	-1.659⬝10⁹	(-3.99%)
`Mathlib.CategoryTheory.Limits.Shapes.Products`	-1.659⬝10⁹	(-2.62%)
`Mathlib.LinearAlgebra.AffineSpace.Independent`	-1.660⬝10⁹	(-3.02%)
`Mathlib.LinearAlgebra.Eigenspace.Basic`	-1.661⬝10⁹	(-1.30%)
`Mathlib.CategoryTheory.Monoidal.Bimod`	-1.666⬝10⁹	(-1.12%)
`Mathlib.LinearAlgebra.Basis.Defs`	-1.668⬝10⁹	(-2.67%)
`Mathlib.Combinatorics.SimpleGraph.Basic`	-1.670⬝10⁹	(-6.91%)
`Mathlib.CategoryTheory.Preadditive.Biproducts`	-1.671⬝10⁹	(-2.01%)
`Mathlib.Topology.ContinuousMap.Algebra`	-1.673⬝10⁹	(-1.73%)
`Mathlib.Algebra.Homology.ShortComplex.Exact`	-1.673⬝10⁹	(-3.71%)
`Mathlib.Order.Filter.Germ.Basic`	-1.679⬝10⁹	(-6.68%)
`Mathlib.LinearAlgebra.AffineSpace.AffineMap`	-1.686⬝10⁹	(-1.51%)
`Mathlib.MeasureTheory.Group.FundamentalDomain`	-1.688⬝10⁹	(-1.16%)
`Mathlib.Topology.Inseparable`	-1.688⬝10⁹	(-9.24%)
`Mathlib.Topology.Algebra.Monoid`	-1.690⬝10⁹	(-4.03%)
`Mathlib.Topology.UniformSpace.UniformConvergence`	-1.693⬝10⁹	(-6.51%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital`	-1.694⬝10⁹	(-0.75%)
`Mathlib.Analysis.MeanInequalities`	-1.695⬝10⁹	(-2.49%)
`Mathlib.Analysis.SpecificLimits.Normed`	-1.697⬝10⁹	(-2.62%)
`Mathlib.Probability.Independence.Basic`	-1.700⬝10⁹	(-6.08%)
`Mathlib.Algebra.Module.Torsion`	-1.705⬝10⁹	(-2.16%)
`Mathlib.Topology.VectorBundle.Basic`	-1.712⬝10⁹	(-2.78%)
`Mathlib.Order.Minimal`	-1.712⬝10⁹	(-7.34%)
`Mathlib.CategoryTheory.Limits.IsLimit`	-1.712⬝10⁹	(-1.93%)
`Mathlib.Data.Finset.Image`	-1.715⬝10⁹	(-8.20%)
`Mathlib.Data.ENNReal.Basic`	-1.716⬝10⁹	(-6.15%)
`Mathlib.MeasureTheory.Measure.Regular`	-1.716⬝10⁹	(-4.69%)
`Mathlib.Analysis.LocallyConvex.WithSeminorms`	-1.716⬝10⁹	(-1.77%)
`Mathlib.CategoryTheory.Limits.Shapes.Images`	-1.717⬝10⁹	(-4.85%)
`Mathlib.Analysis.Normed.Algebra.Spectrum`	-1.717⬝10⁹	(-1.24%)
`Mathlib.GroupTheory.FreeGroup.Basic`	-1.725⬝10⁹	(-4.35%)
`Mathlib.Analysis.Normed.Lp.PiLp`	-1.732⬝10⁹	(-2.29%)
`Mathlib.Analysis.Convex.Between`	-1.737⬝10⁹	(-0.90%)
`Mathlib.Order.CompleteBooleanAlgebra`	-1.738⬝10⁹	(-4.22%)
`Mathlib.Analysis.BoundedVariation`	-1.743⬝10⁹	(-3.09%)
`Mathlib.Algebra.Star.StarAlgHom`	-1.743⬝10⁹	(-3.77%)
`Mathlib.Topology.Maps.Basic`	-1.744⬝10⁹	(-11.81%)
`Mathlib.Order.Hom.CompleteLattice`	-1.744⬝10⁹	(-8.49%)
`Mathlib.Algebra.BigOperators.Group.List`	-1.747⬝10⁹	(-5.86%)
`Mathlib.Computability.PartrecCode`	-1.748⬝10⁹	(-1.95%)
`Mathlib.RingTheory.Valuation.Basic`	-1.748⬝10⁹	(-4.02%)
`Mathlib.NumberTheory.PellMatiyasevic`	-1.749⬝10⁹	(-3.83%)
`Mathlib.Data.Part`	-1.755⬝10⁹	(-8.94%)
`Mathlib.Data.Real.Hyperreal`	-1.755⬝10⁹	(-5.91%)
`Mathlib.Algebra.Group.Subgroup.Basic`	-1.756⬝10⁹	(-4.73%)
`Mathlib.AlgebraicGeometry.StructureSheaf`	-1.761⬝10⁹	(-1.05%)
`Mathlib.RingTheory.FractionalIdeal.Operations`	-1.761⬝10⁹	(-1.68%)
`Mathlib.CategoryTheory.Monoidal.Braided.Basic`	-1.763⬝10⁹	(-2.13%)
`Mathlib.MeasureTheory.Function.UniformIntegrable`	-1.764⬝10⁹	(-3.08%)
`Mathlib.Topology.UniformSpace.Equicontinuity`	-1.765⬝10⁹	(-8.14%)
`Mathlib.CategoryTheory.Limits.Shapes.Types`	-1.767⬝10⁹	(-4.18%)
`Mathlib.CategoryTheory.Limits.Final`	-1.767⬝10⁹	(-0.97%)
`Mathlib.Algebra.Polynomial.Eval.Defs`	-1.770⬝10⁹	(-5.74%)
`Mathlib.MeasureTheory.Covering.Besicovitch`	-1.773⬝10⁹	(-3.73%)
`Mathlib.Algebra.Star.Subalgebra`	-1.776⬝10⁹	(-2.22%)
`Mathlib.Algebra.Associated.Basic`	-1.776⬝10⁹	(-7.08%)
`Mathlib.Analysis.Analytic.Composition`	-1.784⬝10⁹	(-1.08%)
`Mathlib.Algebra.Order.Group.Unbundled.Basic`	-1.785⬝10⁹	(-6.12%)
`Mathlib.Topology.UniformSpace.UniformConvergenceTopology`	-1.786⬝10⁹	(-4.58%)
`Mathlib.Data.Matrix.Block`	-1.787⬝10⁹	(-3.26%)
`Mathlib.AlgebraicTopology.SimplexCategory`	-1.792⬝10⁹	(-3.42%)
`Mathlib.Computability.Partrec`	-1.793⬝10⁹	(-6.37%)
`Mathlib.CategoryTheory.Comma.StructuredArrow.Basic`	-1.794⬝10⁹	(-0.84%)
`Mathlib.LinearAlgebra.PiTensorProduct`	-1.796⬝10⁹	(-1.23%)
`Mathlib.Logic.Equiv.PartialEquiv`	-1.799⬝10⁹	(-8.40%)
`Mathlib.Algebra.Homology.HomotopyCategory.HomComplex`	-1.799⬝10⁹	(-2.19%)
`Mathlib.RingTheory.PowerSeries.Basic`	-1.800⬝10⁹	(-3.93%)
`Mathlib.Data.List.Cycle`	-1.804⬝10⁹	(-6.74%)
`Mathlib.Geometry.Euclidean.Angle.Oriented.Basic`	-1.805⬝10⁹	(-1.29%)
`Mathlib.Analysis.Convex.Side`	-1.809⬝10⁹	(-2.18%)
`Mathlib.FieldTheory.PurelyInseparable`	-1.812⬝10⁹	(-0.83%)
`Mathlib.Topology.UniformSpace.Cauchy`	-1.814⬝10⁹	(-7.11%)
`Mathlib.RingTheory.Ideal.Quotient.Operations`	-1.815⬝10⁹	(-1.45%)
`Mathlib.Analysis.Calculus.ContDiff.Defs`	-1.817⬝10⁹	(-1.25%)
`Mathlib.AlgebraicGeometry.EllipticCurve.Affine`	-1.839⬝10⁹	(-1.11%)
`Mathlib.MeasureTheory.Function.AEEqFun`	-1.840⬝10⁹	(-5.02%)
`Mathlib.MeasureTheory.Decomposition.Lebesgue`	-1.848⬝10⁹	(-2.69%)
`Mathlib.Order.GaloisConnection`	-1.850⬝10⁹	(-9.28%)
`Mathlib.MeasureTheory.Group.Arithmetic`	-1.854⬝10⁹	(-4.23%)
`Mathlib.Order.ConditionallyCompleteLattice.Basic`	-1.855⬝10⁹	(-6.72%)
`Mathlib.Analysis.InnerProductSpace.PiL2`	-1.856⬝10⁹	(-1.01%)
`Mathlib.Data.Finset.Sups`	-1.857⬝10⁹	(-5.91%)
`Mathlib.Data.Finset.Card`	-1.859⬝10⁹	(-7.98%)
`Mathlib.CategoryTheory.Limits.Preserves.Basic`	-1.859⬝10⁹	(-6.46%)
`Mathlib.AlgebraicGeometry.AffineScheme`	-1.860⬝10⁹	(-0.78%)
`Mathlib.CategoryTheory.Comma.Over`	-1.862⬝10⁹	(-0.58%)
`Mathlib.MeasureTheory.Function.SimpleFuncDenseLp`	-1.862⬝10⁹	(-1.73%)
`Mathlib.RingTheory.Localization.Defs`	-1.864⬝10⁹	(-2.41%)
`Mathlib.Analysis.Calculus.FDeriv.Measurable`	-1.866⬝10⁹	(-1.83%)
`Mathlib.CategoryTheory.Localization.CalculusOfFractions`	-1.867⬝10⁹	(-4.64%)
`Mathlib.CategoryTheory.ComposableArrows`	-1.871⬝10⁹	(-0.62%)
`Mathlib.Algebra.Homology.ShortComplex.LeftHomology`	-1.873⬝10⁹	(-3.53%)
`Mathlib.LinearAlgebra.Matrix.ToLin`	-1.873⬝10⁹	(-1.38%)
`Mathlib.MeasureTheory.Measure.Prod`	-1.877⬝10⁹	(-3.47%)
`Mathlib.LinearAlgebra.Alternating.Basic`	-1.884⬝10⁹	(-2.37%)
`Mathlib.Algebra.Ring.Subsemiring.Basic`	-1.891⬝10⁹	(-5.71%)
`Mathlib.Algebra.Homology.ShortComplex.Homology`	-1.899⬝10⁹	(-4.62%)
`Mathlib.FieldTheory.RatFunc.Basic`	-1.901⬝10⁹	(-0.82%)
`Mathlib.GroupTheory.CoprodI`	-1.901⬝10⁹	(-2.80%)
`Mathlib.Algebra.Homology.HomologicalComplex`	-1.902⬝10⁹	(-4.98%)
`Mathlib.Analysis.Analytic.Constructions`	-1.905⬝10⁹	(-1.60%)
`Mathlib.RingTheory.Algebraic`	-1.912⬝10⁹	(-1.49%)
`Mathlib.SetTheory.Cardinal.Arithmetic`	-1.914⬝10⁹	(-5.81%)
`Mathlib.Algebra.BigOperators.Finprod`	-1.920⬝10⁹	(-4.09%)
`Mathlib.Analysis.Calculus.MeanValue`	-1.935⬝10⁹	(-2.42%)
`Mathlib.SetTheory.Game.Basic`	-1.938⬝10⁹	(-2.64%)
`Mathlib.Order.RelClasses`	-1.956⬝10⁹	(-14.98%)
`Mathlib.Analysis.Normed.Operator.LinearIsometry`	-1.962⬝10⁹	(-1.13%)
`Mathlib.LinearAlgebra.AffineSpace.Combination`	-1.969⬝10⁹	(-2.85%)
`Mathlib.Order.WellFoundedSet`	-1.976⬝10⁹	(-8.40%)
`Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle`	-1.982⬝10⁹	(-3.31%)
`Mathlib.MeasureTheory.Function.Jacobian`	-1.983⬝10⁹	(-1.04%)
`Mathlib.Algebra.DirectLimit`	-1.984⬝10⁹	(-1.43%)
`Mathlib.MeasureTheory.Measure.Hausdorff`	-1.990⬝10⁹	(-2.70%)
`Mathlib.Algebra.Module.LinearMap.Defs`	-1.991⬝10⁹	(-3.80%)
`Mathlib.Data.Matroid.Basic`	-1.999⬝10⁹	(-8.76%)

136 files, Instructions -3.0⬝10⁹

File	Instructions	%
`Mathlib.NumberTheory.Padics.PadicNumbers`	-2.1⬝10⁹	(-3.27%)
`Mathlib.Geometry.RingedSpace.OpenImmersion`	-2.1⬝10⁹	(-0.86%)
`Mathlib.Data.Matrix.Mul`	-2.6⬝10⁹	(-3.99%)
`Mathlib.NumberTheory.Zsqrtd.Basic`	-2.11⬝10⁹	(-2.99%)
`Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic`	-2.11⬝10⁹	(-0.78%)
`Mathlib.ModelTheory.Substructures`	-2.12⬝10⁹	(-6.86%)
`Mathlib.Topology.Order.OrderClosed`	-2.13⬝10⁹	(-6.08%)
`Mathlib.Order.OmegaCompletePartialOrder`	-2.15⬝10⁹	(-7.15%)
`Mathlib.Order.Bounds.Basic`	-2.18⬝10⁹	(-11.18%)
`Mathlib.RingTheory.LaurentSeries`	-2.19⬝10⁹	(-1.05%)
`Mathlib.Algebra.Group.Hom.Defs`	-2.24⬝10⁹	(-7.93%)
`Mathlib.Geometry.Manifold.ChartedSpace`	-2.33⬝10⁹	(-7.48%)
`Mathlib.LinearAlgebra.LinearPMap`	-2.36⬝10⁹	(-2.35%)
`Mathlib.ModelTheory.Semantics`	-2.38⬝10⁹	(-5.72%)
`Mathlib.Algebra.Lie.Basic`	-2.41⬝10⁹	(-2.93%)
`Mathlib.Algebra.Order.Group.Pointwise.Interval`	-2.44⬝10⁹	(-1.99%)
`Mathlib.Algebra.Group.Submonoid.Operations`	-2.51⬝10⁹	(-4.61%)
`Mathlib.Algebra.Order.CauSeq.Basic`	-2.60⬝10⁹	(-2.67%)
`Mathlib.Topology.Order`	-2.61⬝10⁹	(-9.92%)
`Mathlib.Tactic.CategoryTheory.Monoidal.Normalize`	-2.62⬝10⁹	(-3.02%)
`Mathlib.Logic.Equiv.Defs`	-2.63⬝10⁹	(-13.13%)
`Mathlib.MeasureTheory.Constructions.Pi`	-2.73⬝10⁹	(-4.47%)
`Mathlib.Analysis.Calculus.FDeriv.Mul`	-2.74⬝10⁹	(-0.55%)
`Mathlib.Topology.Bases`	-2.80⬝10⁹	(-6.14%)
`Mathlib.Algebra.Ring.Subring.Basic`	-2.82⬝10⁹	(-4.60%)
`Mathlib.Data.Seq.Seq`	-2.86⬝10⁹	(-8.46%)
`Mathlib.MeasureTheory.Constructions.BorelSpace.Order`	-2.88⬝10⁹	(-4.08%)
`Mathlib.Data.Complex.Basic`	-2.99⬝10⁹	(-5.55%)
`Mathlib.Topology.Homeomorph`	-2.100⬝10⁹	(-6.60%)
`Mathlib.Algebra.Order.ToIntervalMod`	-2.110⬝10⁹	(-2.64%)
`Mathlib.CategoryTheory.Monoidal.Functor`	-2.116⬝10⁹	(-1.58%)
`Mathlib.Order.SuccPred.Limit`	-2.117⬝10⁹	(-9.28%)
`Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq`	-2.121⬝10⁹	(-4.47%)
`Mathlib.CategoryTheory.Limits.HasLimits`	-2.124⬝10⁹	(-2.78%)
`Mathlib.Data.Set.Finite.Basic`	-2.135⬝10⁹	(-9.79%)
`Mathlib.Tactic.Ring.Basic`	-2.149⬝10⁹	(-1.64%)
`Mathlib.RingTheory.Polynomial.Basic`	-2.149⬝10⁹	(-2.65%)
`Mathlib.CategoryTheory.Limits.Shapes.Kernels`	-2.156⬝10⁹	(-3.50%)
`Mathlib.CategoryTheory.Limits.Shapes.Equalizers`	-2.164⬝10⁹	(-3.67%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital`	-2.166⬝10⁹	(-1.53%)
`Mathlib.Algebra.Group.Defs`	-2.174⬝10⁹	(-10.26%)
`Mathlib.MeasureTheory.Integral.FundThmCalculus`	-2.191⬝10⁹	(-2.45%)
`Mathlib.Algebra.Order.Field.Basic`	-2.194⬝10⁹	(-1.98%)
`Mathlib.Combinatorics.SimpleGraph.Path`	-2.200⬝10⁹	(-9.48%)
`Mathlib.MeasureTheory.Measure.Restrict`	-2.203⬝10⁹	(-5.84%)
`Mathlib.Algebra.Homology.ShortComplex.RightHomology`	-2.212⬝10⁹	(-3.45%)
`Mathlib.Analysis.Normed.Field.Basic`	-2.218⬝10⁹	(-1.97%)
`Mathlib.CategoryTheory.Limits.Opposites`	-2.220⬝10⁹	(-1.40%)
`Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic`	-2.221⬝10⁹	(-4.13%)
`Mathlib.Data.Fintype.Card`	-2.232⬝10⁹	(-12.14%)
`Mathlib.GroupTheory.Perm.Cycle.Basic`	-2.234⬝10⁹	(-5.56%)
`Mathlib.RingTheory.Ideal.Maps`	-2.236⬝10⁹	(-3.38%)
`Mathlib.Order.Filter.Pointwise`	-2.237⬝10⁹	(-6.36%)
`Mathlib.LinearAlgebra.Prod`	-2.243⬝10⁹	(-2.68%)
`Mathlib.Analysis.InnerProductSpace.Projection`	-2.249⬝10⁹	(-1.10%)
`Mathlib.Data.Set.Prod`	-2.253⬝10⁹	(-7.19%)
`Mathlib.Topology.Semicontinuous`	-2.257⬝10⁹	(-4.98%)
`Mathlib.NumberTheory.NumberField.Embeddings`	-2.270⬝10⁹	(-2.07%)
`Mathlib.Analysis.Calculus.FDeriv.Basic`	-2.271⬝10⁹	(-2.12%)
`Mathlib.Data.ENNReal.Inv`	-2.286⬝10⁹	(-3.38%)
`Mathlib.CategoryTheory.Monoidal.Category`	-2.289⬝10⁹	(-2.21%)
`Mathlib.Combinatorics.SimpleGraph.Subgraph`	-2.296⬝10⁹	(-6.54%)
`Mathlib.Geometry.Manifold.MFDeriv.Basic`	-2.302⬝10⁹	(-2.04%)
`Mathlib.Algebra.TrivSqZeroExt`	-2.306⬝10⁹	(-1.95%)
`Mathlib.Data.Seq.Computation`	-2.312⬝10⁹	(-10.19%)
`Mathlib.Analysis.Distribution.SchwartzSpace`	-2.323⬝10⁹	(-1.18%)
`Mathlib.Probability.Process.Stopping`	-2.333⬝10⁹	(-3.80%)
`Mathlib.Order.Heyting.Basic`	-2.337⬝10⁹	(-6.09%)
`Mathlib.Data.Fin.Tuple.Basic`	-2.337⬝10⁹	(-8.34%)
`Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv`	-2.361⬝10⁹	(-1.67%)
`Mathlib.Analysis.Normed.Lp.lpSpace`	-2.361⬝10⁹	(-1.16%)
`Mathlib.GroupTheory.MonoidLocalization.Basic`	-2.375⬝10⁹	(-2.79%)
`Mathlib.Order.Interval.Finset.Basic`	-2.375⬝10⁹	(-7.91%)
`Mathlib.Topology.Compactness.Compact`	-2.376⬝10⁹	(-7.84%)
`Mathlib.Tactic.CC.Addition`	-2.381⬝10⁹	(-2.03%)
`Mathlib.Logic.Function.Basic`	-2.400⬝10⁹	(-17.02%)
`Mathlib.Algebra.Order.Monoid.Unbundled.Basic`	-2.405⬝10⁹	(-8.39%)
`Mathlib.Data.NNReal.Defs`	-2.410⬝10⁹	(-4.04%)
`Mathlib.SetTheory.Ordinal.Notation`	-2.413⬝10⁹	(-4.89%)
`Mathlib.MeasureTheory.Integral.IntervalIntegral`	-2.427⬝10⁹	(-2.53%)
`Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts`	-2.439⬝10⁹	(-2.60%)
`Mathlib.GroupTheory.OrderOfElement`	-2.448⬝10⁹	(-3.20%)
`Mathlib.Data.Set.Card`	-2.457⬝10⁹	(-5.25%)
`Mathlib.Order.Filter.Bases`	-2.459⬝10⁹	(-10.02%)
`Mathlib.Algebra.Module.LocalizedModule.Basic`	-2.474⬝10⁹	(-1.35%)
`Mathlib.Analysis.Convex.Function`	-2.484⬝10⁹	(-2.67%)
`Mathlib.Topology.PartialHomeomorph`	-2.485⬝10⁹	(-6.98%)
`Mathlib.Analysis.NormedSpace.Multilinear.Basic`	-2.486⬝10⁹	(-0.89%)
`Mathlib.Order.Interval.Finset.Defs`	-2.493⬝10⁹	(-8.07%)
`Mathlib.Algebra.Polynomial.Basic`	-2.495⬝10⁹	(-5.44%)
`Mathlib.NumberTheory.ArithmeticFunction`	-2.498⬝10⁹	(-3.20%)
`Mathlib.Order.Hom.Basic`	-2.504⬝10⁹	(-8.11%)
`Mathlib.Analysis.SpecialFunctions.Pow.NNReal`	-2.517⬝10⁹	(-4.59%)
`Mathlib.Algebra.GCDMonoid.Basic`	-2.531⬝10⁹	(-5.23%)
`Mathlib.Topology.Connected.PathConnected`	-2.540⬝10⁹	(-4.22%)
`Mathlib.MeasureTheory.VectorMeasure.Basic`	-2.543⬝10⁹	(-4.87%)
`Mathlib.MeasureTheory.Integral.IntegralEqImproper`	-2.545⬝10⁹	(-2.95%)
`Mathlib.Data.Finsupp.Defs`	-2.545⬝10⁹	(-6.96%)
`Mathlib.Algebra.Algebra.NonUnitalSubalgebra`	-2.552⬝10⁹	(-3.28%)
`Mathlib.Order.Atoms`	-2.559⬝10⁹	(-6.76%)
`Mathlib.SetTheory.Cardinal.Cofinality`	-2.562⬝10⁹	(-6.45%)
`Mathlib.Data.Fintype.Basic`	-2.574⬝10⁹	(-8.39%)
`Mathlib.Algebra.Star.NonUnitalSubalgebra`	-2.575⬝10⁹	(-1.61%)
`Mathlib.Order.Monotone.Basic`	-2.590⬝10⁹	(-12.97%)
`Mathlib.Analysis.RCLike.Basic`	-2.594⬝10⁹	(-2.14%)
`Mathlib.Algebra.Group.Basic`	-2.597⬝10⁹	(-6.48%)
`Mathlib.RingTheory.TensorProduct.Basic`	-2.600⬝10⁹	(-0.84%)
`Mathlib.Analysis.Analytic.Basic`	-2.607⬝10⁹	(-1.12%)
`Mathlib.Topology.MetricSpace.Pseudo.Defs`	-2.608⬝10⁹	(-6.13%)
`Mathlib.LinearAlgebra.LinearIndependent`	-2.624⬝10⁹	(-2.39%)
`Mathlib.RingTheory.DedekindDomain.Ideal`	-2.646⬝10⁹	(-1.26%)
`Mathlib.Logic.Basic`	-2.649⬝10⁹	(-19.56%)
`Mathlib.Analysis.Convolution`	-2.674⬝10⁹	(-0.67%)
`Mathlib.Algebra.Order.Module.Defs`	-2.678⬝10⁹	(-3.24%)
`Mathlib.Probability.Independence.Kernel`	-2.691⬝10⁹	(-4.89%)
`Mathlib.Algebra.Algebra.Subalgebra.Basic`	-2.723⬝10⁹	(-4.27%)
`Mathlib.LinearAlgebra.QuadraticForm.Basic`	-2.730⬝10⁹	(-1.45%)
`Mathlib.Combinatorics.SimpleGraph.Walk`	-2.732⬝10⁹	(-7.15%)
`Mathlib.Order.Lattice`	-2.735⬝10⁹	(-10.92%)
`Mathlib.Probability.Kernel.Composition`	-2.746⬝10⁹	(-5.63%)
`Mathlib.Order.SuccPred.Basic`	-2.757⬝10⁹	(-8.28%)
`Mathlib.Analysis.Seminorm`	-2.775⬝10⁹	(-1.97%)
`Mathlib.Analysis.SpecialFunctions.Pow.Real`	-2.797⬝10⁹	(-4.94%)
`Mathlib.MeasureTheory.Function.SimpleFunc`	-2.828⬝10⁹	(-5.06%)
`Mathlib.Geometry.Manifold.SmoothManifoldWithCorners`	-2.847⬝10⁹	(-5.20%)
`Mathlib.Data.DFinsupp.Defs`	-2.870⬝10⁹	(-6.48%)
`Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic`	-2.877⬝10⁹	(-2.59%)
`Mathlib.RingTheory.Ideal.Operations`	-2.883⬝10⁹	(-3.08%)
`Mathlib.Computability.AkraBazzi.AkraBazzi`	-2.888⬝10⁹	(-1.87%)
`Mathlib.Order.WithBot`	-2.890⬝10⁹	(-9.77%)
`Mathlib.SetTheory.Ordinal.Basic`	-2.917⬝10⁹	(-6.88%)
`Mathlib.Analysis.Normed.Group.Basic`	-2.922⬝10⁹	(-3.73%)
`Mathlib.Data.Finset.Lattice.Fold`	-2.949⬝10⁹	(-5.76%)
`Mathlib.Computability.TMToPartrec`	-2.956⬝10⁹	(-4.92%)
`Mathlib.Algebra.MonoidAlgebra.Defs`	-2.978⬝10⁹	(-3.32%)
`Mathlib.Algebra.Lie.Submodule`	-2.991⬝10⁹	(-2.08%)

45 files, Instructions -4.0⬝10⁹

File	Instructions	%
`Mathlib.Topology.Category.Profinite.Nobeling`	-3.19⬝10⁹	(-2.65%)
`Mathlib.MeasureTheory.Function.LpSeminorm.Basic`	-3.57⬝10⁹	(-3.43%)
`Mathlib.MeasureTheory.Function.L1Space`	-3.71⬝10⁹	(-3.08%)
`Mathlib.Order.Basic`	-3.111⬝10⁹	(-11.46%)
`Mathlib.Data.Seq.WSeq`	-3.132⬝10⁹	(-6.69%)
`Mathlib.LinearAlgebra.Multilinear.Basic`	-3.141⬝10⁹	(-2.63%)
`Mathlib.Data.Nat.Defs`	-3.147⬝10⁹	(-8.06%)
`Mathlib.LinearAlgebra.AffineSpace.AffineSubspace`	-3.148⬝10⁹	(-2.48%)
`Mathlib.Topology.ContinuousMap.Bounded.Basic`	-3.151⬝10⁹	(-3.23%)
`Mathlib.Data.ZMod.Basic`	-3.233⬝10⁹	(-5.59%)
`Mathlib.MeasureTheory.Measure.Typeclasses`	-3.254⬝10⁹	(-6.01%)
`Mathlib.MeasureTheory.MeasurableSpace.Basic`	-3.287⬝10⁹	(-9.37%)
`Mathlib.Order.Filter.AtTopBot`	-3.292⬝10⁹	(-8.36%)
`Mathlib.Algebra.Quaternion`	-3.311⬝10⁹	(-1.84%)
`Mathlib.Data.Num.Lemmas`	-3.315⬝10⁹	(-2.39%)
`Mathlib.LinearAlgebra.TensorProduct.Basic`	-3.322⬝10⁹	(-1.61%)
`Mathlib.Data.Set.Image`	-3.322⬝10⁹	(-10.84%)
`Mathlib.Algebra.MvPolynomial.Basic`	-3.322⬝10⁹	(-3.37%)
`Mathlib.MeasureTheory.Integral.SetToL1`	-3.358⬝10⁹	(-1.08%)
`Mathlib.Topology.ContinuousOn`	-3.361⬝10⁹	(-9.15%)
`Mathlib.Computability.Primrec`	-3.377⬝10⁹	(-6.85%)
`Mathlib.MeasureTheory.Integral.SetIntegral`	-3.390⬝10⁹	(-2.65%)
`Mathlib.Data.Finsupp.Basic`	-3.407⬝10⁹	(-5.20%)
`Mathlib.FieldTheory.Adjoin`	-3.408⬝10⁹	(-1.15%)
`Mathlib.Topology.Algebra.Group.Basic`	-3.423⬝10⁹	(-3.88%)
`Mathlib.Algebra.Group.Pointwise.Set.Basic`	-3.447⬝10⁹	(-7.46%)
`Mathlib.Topology.Instances.ENNReal`	-3.467⬝10⁹	(-4.46%)
`Mathlib.LinearAlgebra.Dual`	-3.485⬝10⁹	(-0.79%)
`Mathlib.SetTheory.ZFC.Basic`	-3.521⬝10⁹	(-10.48%)
`Mathlib.Data.Ordmap.Ordset`	-3.552⬝10⁹	(-5.25%)
`Mathlib.Data.Fin.Basic`	-3.591⬝10⁹	(-10.04%)
`Mathlib.Logic.Equiv.Basic`	-3.635⬝10⁹	(-9.45%)
`Mathlib.Algebra.Order.Floor`	-3.637⬝10⁹	(-2.89%)
`Mathlib.Data.Real.EReal`	-3.665⬝10⁹	(-5.48%)
`Mathlib.Topology.UniformSpace.Basic`	-3.665⬝10⁹	(-7.85%)
`Mathlib.Data.Complex.Exponential`	-3.667⬝10⁹	(-2.62%)
`Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic`	-3.672⬝10⁹	(-4.96%)
`Mathlib.Topology.Basic`	-3.681⬝10⁹	(-10.25%)
`Mathlib.Order.Hom.Lattice`	-3.727⬝10⁹	(-7.61%)
`Mathlib.Order.Interval.Set.Basic`	-3.813⬝10⁹	(-7.42%)
`Mathlib.CategoryTheory.Limits.Shapes.Biproducts`	-3.814⬝10⁹	(-1.30%)
`Mathlib.MeasureTheory.Integral.Bochner`	-3.874⬝10⁹	(-2.11%)
`Mathlib.SetTheory.Game.PGame`	-3.892⬝10⁹	(-7.24%)
`Mathlib.Analysis.Calculus.ContDiff.Basic`	-3.969⬝10⁹	(-1.03%)
`Mathlib.MeasureTheory.Function.LpSpace`	-3.976⬝10⁹	(-1.82%)

15 files, Instructions -5.0⬝10⁹

File	Instructions	%
`Mathlib.MeasureTheory.Measure.MeasureSpace`	-4.132⬝10⁹	(-4.45%)
`Mathlib.Order.LiminfLimsup`	-4.160⬝10⁹	(-6.84%)
`Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian`	-4.209⬝10⁹	(-1.88%)
`Mathlib.Algebra.Group.Pointwise.Finset.Basic`	-4.263⬝10⁹	(-4.59%)
`Mathlib.Order.UpperLower.Basic`	-4.277⬝10⁹	(-4.82%)
`Mathlib.Topology.Constructions`	-4.318⬝10⁹	(-9.36%)
`Mathlib.Data.Set.Function`	-4.349⬝10⁹	(-9.53%)
`Mathlib.AlgebraicGeometry.EllipticCurve.Projective`	-4.386⬝10⁹	(-1.46%)
`Mathlib.Algebra.Order.GroupWithZero.Unbundled`	-4.474⬝10⁹	(-7.35%)
`Mathlib.MeasureTheory.Integral.Lebesgue`	-4.519⬝10⁹	(-4.23%)
`Mathlib.Order.CompleteLattice`	-4.592⬝10⁹	(-9.06%)
`Mathlib.Computability.TuringMachine`	-4.768⬝10⁹	(-5.72%)
`Mathlib.SetTheory.Cardinal.Basic`	-4.770⬝10⁹	(-7.08%)
`Mathlib.Algebra.BigOperators.Group.Finset`	-4.859⬝10⁹	(-5.42%)
`Mathlib.Analysis.Asymptotics.Asymptotics`	-4.895⬝10⁹	(-4.02%)

8 files, Instructions -6.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.InnerProductSpace.Basic`	-5.8⬝10⁹	(-1.64%)
`Mathlib.Data.Set.Lattice`	-5.38⬝10⁹	(-6.51%)
`Mathlib.Order.Filter.Basic`	-5.182⬝10⁹	(-10.32%)
`Mathlib.Topology.Algebra.Module.Basic`	-5.200⬝10⁹	(-2.14%)
`Mathlib.Data.List.Basic`	-5.254⬝10⁹	(-9.20%)
`Mathlib.Data.Set.Basic`	-5.294⬝10⁹	(-9.03%)
`Mathlib.Topology.Separation.Basic`	-5.354⬝10⁹	(-9.18%)
`Mathlib.SetTheory.Ordinal.Arithmetic`	-5.577⬝10⁹	(-6.59%)

File	Instructions	%
`Mathlib.Data.Multiset.Basic`	-6.502⬝10⁹	(-8.97%)

perf: TRY disabling ALL syntax style linters, see what the effect is

3a4fded

grunweg added WIP Work in progress t-linter Linter awaiting-bench labels Nov 27, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

perf: TRY disabling ALL syntax style linters, see what the effect is #19551

perf: TRY disabling ALL syntax style linters, see what the effect is #19551

grunweg commented Nov 27, 2024

github-actions bot commented Nov 27, 2024

grunweg commented Nov 27, 2024

grunweg commented Nov 27, 2024

leanprover-bot commented Nov 27, 2024

adomani commented Nov 28, 2024

perf: TRY disabling ALL syntax style linters, see what the effect is #19551

Are you sure you want to change the base?

perf: TRY disabling ALL syntax style linters, see what the effect is #19551

Conversation

grunweg commented Nov 27, 2024

github-actions bot commented Nov 27, 2024

PR summary 3a4fded931

Import changes for modified files

Declarations diff

grunweg commented Nov 27, 2024

grunweg commented Nov 27, 2024

leanprover-bot commented Nov 27, 2024

adomani commented Nov 28, 2024