chore: run `lake shake` iteratively and fix problems by MichaelStollBayreuth · Pull Request #39481 · leanprover-community/mathlib4

MichaelStollBayreuth · 2026-05-16T21:31:10Z

This adds -- shake: keep-all to all modules under Mathlib.Lean, Mathlib.Tactic and Mathlib.Util.
Then it goes through the remaining modules in topological order (according to the list in MS_test/topsort3.txt) and for each of them, runs lake shake --force <name> --only <name> --fix, followed by lake build <name>. If there is no error, the changes are commited. Otherwise, the problems are fixed manually; then the changes are committed.

This has been done for the first ~400 modules in the list. 38 of them required manual fixes; they are listed in MS_test/after_shake_fixes.txt.

We note that the import stats bot claims that the number of imports actually increases in most files, which somehow runs counter expectations...

Discussion: #mathlib4 > shake without --add-public @ 💬

github-actions · 2026-05-16T21:32:26Z

PR summary b28b8b58c3

Import changes exceeding 2%

%	File
+3.65%	`Mathlib.Algebra.BigOperators.Group.List.Basic`
+3.33%	`Mathlib.Algebra.CharZero.Defs`
+2.79%	`Mathlib.Algebra.ContinuedFractions.Basic`
+4.58%	`Mathlib.Algebra.Divisibility.Basic`
+4.48%	`Mathlib.Algebra.Divisibility.Hom`
+3.32%	`Mathlib.Algebra.Divisibility.Prod`
+4.83%	`Mathlib.Algebra.Divisibility.Units`
+3.80%	`Mathlib.Algebra.EuclideanDomain.Field`
+3.57%	`Mathlib.Algebra.Expr`
+3.03%	`Mathlib.Algebra.Field.Defs`
+3.75%	`Mathlib.Algebra.Field.IsField`
+3.47%	`Mathlib.Algebra.Free`
+3.34%	`Mathlib.Algebra.FreeMonoid.Basic`
+3.30%	`Mathlib.Algebra.FreeMonoid.Count`
+2.10%	`Mathlib.Algebra.Group.Action.Pretransitive`
+4.59%	`Mathlib.Algebra.Group.Basic`
+4.42%	`Mathlib.Algebra.Group.Commute.Basic`
+4.96%	`Mathlib.Algebra.Group.Commute.Units`
+5.19%	`Mathlib.Algebra.Group.Defs`
+3.14%	`Mathlib.Algebra.Group.Equiv.Basic`
+2.08%	`Mathlib.Algebra.Group.Equiv.TypeTags`
+2.70%	`Mathlib.Algebra.Group.Ext`
+4.27%	`Mathlib.Algebra.Group.Hom.Basic`
+2.73%	`Mathlib.Algebra.Group.Hom.Defs`
+3.79%	`Mathlib.Algebra.Group.Hom.End`
+4.03%	`Mathlib.Algebra.Group.Hom.Instances`
+3.25%	`Mathlib.Algebra.Group.Idempotent`
+2.97%	`Mathlib.Algebra.Group.InjSurj`
+4.92%	`Mathlib.Algebra.Group.Int.Units`
+3.47%	`Mathlib.Algebra.Group.Invertible.Basic`
+5.13%	`Mathlib.Algebra.Group.Invertible.Defs`
+3.12%	`Mathlib.Algebra.Group.Irreducible.Defs`
+6.56%	`Mathlib.Algebra.Group.ModEq`
+2.82%	`Mathlib.Algebra.Group.Nat.Hom`
+2.14%	`Mathlib.Algebra.Group.Opposite`
+2.80%	`Mathlib.Algebra.Group.Pi.Basic`
+3.70%	`Mathlib.Algebra.Group.Prod`
+4.50%	`Mathlib.Algebra.Group.Semiconj.Basic`
+4.60%	`Mathlib.Algebra.Group.Semiconj.Defs`
+5.00%	`Mathlib.Algebra.Group.Semiconj.Units`
+4.55%	`Mathlib.Algebra.Group.Torsion`
+2.96%	`Mathlib.Algebra.Group.TypeTags.Basic`
+5.04%	`Mathlib.Algebra.Group.Units.Basic`
+4.49%	`Mathlib.Algebra.Group.Units.Defs`
+3.50%	`Mathlib.Algebra.Group.Units.Hom`
+2.74%	`Mathlib.Algebra.Group.WithOne.Basic`
+3.28%	`Mathlib.Algebra.Group.WithOne.Defs`
+4.20%	`Mathlib.Algebra.GroupWithZero.Basic`
+6.90%	`Mathlib.Algebra.GroupWithZero.Commute`
+3.45%	`Mathlib.Algebra.GroupWithZero.Defs`
+2.80%	`Mathlib.Algebra.GroupWithZero.Divisibility`
+4.00%	`Mathlib.Algebra.GroupWithZero.Hom`
+3.17%	`Mathlib.Algebra.GroupWithZero.Idempotent`
+2.80%	`Mathlib.Algebra.GroupWithZero.InjSurj`
+5.39%	`Mathlib.Algebra.GroupWithZero.Invertible`
+2.08%	`Mathlib.Algebra.GroupWithZero.NeZero`
+2.04%	`Mathlib.Algebra.GroupWithZero.Opposite`
+2.77%	`Mathlib.Algebra.GroupWithZero.Prod`
+3.26%	`Mathlib.Algebra.GroupWithZero.Regular`
+6.99%	`Mathlib.Algebra.GroupWithZero.Semiconj`
+7.09%	`Mathlib.Algebra.GroupWithZero.Units.Basic`
+2.84%	`Mathlib.Algebra.GroupWithZero.WithZero`
+3.64%	`Mathlib.Algebra.HierarchyDesign`
+2.88%	`Mathlib.Algebra.Homology.ComplexShape`
+4.76%	`Mathlib.Algebra.Homology.Embedding.Basic`
+3.12%	`Mathlib.Algebra.Notation`
+3.03%	`Mathlib.Algebra.Notation.Defs`
+3.03%	`Mathlib.Algebra.Notation.Lemmas`
+2.17%	`Mathlib.Algebra.Notation.Pi.Basic`
+2.78%	`Mathlib.Algebra.Notation.Pi.Defs`
+2.01%	`Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs`
+2.13%	`Mathlib.Algebra.Order.Monoid.Unbundled.Defs`
+2.78%	`Mathlib.Algebra.Prime.Defs`
+3.60%	`Mathlib.Algebra.Quotient`
+4.42%	`Mathlib.Algebra.Regular.Basic`
+3.11%	`Mathlib.Algebra.Ring.Basic`
+3.12%	`Mathlib.Algebra.Ring.Defs`
+2.50%	`Mathlib.Algebra.Ring.Ext`
+3.91%	`Mathlib.Algebra.Ring.GrindInstances`
+3.03%	`Mathlib.Algebra.Ring.Hom.Defs`
+3.73%	`Mathlib.Algebra.Ring.Hom.InjSurj`
+4.26%	`Mathlib.Algebra.Ring.Idempotent`
+5.07%	`Mathlib.Algebra.Ring.Int.Defs`
+5.20%	`Mathlib.Algebra.Ring.Invertible`
+4.20%	`Mathlib.Algebra.Ring.MinimalAxioms`
+3.42%	`Mathlib.Algebra.Ring.Nat`
+3.65%	`Mathlib.Algebra.Ring.Rat`
+4.07%	`Mathlib.Algebra.Ring.Regular`
+3.26%	`Mathlib.Algebra.Ring.Units`
+2.80%	`Mathlib.Algebra.Ring.WithZero`
+3.64%	`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Note`
+4.06%	`Mathlib.CategoryTheory.Category.Basic`
+3.64%	`Mathlib.CategoryTheory.Category.Init`
+3.70%	`Mathlib.CategoryTheory.ConcreteCategory.Bundled`
+3.97%	`Mathlib.CategoryTheory.ConcreteCategory.BundledHom`
+3.97%	`Mathlib.CategoryTheory.ConcreteCategory.UnbundledHom`
+3.64%	`Mathlib.Combinatorics.Matroid.Init`
+3.64%	`Mathlib.Combinatorics.SimpleGraph.Init`
+5.00%	`Mathlib.Control.Basic`
+3.98%	`Mathlib.Control.Bifunctor`
+4.26%	`Mathlib.Control.Bitraversable.Basic`
+4.09%	`Mathlib.Control.Bitraversable.Instances`
+4.25%	`Mathlib.Control.Bitraversable.Lemmas`
+3.70%	`Mathlib.Control.Combinators`
+4.13%	`Mathlib.Control.EquivFunctor`
+3.70%	`Mathlib.Control.Lawful`
+2.21%	`Mathlib.Control.Traversable.Equiv`
+5.26%	`Mathlib.Control.Traversable.Lemmas`
+3.70%	`Mathlib.Control.ULift`
+3.06%	`Mathlib.Control.ULiftable`
+3.57%	`Mathlib.Data.Array.Defs`
+3.64%	`Mathlib.Data.Array.Extract`
+3.70%	`Mathlib.Data.Bool.AllAny`
+3.70%	`Mathlib.Data.Bracket`
+3.03%	`Mathlib.Data.Char`
+5.45%	`Mathlib.Data.Finset.Attr`
+2.13%	`Mathlib.Data.FunLike.Basic`
+2.11%	`Mathlib.Data.FunLike.Embedding`
+2.08%	`Mathlib.Data.FunLike.Equiv`
+3.48%	`Mathlib.Data.Int.Basic`
+4.10%	`Mathlib.Data.Int.Cast.Basic`
+4.93%	`Mathlib.Data.Int.Cast.Field`
+3.51%	`Mathlib.Data.Int.Cast.Pi`
+2.99%	`Mathlib.Data.Int.GCD`
+3.39%	`Mathlib.Data.Int.Init`
+3.70%	`Mathlib.Data.Int.Notation`
+3.86%	`Mathlib.Data.Int.Sqrt`
+3.01%	`Mathlib.Data.List.Basic`
+2.70%	`Mathlib.Data.List.Chain`
+4.33%	`Mathlib.Data.List.ChainOfFn`
+3.97%	`Mathlib.Data.List.Count`
+3.68%	`Mathlib.Data.List.Dedup`
+2.53%	`Mathlib.Data.List.Defs`
+3.70%	`Mathlib.Data.List.Duplicate`
+3.00%	`Mathlib.Data.List.Enum`
+2.60%	`Mathlib.Data.List.Flatten`
+3.57%	`Mathlib.Data.List.Fold`
+2.35%	`Mathlib.Data.List.GetD`
+3.97%	`Mathlib.Data.List.Induction`
+2.85%	`Mathlib.Data.List.Infix`
+4.37%	`Mathlib.Data.List.InsertIdx`
+3.59%	`Mathlib.Data.List.InsertNth`
+3.00%	`Mathlib.Data.List.Lattice`
+2.75%	`Mathlib.Data.List.Lex`
+3.51%	`Mathlib.Data.List.Lookmap`
+3.91%	`Mathlib.Data.List.Map2`
+3.64%	`Mathlib.Data.List.Monad`
+3.70%	`Mathlib.Data.List.NatAntidiagonal`
+3.72%	`Mathlib.Data.List.Nodup`
+3.99%	`Mathlib.Data.List.OffDiag`
+4.17%	`Mathlib.Data.List.Pairwise`
+4.35%	`Mathlib.Data.List.Palindrome`
+3.65%	`Mathlib.Data.List.Perm.Lattice`
+3.30%	`Mathlib.Data.List.Perm.Subperm`
+4.28%	`Mathlib.Data.List.ProdSigma`
+3.00%	`Mathlib.Data.List.ReduceOption`
+3.44%	`Mathlib.Data.List.Rotate`
+3.88%	`Mathlib.Data.List.TakeDrop`
+2.52%	`Mathlib.Data.List.TakeWhile`
+2850.00%	`Mathlib.Data.List.Triplewise`
+3.26%	`Mathlib.Data.List.Zip`
+3.89%	`Mathlib.Data.Matrix.Auto`
+3.06%	`Mathlib.Data.Nat.Basic`
+3.70%	`Mathlib.Data.Nat.BinaryRec`
+2.47%	`Mathlib.Data.Nat.Bits`
+4.88%	`Mathlib.Data.Nat.Cast.Defs`
+2.92%	`Mathlib.Data.Nat.Choose.Basic`
+3.88%	`Mathlib.Data.Nat.Factorial.Basic`
+4.48%	`Mathlib.Data.Nat.GCD.Basic`
+3.45%	`Mathlib.Data.Nat.Init`
+2.92%	`Mathlib.Data.Nat.Log`
+3.12%	`Mathlib.Data.Nat.MaxPowDiv`
+3.70%	`Mathlib.Data.Nat.Notation`
+3.70%	`Mathlib.Data.Nat.NthRoot.Defs`
+4.13%	`Mathlib.Data.Nat.PSub`
+2.44%	`Mathlib.Data.Nat.Size`
+3.00%	`Mathlib.Data.Nat.Sqrt`
+3.51%	`Mathlib.Data.Num.Basic`
+2.11%	`Mathlib.Data.Option.Basic`
+3.70%	`Mathlib.Data.Option.Defs`
+3.70%	`Mathlib.Data.Option.NAry`
+3.70%	`Mathlib.Data.Ordering.Basic`
+3.85%	`Mathlib.Data.Ordmap.Ordnode`
+3.64%	`Mathlib.Data.Prod.PProd`
+3.33%	`Mathlib.Data.Rat.Defs`
+3.57%	`Mathlib.Data.Rat.Init`
+3.57%	`Mathlib.Data.SProd`
+3.44%	`Mathlib.Data.Seq.Computation`
+2.95%	`Mathlib.Data.Seq.Defs`
+2.94%	`Mathlib.Data.Set.Defs`
+2.30%	`Mathlib.Data.Sigma.Basic`
+2.63%	`Mathlib.Data.Sigma.Lex`
+3.88%	`Mathlib.Data.Stream.Init`
+3.70%	`Mathlib.Data.String.Defs`
+3.57%	`Mathlib.Data.String.Lemmas`
+3.41%	`Mathlib.Data.Sum.Basic`
+3.64%	`Mathlib.Data.Sym.Sym2.Init`
+3.57%	`Mathlib.Data.Tree.Basic`
+3.28%	`Mathlib.Data.Tree.Get`
+5.15%	`Mathlib.Data.Tree.Traversable`
+6.35%	`Mathlib.Data.TwoPointing`
+3.50%	`Mathlib.Data.ULift`
+3.91%	`Mathlib.Data.Vector.Defs`
+3.70%	`Mathlib.Deprecated.Aliases`
+3.70%	`Mathlib.Lean.CoreM`
+3.39%	`Mathlib.Lean.Elab.Tactic.Basic`
+3.64%	`Mathlib.Lean.Elab.Term`
+3.64%	`Mathlib.Lean.EnvExtension`
+3.70%	`Mathlib.Lean.Exception`
+2.86%	`Mathlib.Lean.Expr.ExtraRecognizers`
+3.64%	`Mathlib.Lean.Expr.Rat`
+3.64%	`Mathlib.Lean.FoldEnvironment`
+3.57%	`Mathlib.Lean.GoalsLocation`
+3.70%	`Mathlib.Lean.Json`
+3.57%	`Mathlib.Lean.LocalContext`
+3.64%	`Mathlib.Lean.MessageData.ForExprs`
+3.64%	`Mathlib.Lean.MessageData.Trace`
+3.45%	`Mathlib.Lean.Meta`
+3.57%	`Mathlib.Lean.Meta.Basic`
+8.93%	`Mathlib.Lean.Meta.CongrTheorems`
+3.70%	`Mathlib.Lean.Meta.DiscrTree`
+3.51%	`Mathlib.Lean.Meta.KAbstractPositions`
+3.17%	`Mathlib.Lean.Meta.RefinedDiscrTree`
+3.70%	`Mathlib.Lean.Meta.RefinedDiscrTree.Basic`
+3.39%	`Mathlib.Lean.Meta.RefinedDiscrTree.Encode`
+3.57%	`Mathlib.Lean.Meta.RefinedDiscrTree.Initialize`
+3.33%	`Mathlib.Lean.Meta.RefinedDiscrTree.Lookup`
+3.57%	`Mathlib.Lean.Meta.Simp`
+3.64%	`Mathlib.Lean.Meta.Tactic.Rewrite`
+3.57%	`Mathlib.Lean.Name`
+3.64%	`Mathlib.Lean.PrettyPrinter.Delaborator`
+3.70%	`Mathlib.Lean.Thunk`
+3.23%	`Mathlib.Logic.Basic`
+3.40%	`Mathlib.Logic.Embedding.Basic`
+3.55%	`Mathlib.Logic.Equiv.Basic`
+3.52%	`Mathlib.Logic.Equiv.Bool`
+3.91%	`Mathlib.Logic.Equiv.Option`
+3.70%	`Mathlib.Logic.ExistsUnique`
+2.33%	`Mathlib.Logic.Function.Basic`
+3.70%	`Mathlib.Logic.Function.Coequalizer`
+3.70%	`Mathlib.Logic.Function.CompTypeclasses`
+2.30%	`Mathlib.Logic.Function.Conjugate`
+3.51%	`Mathlib.Logic.Function.Defs`
+2.25%	`Mathlib.Logic.Function.Iterate`
+3.70%	`Mathlib.Logic.Function.ULift`
+2.25%	`Mathlib.Logic.IsEmpty.Basic`
+3.70%	`Mathlib.Logic.IsEmpty.Defs`
+8.11%	`Mathlib.Logic.Lemmas`
+3.70%	`Mathlib.Logic.Nonempty`
+3.57%	`Mathlib.Logic.Nontrivial.Defs`
+3.70%	`Mathlib.Logic.OpClass`
+2.27%	`Mathlib.Logic.Pairwise`
+3.75%	`Mathlib.Logic.Relation`
+3.45%	`Mathlib.Logic.Relator`
+2.25%	`Mathlib.Logic.Unique`
+2.63%	`Mathlib.Order.Basic`
+2.74%	`Mathlib.Order.BoundedOrder.Basic`
+2.37%	`Mathlib.Order.BoundedOrder.Monotone`
+2.90%	`Mathlib.Order.Bounds.Defs`
+2.96%	`Mathlib.Order.Compare`
+5.13%	`Mathlib.Order.Defs.LinearOrder`
+2.82%	`Mathlib.Order.Defs.Unbundled`
+2.38%	`Mathlib.Order.Lattice`
+2.96%	`Mathlib.Order.Max`
+2.45%	`Mathlib.Order.Monotone.Basic`
+2.38%	`Mathlib.Order.Monotone.Defs`
+2.99%	`Mathlib.Order.OrderDual`
+2.94%	`Mathlib.Order.RelClasses`
+2.08%	`Mathlib.Tactic.Abel`
+3.70%	`Mathlib.Tactic.ApplyAt`
+3.70%	`Mathlib.Tactic.ApplyCongr`
+3.64%	`Mathlib.Tactic.ApplyWith`
+3.57%	`Mathlib.Tactic.ArithMult`
+3.64%	`Mathlib.Tactic.ArithMult.Init`
+5.26%	`Mathlib.Tactic.Attr.Core`
+3.57%	`Mathlib.Tactic.Attr.Register`
+3.45%	`Mathlib.Tactic.Bound.Attribute`
+3.64%	`Mathlib.Tactic.Bound.Init`
+2.90%	`Mathlib.Tactic.ByCases`
+2.90%	`Mathlib.Tactic.ByContra`
+2.47%	`Mathlib.Tactic.CancelDenoms.Core`
+3.64%	`Mathlib.Tactic.Cases`
+3.70%	`Mathlib.Tactic.CasesM`
+3.91%	`Mathlib.Tactic.CategoryTheory.BicategoricalComp`
+3.81%	`Mathlib.Tactic.CategoryTheory.Bicategory.Basic`
+3.89%	`Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes`
+3.86%	`Mathlib.Tactic.CategoryTheory.Bicategory.Normalize`
+3.86%	`Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence`
+3.97%	`Mathlib.Tactic.CategoryTheory.CancelIso`
+3.70%	`Mathlib.Tactic.CategoryTheory.CategoryStar`
+4.04%	`Mathlib.Tactic.CategoryTheory.CheckCompositions`
+4.00%	`Mathlib.Tactic.CategoryTheory.Coherence.Basic`
+3.70%	`Mathlib.Tactic.CategoryTheory.Coherence.Datatypes`
+3.64%	`Mathlib.Tactic.CategoryTheory.Coherence.Normalize`
+3.64%	`Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence`
+3.77%	`Mathlib.Tactic.CategoryTheory.Elementwise`
+3.97%	`Mathlib.Tactic.CategoryTheory.IsoReassoc`
+3.48%	`Mathlib.Tactic.CategoryTheory.Monoidal.Basic`
+3.55%	`Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes`
+3.53%	`Mathlib.Tactic.CategoryTheory.Monoidal.Normalize`
+3.53%	`Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence`
+3.57%	`Mathlib.Tactic.CategoryTheory.MonoidalComp`
+4.00%	`Mathlib.Tactic.CategoryTheory.Reassoc`
+3.70%	`Mathlib.Tactic.Change`
+3.70%	`Mathlib.Tactic.Check`
+2.30%	`Mathlib.Tactic.Choose`
+3.70%	`Mathlib.Tactic.Clean`
+3.70%	`Mathlib.Tactic.ClearExcept`
+3.70%	`Mathlib.Tactic.ClearExclamation`
+3.70%	`Mathlib.Tactic.Clear_`
+3.70%	`Mathlib.Tactic.Coe`
+24.56%	`Mathlib.Tactic.CongrExclamation`
+8.62%	`Mathlib.Tactic.CongrM`
+3.70%	`Mathlib.Tactic.Constructor`
+3.57%	`Mathlib.Tactic.Continuity`
+3.64%	`Mathlib.Tactic.Continuity.Init`
+4.00%	`Mathlib.Tactic.ContinuousFunctionalCalculus`
+2.94%	`Mathlib.Tactic.Contrapose`
+3.70%	`Mathlib.Tactic.Conv`
+23.73%	`Mathlib.Tactic.Convert`
+3.70%	`Mathlib.Tactic.Core`
+3.70%	`Mathlib.Tactic.CrossRefAttribute`
+5.56%	`Mathlib.Tactic.DSimpPercent`
+3.70%	`Mathlib.Tactic.DefEqAbuse`
+3.70%	`Mathlib.Tactic.DefEqTransformations`
+3.64%	`Mathlib.Tactic.DepRewrite`
+3.64%	`Mathlib.Tactic.DeprecateTo`
+2.63%	`Mathlib.Tactic.DeriveCountable`
+5.21%	`Mathlib.Tactic.DeriveTraversable`
+3.70%	`Mathlib.Tactic.Eqns`
+3.70%	`Mathlib.Tactic.ErwQuestion`
+3.64%	`Mathlib.Tactic.Eval`
+3.70%	`Mathlib.Tactic.ExistsI`
+3.57%	`Mathlib.Tactic.Explode`
+3.70%	`Mathlib.Tactic.Explode.Datatypes`
+3.64%	`Mathlib.Tactic.Explode.Pretty`
+3.64%	`Mathlib.Tactic.Ext`
+3.70%	`Mathlib.Tactic.ExtendDoc`
+3.64%	`Mathlib.Tactic.FBinop`
+3.70%	`Mathlib.Tactic.FailIfNoProgress`
+3.70%	`Mathlib.Tactic.FastInstance`
+3.70%	`Mathlib.Tactic.FieldSimp.Attr`
+2.68%	`Mathlib.Tactic.FinCases`
+3.64%	`Mathlib.Tactic.Find`
+3.70%	`Mathlib.Tactic.FindSyntax`
+3.64%	`Mathlib.Tactic.Finiteness.Attr`
+4.11%	`Mathlib.Tactic.FunProp`
+4.41%	`Mathlib.Tactic.FunProp.Attr`
+4.29%	`Mathlib.Tactic.FunProp.Core`
+3.70%	`Mathlib.Tactic.FunProp.Decl`
+4.23%	`Mathlib.Tactic.FunProp.Elab`
+3.51%	`Mathlib.Tactic.FunProp.FunctionData`
+3.64%	`Mathlib.Tactic.FunProp.Mor`
+4.48%	`Mathlib.Tactic.FunProp.Theorems`
+3.70%	`Mathlib.Tactic.FunProp.ToBatteries`
+6.90%	`Mathlib.Tactic.FunProp.Types`
+2.38%	`Mathlib.Tactic.GCongr`
+2.63%	`Mathlib.Tactic.GCongr.Core`
+2.60%	`Mathlib.Tactic.GCongr.CoreAttrs`
+3.70%	`Mathlib.Tactic.GCongr.ForwardAttr`
+5.06%	`Mathlib.Tactic.GRewrite`
+3.90%	`Mathlib.Tactic.GRewrite.Core`
+5.13%	`Mathlib.Tactic.GRewrite.Elab`
+3.70%	`Mathlib.Tactic.Generalize`
+3.70%	`Mathlib.Tactic.GuardGoalNums`
+3.70%	`Mathlib.Tactic.GuardHypNums`
+3.70%	`Mathlib.Tactic.Have`
+3.70%	`Mathlib.Tactic.HaveI`
+3.64%	`Mathlib.Tactic.HigherOrder`
+3.33%	`Mathlib.Tactic.Hint`
+3.33%	`Mathlib.Tactic.ITauto`
+3.70%	`Mathlib.Tactic.InferParam`
+3.70%	`Mathlib.Tactic.Inhabit`
+3.57%	`Mathlib.Tactic.IrreducibleDef`
+3.70%	`Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes`
+3.64%	`Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss`
+3.51%	`Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector`
+3.64%	`Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm`
+3.28%	`Mathlib.Tactic.Linter`
+3.64%	`Mathlib.Tactic.Linter.DeprecatedModule`
+3.64%	`Mathlib.Tactic.Linter.FindDeprecations`
+3.70%	`Mathlib.Tactic.Linter.HaveLetLinter`
+3.70%	`Mathlib.Tactic.Linter.PPRoundtrip`
+33.33%	`Mathlib.Tactic.Linter.Style`
+3.51%	`Mathlib.Tactic.Linter.TextBased`
+3.70%	`Mathlib.Tactic.Linter.TextBased.UnicodeLinter`
+3.64%	`Mathlib.Tactic.Linter.UpstreamableDecl`
+3.64%	`Mathlib.Tactic.Linter.ValidatePRTitle`
+3.51%	`Mathlib.Tactic.Measurability`
+3.64%	`Mathlib.Tactic.Measurability.Init`
+2.12%	`Mathlib.Tactic.ModCases`
+3.70%	`Mathlib.Tactic.Monotonicity.Attr`
+3.64%	`Mathlib.Tactic.Monotonicity.Basic`
+4.39%	`Mathlib.Tactic.MoveAdd`
+2.07%	`Mathlib.Tactic.NoncommRing`
+66.67%	`Mathlib.Tactic.Nontriviality`
+100.00%	`Mathlib.Tactic.Nontriviality.Core`
+2.10%	`Mathlib.Tactic.NormNum.Basic`
+2.09%	`Mathlib.Tactic.NormNum.BigOperators`
+4.02%	`Mathlib.Tactic.NormNum.Core`
+3.98%	`Mathlib.Tactic.NormNum.Parity`
+2.06%	`Mathlib.Tactic.NormNum.Pow`
+2.05%	`Mathlib.Tactic.NormNum.PowMod`
+4.74%	`Mathlib.Tactic.NormNum.Result`
+3.70%	`Mathlib.Tactic.NthRewrite`
+3.70%	`Mathlib.Tactic.Observe`
+3.70%	`Mathlib.Tactic.OfNat`
+2.38%	`Mathlib.Tactic.Order`
+3.39%	`Mathlib.Tactic.Order.CollectFacts`
+3.33%	`Mathlib.Tactic.Order.Graph.Basic`
+3.28%	`Mathlib.Tactic.Order.Graph.Tarjan`
+3.33%	`Mathlib.Tactic.Order.Preprocessing`
+3.17%	`Mathlib.Tactic.Order.ToInt`
+3.70%	`Mathlib.Tactic.PPWithUniv`
+2.60%	`Mathlib.Tactic.Peel`
+3.70%	`Mathlib.Tactic.Polyrith`
+2.08%	`Mathlib.Tactic.Positivity.Finset`
+2.99%	`Mathlib.Tactic.Push`
+3.64%	`Mathlib.Tactic.Push.Attr`
+3.70%	`Mathlib.Tactic.RSuffices`
+3.70%	`Mathlib.Tactic.Recall`
+3.70%	`Mathlib.Tactic.Recover`
+2.03%	`Mathlib.Tactic.ReduceModChar`
+3.70%	`Mathlib.Tactic.ReduceModChar.Ext`
+3.70%	`Mathlib.Tactic.Relation.Rfl`
+3.70%	`Mathlib.Tactic.Relation.Symm`
+3.70%	`Mathlib.Tactic.Rename`
+3.64%	`Mathlib.Tactic.RenameBVar`
+3.64%	`Mathlib.Tactic.Replace`
+3.70%	`Mathlib.Tactic.RewriteSearch`
+3.33%	`Mathlib.Tactic.Sat.FromLRAT`
+3.39%	`Mathlib.Tactic.Says`
+3.64%	`Mathlib.Tactic.ScopedNS`
+3.70%	`Mathlib.Tactic.Set`
+7.27%	`Mathlib.Tactic.SetLike`
+3.64%	`Mathlib.Tactic.SimpIntro`
+3.70%	`Mathlib.Tactic.SimpRw`
+3.51%	`Mathlib.Tactic.Simproc.Divisors`
+3.51%	`Mathlib.Tactic.Simproc.ExistsAndEq`
+7.02%	`Mathlib.Tactic.Simps.Basic`
+3.70%	`Mathlib.Tactic.Simps.NotationClass`
+3.64%	`Mathlib.Tactic.SplitIfs`
+3.70%	`Mathlib.Tactic.Spread`
+3.17%	`Mathlib.Tactic.Subsingleton`
+3.70%	`Mathlib.Tactic.Substs`
+3.70%	`Mathlib.Tactic.SuccessIfFailWithMsg`
+3.70%	`Mathlib.Tactic.SudoSetOption`
+3.70%	`Mathlib.Tactic.SuppressCompilation`
+3.70%	`Mathlib.Tactic.SwapVar`
+3.33%	`Mathlib.Tactic.TFAE`
+12.50%	`Mathlib.Tactic.TacticAnalysis.Declarations`
+5.26%	`Mathlib.Tactic.Tauto`
+8.77%	`Mathlib.Tactic.TermCongr`
+3.12%	`Mathlib.Tactic.ToAdditive`
+3.03%	`Mathlib.Tactic.ToDual`
+3.70%	`Mathlib.Tactic.ToExpr`
+2.86%	`Mathlib.Tactic.ToFun`
+3.64%	`Mathlib.Tactic.ToLevel`
+3.70%	`Mathlib.Tactic.Trace`
+3.70%	`Mathlib.Tactic.Translate.Attributes`
+3.23%	`Mathlib.Tactic.Translate.Core`
+3.70%	`Mathlib.Tactic.Translate.GuessName`
+3.70%	`Mathlib.Tactic.Translate.Reorder`
+3.17%	`Mathlib.Tactic.Translate.TagUnfoldBoundary`
+3.17%	`Mathlib.Tactic.Translate.ToAdditive`
+3.12%	`Mathlib.Tactic.Translate.ToDual`
+3.64%	`Mathlib.Tactic.Translate.UnfoldBoundary`
+3.70%	`Mathlib.Tactic.TryThis`
+3.70%	`Mathlib.Tactic.TypeCheck`
+3.70%	`Mathlib.Tactic.UnsetOption`
+3.70%	`Mathlib.Tactic.Use`
+3.70%	`Mathlib.Tactic.Variable`
+2.86%	`Mathlib.Tactic.WLOG`
+3.17%	`Mathlib.Tactic.Widget.Calc`
+4.01%	`Mathlib.Tactic.Widget.CommDiag`
+3.28%	`Mathlib.Tactic.Widget.CongrM`
+3.08%	`Mathlib.Tactic.Widget.Conv`
+3.28%	`Mathlib.Tactic.Widget.GCongr`
+3.17%	`Mathlib.Tactic.Widget.InteractiveUnfold`
+2.67%	`Mathlib.Tactic.Widget.LibraryRewrite`
+3.64%	`Mathlib.Tactic.Widget.SelectInsertParamsClass`
+3.45%	`Mathlib.Tactic.Widget.SelectPanelUtils`
+3.43%	`Mathlib.Tactic.Widget.StringDiagram`
+3.70%	`Mathlib.Tactic.WithoutCDot`
+4.41%	`Mathlib.Tactic.Zify`
+3.33%	`Mathlib.Testing.Plausible.Testable`
+2.80%	`Mathlib.Topology.ContinuousMap.Defs`
+3.64%	`Mathlib.Topology.Sheaves.Init`
+3.70%	`Mathlib.Util.AddRelatedDecl`
+3.57%	`Mathlib.Util.AliasIn`
+3.70%	`Mathlib.Util.AssertNoSorry`
+3.64%	`Mathlib.Util.AtLocation`
+3.57%	`Mathlib.Util.AtomM`
+3.51%	`Mathlib.Util.AtomM.Recurse`
+3.70%	`Mathlib.Util.CountHeartbeats`
+3.70%	`Mathlib.Util.DelabNonCanonical`
+3.64%	`Mathlib.Util.Delaborators`
+3.57%	`Mathlib.Util.DischargerAsTactic`
+3.70%	`Mathlib.Util.ElabWithoutMVars`
+3.70%	`Mathlib.Util.Export`
+3.70%	`Mathlib.Util.FormatTable`
+3.70%	`Mathlib.Util.GetAllModules`
+3.70%	`Mathlib.Util.LongNames`
+3.64%	`Mathlib.Util.MemoFix`
+3.28%	`Mathlib.Util.Notation3`
+3.70%	`Mathlib.Util.PPOptions`
+3.57%	`Mathlib.Util.Qq`
+3.64%	`Mathlib.Util.Simp`
+3.70%	`Mathlib.Util.SleepHeartbeats`
+3.70%	`Mathlib.Util.Superscript`
+3.57%	`Mathlib.Util.SynthesizeUsing`
+3.70%	`Mathlib.Util.Tactic`
+3.70%	`Mathlib.Util.TermReduce`
+3.70%	`Mathlib.Util.TransImports`
+3.70%	`Mathlib.Util.WhatsNew`
+3.70%	`Mathlib.Util.WithWeakNamespace`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.List.Triplewise	2	59	+57 (+2850.00%)
Mathlib.Tactic.Nontriviality.Core	2	4	+2 (+100.00%)
Mathlib.Tactic.Nontriviality	3	5	+2 (+66.67%)
Mathlib.Data.List.Forall2	268	101	-167 (-62.31%)
Mathlib.Data.List.Sections	269	102	-167 (-62.08%)
Mathlib.Order.Synonym	136	58	-78 (-57.35%)
Mathlib.Logic.IsEmpty	90	58	-32 (-35.56%)
Mathlib.Tactic.Linter.Style	3	4	+1 (+33.33%)
Mathlib.Tactic.CongrExclamation	57	71	+14 (+24.56%)
Mathlib.Tactic.Convert	59	73	+14 (+23.73%)
Mathlib.Tactic.TacticAnalysis.Declarations	8	9	+1 (+12.50%)
Mathlib.Order.Lex	134	118	-16 (-11.94%)
Mathlib.Data.Nat.Cast.Synonym	146	130	-16 (-10.96%)
Mathlib.Lean.Meta.CongrTheorems	56	61	+5 (+8.93%)
Mathlib.Tactic.TermCongr	57	62	+5 (+8.77%)
Mathlib.Tactic.CongrM	58	63	+5 (+8.62%)
Mathlib.Logic.Lemmas	74	80	+6 (+8.11%)
Mathlib.Tactic.SetLike	55	59	+4 (+7.27%)
Mathlib.Algebra.GroupWithZero.Units.Basic	141	151	+10 (+7.09%)
Mathlib.Tactic.Simps.Basic	57	61	+4 (+7.02%)
Mathlib.Algebra.GroupWithZero.Semiconj	143	153	+10 (+6.99%)
Mathlib.Algebra.GroupWithZero.Commute	145	155	+10 (+6.90%)
Mathlib.Tactic.FunProp.Types	58	62	+4 (+6.90%)
Mathlib.Algebra.Group.ModEq	122	130	+8 (+6.56%)
Mathlib.Data.TwoPointing	63	67	+4 (+6.35%)
Mathlib.Tactic.DSimpPercent	54	57	+3 (+5.56%)
Mathlib.Data.Finset.Attr	55	58	+3 (+5.45%)
Mathlib.Algebra.GroupWithZero.Invertible	167	176	+9 (+5.39%)
Mathlib.Control.Traversable.Lemmas	95	100	+5 (+5.26%)
Mathlib.Tactic.Attr.Core	57	60	+3 (+5.26%)
Mathlib.Tactic.Tauto	57	60	+3 (+5.26%)
Mathlib.Tactic.DeriveTraversable	96	101	+5 (+5.21%)
Mathlib.Algebra.Ring.Invertible	173	182	+9 (+5.20%)
Mathlib.Algebra.Group.Defs	77	81	+4 (+5.19%)
Mathlib.Data.Tree.Traversable	97	102	+5 (+5.15%)
Mathlib.Algebra.Group.Invertible.Defs	78	82	+4 (+5.13%)
Mathlib.Order.Defs.LinearOrder	78	82	+4 (+5.13%)
Mathlib.Tactic.GRewrite.Elab	78	82	+4 (+5.13%)
Mathlib.Algebra.Ring.Int.Defs	138	145	+7 (+5.07%)
Mathlib.Tactic.GRewrite	79	83	+4 (+5.06%)
Mathlib.Algebra.Group.Units.Basic	119	125	+6 (+5.04%)
Mathlib.Algebra.Group.Semiconj.Units	120	126	+6 (+5.00%)
Mathlib.Control.Basic	60	63	+3 (+5.00%)
Mathlib.Algebra.Group.Commute.Units	121	127	+6 (+4.96%)
Mathlib.Data.Int.Cast.Field	142	149	+7 (+4.93%)
Mathlib.Algebra.Group.Int.Units	122	128	+6 (+4.92%)
Mathlib.Data.Nat.Cast.Defs	82	86	+4 (+4.88%)
Mathlib.Algebra.Divisibility.Units	269	282	+13 (+4.83%)
Mathlib.Algebra.Homology.Embedding.Basic	147	154	+7 (+4.76%)
Mathlib.Tactic.NormNum.Result	190	199	+9 (+4.74%)
Mathlib.Algebra.Group.Semiconj.Defs	87	91	+4 (+4.60%)
Mathlib.Algebra.Group.Basic	109	114	+5 (+4.59%)
Mathlib.Algebra.Divisibility.Basic	262	274	+12 (+4.58%)
Mathlib.Algebra.Group.Torsion	110	115	+5 (+4.55%)
Mathlib.Algebra.Group.Semiconj.Basic	111	116	+5 (+4.50%)
Mathlib.Algebra.Group.Units.Defs	89	93	+4 (+4.49%)
Mathlib.Data.Nat.GCD.Basic	290	303	+13 (+4.48%)
Mathlib.Algebra.Divisibility.Hom	268	280	+12 (+4.48%)
Mathlib.Tactic.FunProp.Theorems	67	70	+3 (+4.48%)
Mathlib.Algebra.Group.Commute.Basic	113	118	+5 (+4.42%)
Mathlib.Algebra.Regular.Basic	113	118	+5 (+4.42%)
Mathlib.Tactic.FunProp.Attr	68	71	+3 (+4.41%)
Mathlib.Tactic.Zify	136	142	+6 (+4.41%)
Mathlib.Tactic.MoveAdd	114	119	+5 (+4.39%)
Mathlib.Data.List.InsertIdx	252	263	+11 (+4.37%)
Mathlib.Data.List.Palindrome	253	264	+11 (+4.35%)
Mathlib.Data.List.ChainOfFn	254	265	+11 (+4.33%)
Mathlib.Tactic.FunProp.Core	70	73	+3 (+4.29%)
Mathlib.Data.List.ProdSigma	257	268	+11 (+4.28%)
Mathlib.Algebra.Group.Hom.Basic	117	122	+5 (+4.27%)
Mathlib.Control.Bitraversable.Basic	258	269	+11 (+4.26%)
Mathlib.Algebra.Ring.Idempotent	141	147	+6 (+4.26%)
Mathlib.Control.Bitraversable.Lemmas	259	270	+11 (+4.25%)
Mathlib.Tactic.FunProp.Elab	71	74	+3 (+4.23%)
Mathlib.Data.Int.Order.Basic	95	91	-4 (-4.21%)
Mathlib.Algebra.GroupWithZero.Basic	119	124	+5 (+4.20%)
Mathlib.Algebra.Ring.MinimalAxioms	119	124	+5 (+4.20%)
Mathlib.Data.List.Pairwise	96	100	+4 (+4.17%)
Mathlib.Control.EquivFunctor	121	126	+5 (+4.13%)
Mathlib.Data.Nat.PSub	121	126	+5 (+4.13%)
Mathlib.Tactic.FunProp	73	76	+3 (+4.11%)
Mathlib.Data.Int.Cast.Basic	122	127	+5 (+4.10%)
Mathlib.Control.Bitraversable.Instances	269	280	+11 (+4.09%)
Mathlib.Algebra.Ring.Regular	123	128	+5 (+4.07%)
Mathlib.CategoryTheory.Category.Basic	271	282	+11 (+4.06%)
Mathlib.Tactic.CategoryTheory.CheckCompositions	272	283	+11 (+4.04%)
Mathlib.Algebra.Group.Hom.Instances	124	129	+5 (+4.03%)
Mathlib.Tactic.NormNum.Core	199	207	+8 (+4.02%)
Mathlib.Tactic.Widget.CommDiag	274	285	+11 (+4.01%)
Mathlib.Algebra.GroupWithZero.Hom	125	130	+5 (+4.00%)
Mathlib.Tactic.CategoryTheory.Coherence.Basic	275	286	+11 (+4.00%)
Mathlib.Tactic.CategoryTheory.Reassoc	275	286	+11 (+4.00%)
Mathlib.Tactic.ContinuousFunctionalCalculus	75	78	+3 (+4.00%)
Mathlib.Testing.Plausible.Sampleable	100	96	-4 (-4.00%)
Mathlib.Data.List.OffDiag	276	287	+11 (+3.99%)
Mathlib.Control.Bifunctor	251	261	+10 (+3.98%)
Mathlib.Tactic.NormNum.Parity	201	209	+8 (+3.98%)
Mathlib.Tactic.CategoryTheory.CancelIso	277	288	+11 (+3.97%)
Mathlib.Tactic.CategoryTheory.IsoReassoc	277	288	+11 (+3.97%)
Mathlib.CategoryTheory.ConcreteCategory.BundledHom	252	262	+10 (+3.97%)
Mathlib.CategoryTheory.ConcreteCategory.UnbundledHom	252	262	+10 (+3.97%)
Mathlib.Data.List.Count	252	262	+10 (+3.97%)
Mathlib.Data.List.Induction	252	262	+10 (+3.97%)
Mathlib.Tactic.CategoryTheory.BicategoricalComp	281	292	+11 (+3.91%)
Mathlib.Algebra.Ring.GrindInstances	128	133	+5 (+3.91%)
Mathlib.Data.List.Map2	256	266	+10 (+3.91%)
Mathlib.Data.Vector.Defs	256	266	+10 (+3.91%)
Mathlib.Logic.Equiv.Option	128	133	+5 (+3.91%)
Mathlib.Tactic.GRewrite.Core	77	80	+3 (+3.90%)
Mathlib.Data.Matrix.Auto	257	267	+10 (+3.89%)
Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes	283	294	+11 (+3.89%)
Mathlib.Data.List.TakeDrop	258	268	+10 (+3.88%)
Mathlib.Data.Nat.Factorial.Basic	258	268	+10 (+3.88%)
Mathlib.Data.Stream.Init	258	268	+10 (+3.88%)
Mathlib.Data.Int.Sqrt	259	269	+10 (+3.86%)
Mathlib.Tactic.CategoryTheory.Bicategory.Normalize	285	296	+11 (+3.86%)
Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence	285	296	+11 (+3.86%)
Mathlib.Data.Ordmap.Ordnode	156	162	+6 (+3.85%)
Mathlib.Tactic.CategoryTheory.Bicategory.Basic	289	300	+11 (+3.81%)
Mathlib.Algebra.EuclideanDomain.Field	184	191	+7 (+3.80%)
Mathlib.Algebra.Group.Hom.End	132	137	+5 (+3.79%)
Mathlib.Tactic.CategoryTheory.Elementwise	292	303	+11 (+3.77%)
Mathlib.Logic.Relation	80	83	+3 (+3.75%)
Mathlib.Algebra.Field.IsField	267	277	+10 (+3.75%)
Mathlib.Algebra.Ring.Hom.InjSurj	134	139	+5 (+3.73%)
Mathlib.Data.List.Nodup	269	279	+10 (+3.72%)
Mathlib.Algebra.Group.Prod	162	168	+6 (+3.70%)
Mathlib.CategoryTheory.ConcreteCategory.Bundled	54	56	+2 (+3.70%)
Mathlib.Control.Combinators	54	56	+2 (+3.70%)
Mathlib.Control.Lawful	54	56	+2 (+3.70%)
Mathlib.Control.ULift	54	56	+2 (+3.70%)
Mathlib.Data.Bool.AllAny	54	56	+2 (+3.70%)
Mathlib.Data.Bracket	54	56	+2 (+3.70%)
Mathlib.Data.Int.Notation	54	56	+2 (+3.70%)
Mathlib.Data.List.Duplicate	270	280	+10 (+3.70%)
Mathlib.Data.List.NatAntidiagonal	270	280	+10 (+3.70%)
Mathlib.Data.Nat.BinaryRec	54	56	+2 (+3.70%)
Mathlib.Data.Nat.Notation	54	56	+2 (+3.70%)
Mathlib.Data.Nat.NthRoot.Defs	54	56	+2 (+3.70%)
Mathlib.Data.Option.Defs	54	56	+2 (+3.70%)
Mathlib.Data.Option.NAry	54	56	+2 (+3.70%)
Mathlib.Data.Ordering.Basic	54	56	+2 (+3.70%)
Mathlib.Data.String.Defs	54	56	+2 (+3.70%)
Mathlib.Deprecated.Aliases	54	56	+2 (+3.70%)
Mathlib.Lean.CoreM	54	56	+2 (+3.70%)
Mathlib.Lean.Exception	54	56	+2 (+3.70%)
Mathlib.Lean.Json	54	56	+2 (+3.70%)
Mathlib.Lean.Meta.DiscrTree	54	56	+2 (+3.70%)
Mathlib.Lean.Meta.RefinedDiscrTree.Basic	54	56	+2 (+3.70%)
Mathlib.Lean.Thunk	54	56	+2 (+3.70%)
Mathlib.Logic.ExistsUnique	54	56	+2 (+3.70%)
Mathlib.Logic.Function.Coequalizer	54	56	+2 (+3.70%)
Mathlib.Logic.Function.CompTypeclasses	54	56	+2 (+3.70%)
Mathlib.Logic.Function.ULift	54	56	+2 (+3.70%)
Mathlib.Logic.IsEmpty.Defs	54	56	+2 (+3.70%)
Mathlib.Logic.Nonempty	54	56	+2 (+3.70%)
Mathlib.Logic.OpClass	54	56	+2 (+3.70%)
Mathlib.Tactic.ApplyAt	54	56	+2 (+3.70%)
Mathlib.Tactic.ApplyCongr	54	56	+2 (+3.70%)
Mathlib.Tactic.CasesM	54	56	+2 (+3.70%)
Mathlib.Tactic.CategoryTheory.CategoryStar	54	56	+2 (+3.70%)
Mathlib.Tactic.CategoryTheory.Coherence.Datatypes	54	56	+2 (+3.70%)
Mathlib.Tactic.Change	54	56	+2 (+3.70%)
Mathlib.Tactic.Check	54	56	+2 (+3.70%)
Mathlib.Tactic.Clean	54	56	+2 (+3.70%)
Mathlib.Tactic.ClearExcept	54	56	+2 (+3.70%)
Mathlib.Tactic.ClearExclamation	54	56	+2 (+3.70%)
Mathlib.Tactic.Clear_	54	56	+2 (+3.70%)
Mathlib.Tactic.Coe	54	56	+2 (+3.70%)
Mathlib.Tactic.Constructor	54	56	+2 (+3.70%)
Mathlib.Tactic.Conv	54	56	+2 (+3.70%)
Mathlib.Tactic.Core	54	56	+2 (+3.70%)
Mathlib.Tactic.CrossRefAttribute	54	56	+2 (+3.70%)
Mathlib.Tactic.DefEqAbuse	54	56	+2 (+3.70%)
Mathlib.Tactic.DefEqTransformations	54	56	+2 (+3.70%)
Mathlib.Tactic.Eqns	54	56	+2 (+3.70%)
Mathlib.Tactic.ErwQuestion	54	56	+2 (+3.70%)
Mathlib.Tactic.ExistsI	54	56	+2 (+3.70%)
Mathlib.Tactic.Explode.Datatypes	54	56	+2 (+3.70%)
Mathlib.Tactic.ExtendDoc	54	56	+2 (+3.70%)
Mathlib.Tactic.FailIfNoProgress	54	56	+2 (+3.70%)
Mathlib.Tactic.FastInstance	54	56	+2 (+3.70%)
Mathlib.Tactic.FieldSimp.Attr	54	56	+2 (+3.70%)
Mathlib.Tactic.FindSyntax	54	56	+2 (+3.70%)
Mathlib.Tactic.FunProp.Decl	54	56	+2 (+3.70%)
Mathlib.Tactic.FunProp.ToBatteries	54	56	+2 (+3.70%)
Mathlib.Tactic.GCongr.ForwardAttr	54	56	+2 (+3.70%)
Mathlib.Tactic.Generalize	54	56	+2 (+3.70%)
Mathlib.Tactic.GuardGoalNums	54	56	+2 (+3.70%)
Mathlib.Tactic.GuardHypNums	54	56	+2 (+3.70%)
Mathlib.Tactic.Have	54	56	+2 (+3.70%)
Mathlib.Tactic.HaveI	54	56	+2 (+3.70%)
Mathlib.Tactic.InferParam	54	56	+2 (+3.70%)
Mathlib.Tactic.Inhabit	54	56	+2 (+3.70%)
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes	54	56	+2 (+3.70%)
Mathlib.Tactic.Linter.HaveLetLinter	54	56	+2 (+3.70%)
Mathlib.Tactic.Linter.PPRoundtrip	54	56	+2 (+3.70%)
Mathlib.Tactic.Linter.TextBased.UnicodeLinter	54	56	+2 (+3.70%)
Mathlib.Tactic.Monotonicity.Attr	54	56	+2 (+3.70%)
Mathlib.Tactic.NthRewrite	54	56	+2 (+3.70%)
Mathlib.Tactic.Observe	54	56	+2 (+3.70%)
Mathlib.Tactic.OfNat	54	56	+2 (+3.70%)
Mathlib.Tactic.PPWithUniv	54	56	+2 (+3.70%)
Mathlib.Tactic.Polyrith	54	56	+2 (+3.70%)
Mathlib.Tactic.RSuffices	54	56	+2 (+3.70%)
Mathlib.Tactic.Recall	54	56	+2 (+3.70%)
Mathlib.Tactic.Recover	54	56	+2 (+3.70%)
Mathlib.Tactic.ReduceModChar.Ext	54	56	+2 (+3.70%)
Mathlib.Tactic.Relation.Rfl	54	56	+2 (+3.70%)
Mathlib.Tactic.Relation.Symm	54	56	+2 (+3.70%)
Mathlib.Tactic.Rename	54	56	+2 (+3.70%)
Mathlib.Tactic.RewriteSearch	54	56	+2 (+3.70%)
Mathlib.Tactic.Set	54	56	+2 (+3.70%)
Mathlib.Tactic.SimpRw	54	56	+2 (+3.70%)
Mathlib.Tactic.Simps.NotationClass	54	56	+2 (+3.70%)
Mathlib.Tactic.Spread	54	56	+2 (+3.70%)
Mathlib.Tactic.Substs	54	56	+2 (+3.70%)
Mathlib.Tactic.SuccessIfFailWithMsg	54	56	+2 (+3.70%)
Mathlib.Tactic.SudoSetOption	54	56	+2 (+3.70%)
Mathlib.Tactic.SuppressCompilation	54	56	+2 (+3.70%)
Mathlib.Tactic.SwapVar	54	56	+2 (+3.70%)
Mathlib.Tactic.ToExpr	54	56	+2 (+3.70%)
Mathlib.Tactic.Trace	54	56	+2 (+3.70%)
Mathlib.Tactic.Translate.Attributes	54	56	+2 (+3.70%)
Mathlib.Tactic.Translate.GuessName	54	56	+2 (+3.70%)
Mathlib.Tactic.Translate.Reorder	54	56	+2 (+3.70%)
Mathlib.Tactic.TryThis	54	56	+2 (+3.70%)
Mathlib.Tactic.TypeCheck	54	56	+2 (+3.70%)
Mathlib.Tactic.UnsetOption	54	56	+2 (+3.70%)
Mathlib.Tactic.Use	54	56	+2 (+3.70%)
Mathlib.Tactic.Variable	54	56	+2 (+3.70%)
Mathlib.Tactic.WithoutCDot	54	56	+2 (+3.70%)
Mathlib.Util.AddRelatedDecl	54	56	+2 (+3.70%)
Mathlib.Util.AssertNoSorry	54	56	+2 (+3.70%)
Mathlib.Util.CountHeartbeats	54	56	+2 (+3.70%)
Mathlib.Util.DelabNonCanonical	54	56	+2 (+3.70%)
Mathlib.Util.ElabWithoutMVars	54	56	+2 (+3.70%)
Mathlib.Util.Export	54	56	+2 (+3.70%)
Mathlib.Util.FormatTable	54	56	+2 (+3.70%)
Mathlib.Util.GetAllModules	54	56	+2 (+3.70%)
Mathlib.Util.LongNames	54	56	+2 (+3.70%)
Mathlib.Util.PPOptions	54	56	+2 (+3.70%)
Mathlib.Util.SleepHeartbeats	54	56	+2 (+3.70%)
Mathlib.Util.Superscript	54	56	+2 (+3.70%)
Mathlib.Util.Tactic	54	56	+2 (+3.70%)
Mathlib.Util.TermReduce	54	56	+2 (+3.70%)
Mathlib.Util.TransImports	54	56	+2 (+3.70%)
Mathlib.Util.WhatsNew	54	56	+2 (+3.70%)
Mathlib.Util.WithWeakNamespace	54	56	+2 (+3.70%)
Mathlib.Data.List.Dedup	272	282	+10 (+3.68%)
Mathlib.Algebra.BigOperators.Group.List.Basic	301	312	+11 (+3.65%)
Mathlib.Data.List.Perm.Lattice	274	284	+10 (+3.65%)
Mathlib.Algebra.Ring.Rat	329	341	+12 (+3.65%)
Mathlib.Algebra.HierarchyDesign	55	57	+2 (+3.64%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Note	55	57	+2 (+3.64%)
Mathlib.CategoryTheory.Category.Init	55	57	+2 (+3.64%)
Mathlib.Combinatorics.Matroid.Init	55	57	+2 (+3.64%)
Mathlib.Combinatorics.SimpleGraph.Init	55	57	+2 (+3.64%)
Mathlib.Data.Array.Extract	55	57	+2 (+3.64%)
Mathlib.Data.List.Monad	55	57	+2 (+3.64%)
Mathlib.Data.Prod.PProd	55	57	+2 (+3.64%)
Mathlib.Data.Sym.Sym2.Init	55	57	+2 (+3.64%)
Mathlib.Lean.Elab.Term	55	57	+2 (+3.64%)
Mathlib.Lean.EnvExtension	55	57	+2 (+3.64%)
Mathlib.Lean.Expr.Rat	55	57	+2 (+3.64%)
Mathlib.Lean.FoldEnvironment	55	57	+2 (+3.64%)
Mathlib.Lean.MessageData.ForExprs	55	57	+2 (+3.64%)
Mathlib.Lean.MessageData.Trace	55	57	+2 (+3.64%)
Mathlib.Lean.Meta.Tactic.Rewrite	55	57	+2 (+3.64%)
Mathlib.Lean.PrettyPrinter.Delaborator	55	57	+2 (+3.64%)
Mathlib.Tactic.ApplyWith	55	57	+2 (+3.64%)
Mathlib.Tactic.ArithMult.Init	55	57	+2 (+3.64%)
Mathlib.Tactic.Bound.Init	55	57	+2 (+3.64%)
Mathlib.Tactic.Cases	55	57	+2 (+3.64%)
Mathlib.Tactic.CategoryTheory.Coherence.Normalize	55	57	+2 (+3.64%)
Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence	55	57	+2 (+3.64%)
Mathlib.Tactic.Continuity.Init	55	57	+2 (+3.64%)
Mathlib.Tactic.DepRewrite	55	57	+2 (+3.64%)
Mathlib.Tactic.DeprecateTo	55	57	+2 (+3.64%)
Mathlib.Tactic.Eval	55	57	+2 (+3.64%)
Mathlib.Tactic.Explode.Pretty	55	57	+2 (+3.64%)
Mathlib.Tactic.Ext	55	57	+2 (+3.64%)
Mathlib.Tactic.FBinop	55	57	+2 (+3.64%)
Mathlib.Tactic.Find	55	57	+2 (+3.64%)
Mathlib.Tactic.Finiteness.Attr	55	57	+2 (+3.64%)
Mathlib.Tactic.FunProp.Mor	55	57	+2 (+3.64%)
Mathlib.Tactic.HigherOrder	55	57	+2 (+3.64%)
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss	55	57	+2 (+3.64%)
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm	55	57	+2 (+3.64%)
Mathlib.Tactic.Linter.DeprecatedModule	55	57	+2 (+3.64%)
Mathlib.Tactic.Linter.FindDeprecations	55	57	+2 (+3.64%)
Mathlib.Tactic.Linter.UpstreamableDecl	55	57	+2 (+3.64%)
Mathlib.Tactic.Linter.ValidatePRTitle	55	57	+2 (+3.64%)
Mathlib.Tactic.Measurability.Init	55	57	+2 (+3.64%)
Mathlib.Tactic.Monotonicity.Basic	55	57	+2 (+3.64%)
Mathlib.Tactic.Push.Attr	55	57	+2 (+3.64%)
Mathlib.Tactic.RenameBVar	55	57	+2 (+3.64%)
Mathlib.Tactic.Replace	55	57	+2 (+3.64%)
Mathlib.Tactic.ScopedNS	55	57	+2 (+3.64%)
Mathlib.Tactic.SimpIntro	55	57	+2 (+3.64%)
Mathlib.Tactic.SplitIfs	55	57	+2 (+3.64%)
Mathlib.Tactic.ToLevel	55	57	+2 (+3.64%)
Mathlib.Tactic.Translate.UnfoldBoundary	55	57	+2 (+3.64%)
Mathlib.Tactic.Widget.SelectInsertParamsClass	55	57	+2 (+3.64%)
Mathlib.Topology.Sheaves.Init	55	57	+2 (+3.64%)
Mathlib.Util.AtLocation	55	57	+2 (+3.64%)
Mathlib.Util.Delaborators	55	57	+2 (+3.64%)
Mathlib.Util.MemoFix	55	57	+2 (+3.64%)
Mathlib.Util.Simp	55	57	+2 (+3.64%)
Mathlib.Algebra.Quotient	250	259	+9 (+3.60%)
Mathlib.Data.List.InsertNth	251	260	+9 (+3.59%)
Mathlib.Algebra.Expr	56	58	+2 (+3.57%)
Mathlib.Data.Array.Defs	56	58	+2 (+3.57%)
Mathlib.Data.List.Fold	56	58	+2 (+3.57%)
Mathlib.Data.Rat.Init	56	58	+2 (+3.57%)
Mathlib.Data.SProd	56	58	+2 (+3.57%)
Mathlib.Data.String.Lemmas	56	58	+2 (+3.57%)
Mathlib.Data.Tree.Basic	56	58	+2 (+3.57%)
Mathlib.Lean.GoalsLocation	56	58	+2 (+3.57%)
Mathlib.Lean.LocalContext	56	58	+2 (+3.57%)
Mathlib.Lean.Meta.Basic	56	58	+2 (+3.57%)
Mathlib.Lean.Meta.RefinedDiscrTree.Initialize	56	58	+2 (+3.57%)
Mathlib.Lean.Meta.Simp	56	58	+2 (+3.57%)
Mathlib.Lean.Name	56	58	+2 (+3.57%)
Mathlib.Logic.Nontrivial.Defs	56	58	+2 (+3.57%)
Mathlib.Tactic.ArithMult	56	58	+2 (+3.57%)
Mathlib.Tactic.Attr.Register	56	58	+2 (+3.57%)
Mathlib.Tactic.CategoryTheory.MonoidalComp	308	319	+11 (+3.57%)
Mathlib.Tactic.Continuity	56	58	+2 (+3.57%)
Mathlib.Tactic.Explode	56	58	+2 (+3.57%)
Mathlib.Tactic.IrreducibleDef	56	58	+2 (+3.57%)
Mathlib.Util.AliasIn	56	58	+2 (+3.57%)
Mathlib.Util.AtomM	56	58	+2 (+3.57%)
Mathlib.Util.DischargerAsTactic	56	58	+2 (+3.57%)
Mathlib.Util.Qq	56	58	+2 (+3.57%)
Mathlib.Util.SynthesizeUsing	56	58	+2 (+3.57%)
Mathlib.Order.GaloisConnection.Defs	169	163	-6 (-3.55%)
Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes	310	321	+11 (+3.55%)
Mathlib.Logic.Equiv.Basic	141	146	+5 (+3.55%)
Mathlib.Tactic.CategoryTheory.Monoidal.Normalize	312	323	+11 (+3.53%)
Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence	312	323	+11 (+3.53%)
Mathlib.Logic.Equiv.Bool	142	147	+5 (+3.52%)
Mathlib.Data.Int.Cast.Pi	57	59	+2 (+3.51%)
Mathlib.Data.List.Lookmap	57	59	+2 (+3.51%)
Mathlib.Data.Num.Basic	57	59	+2 (+3.51%)
Mathlib.Lean.Meta.KAbstractPositions	57	59	+2 (+3.51%)
Mathlib.Logic.Function.Defs	57	59	+2 (+3.51%)
Mathlib.Tactic.FunProp.FunctionData	57	59	+2 (+3.51%)
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector	57	59	+2 (+3.51%)
Mathlib.Tactic.Linter.TextBased	57	59	+2 (+3.51%)
Mathlib.Tactic.Measurability	57	59	+2 (+3.51%)
Mathlib.Tactic.Simproc.Divisors	57	59	+2 (+3.51%)
Mathlib.Tactic.Simproc.ExistsAndEq	57	59	+2 (+3.51%)
Mathlib.Util.AtomM.Recurse	57	59	+2 (+3.51%)
Mathlib.Algebra.Group.Units.Hom	143	148	+5 (+3.50%)
Mathlib.Data.ULift	143	148	+5 (+3.50%)
Mathlib.Tactic.CategoryTheory.Monoidal.Basic	316	327	+11 (+3.48%)
Mathlib.Data.Int.Basic	115	119	+4 (+3.48%)
Mathlib.Algebra.Free	144	149	+5 (+3.47%)
Mathlib.Algebra.Group.Invertible.Basic	144	149	+5 (+3.47%)
Mathlib.Algebra.GroupWithZero.Defs	87	90	+3 (+3.45%)
Mathlib.Data.Nat.Init	58	60	+2 (+3.45%)
Mathlib.Lean.Meta	58	60	+2 (+3.45%)
Mathlib.Logic.Relator	58	60	+2 (+3.45%)
Mathlib.Tactic.Bound.Attribute	58	60	+2 (+3.45%)
Mathlib.Tactic.Widget.SelectPanelUtils	58	60	+2 (+3.45%)
Mathlib.Data.List.Rotate	291	301	+10 (+3.44%)
Mathlib.Data.Seq.Computation	262	271	+9 (+3.44%)
Mathlib.Tactic.Widget.StringDiagram	321	332	+11 (+3.43%)
Mathlib.Algebra.Ring.Nat	117	121	+4 (+3.42%)
Mathlib.Data.Sum.Basic	88	91	+3 (+3.41%)
Mathlib.Logic.Embedding.Basic	147	152	+5 (+3.40%)
Mathlib.Data.Int.Init	59	61	+2 (+3.39%)
Mathlib.Lean.Elab.Tactic.Basic	59	61	+2 (+3.39%)
Mathlib.Lean.Meta.RefinedDiscrTree.Encode	59	61	+2 (+3.39%)
Mathlib.Tactic.Order.CollectFacts	59	61	+2 (+3.39%)
Mathlib.Tactic.Says	59	61	+2 (+3.39%)
Mathlib.Algebra.FreeMonoid.Basic	299	309	+10 (+3.34%)
Mathlib.Algebra.CharZero.Defs	90	93	+3 (+3.33%)
Mathlib.Data.Rat.Defs	270	279	+9 (+3.33%)
Mathlib.Lean.Meta.RefinedDiscrTree.Lookup	60	62	+2 (+3.33%)
Mathlib.Tactic.Hint	60	62	+2 (+3.33%)
Mathlib.Tactic.ITauto	60	62	+2 (+3.33%)
Mathlib.Tactic.Order.Graph.Basic	60	62	+2 (+3.33%)
Mathlib.Tactic.Order.Preprocessing	60	62	+2 (+3.33%)
Mathlib.Tactic.Sat.FromLRAT	90	93	+3 (+3.33%)
Mathlib.Tactic.TFAE	60	62	+2 (+3.33%)
Mathlib.Testing.Plausible.Testable	60	62	+2 (+3.33%)
Mathlib.Algebra.Divisibility.Prod	301	311	+10 (+3.32%)
Mathlib.Algebra.FreeMonoid.Count	303	313	+10 (+3.30%)
Mathlib.Data.List.Perm.Subperm	273	282	+9 (+3.30%)
Mathlib.Algebra.Group.WithOne.Defs	274	283	+9 (+3.28%)
Mathlib.Data.Tree.Get	61	63	+2 (+3.28%)
Mathlib.Tactic.Linter	61	63	+2 (+3.28%)
Mathlib.Tactic.Order.Graph.Tarjan	61	63	+2 (+3.28%)
Mathlib.Tactic.Widget.CongrM	61	63	+2 (+3.28%)
Mathlib.Tactic.Widget.GCongr	61	63	+2 (+3.28%)
Mathlib.Util.Notation3	61	63	+2 (+3.28%)
Mathlib.Algebra.GroupWithZero.Regular	92	95	+3 (+3.26%)
Mathlib.Algebra.Ring.Units	184	190	+6 (+3.26%)
Mathlib.Data.List.Zip	276	285	+9 (+3.26%)
Mathlib.Algebra.Group.Idempotent	123	127	+4 (+3.25%)
Mathlib.Logic.Basic	62	64	+2 (+3.23%)
Mathlib.Tactic.Translate.Core	62	64	+2 (+3.23%)
Mathlib.Algebra.GroupWithZero.Idempotent	126	130	+4 (+3.17%)
Mathlib.Lean.Meta.RefinedDiscrTree	63	65	+2 (+3.17%)
Mathlib.Tactic.Order.ToInt	63	65	+2 (+3.17%)
Mathlib.Tactic.Subsingleton	63	65	+2 (+3.17%)
Mathlib.Tactic.Translate.TagUnfoldBoundary	63	65	+2 (+3.17%)
Mathlib.Tactic.Translate.ToAdditive	63	65	+2 (+3.17%)
Mathlib.Tactic.Widget.Calc	63	65	+2 (+3.17%)
Mathlib.Tactic.Widget.InteractiveUnfold	63	65	+2 (+3.17%)
Mathlib.Algebra.Group.Equiv.Basic	159	164	+5 (+3.14%)
Mathlib.Algebra.Group.Irreducible.Defs	96	99	+3 (+3.12%)
Mathlib.Algebra.Notation	64	66	+2 (+3.12%)
Mathlib.Algebra.Ring.Defs	96	99	+3 (+3.12%)
Mathlib.Data.Nat.MaxPowDiv	64	66	+2 (+3.12%)
Mathlib.Tactic.ToAdditive	64	66	+2 (+3.12%)
Mathlib.Tactic.Translate.ToDual	64	66	+2 (+3.12%)
Mathlib.Algebra.Ring.Basic	161	166	+5 (+3.11%)
Mathlib.Tactic.Widget.Conv	65	67	+2 (+3.08%)
Mathlib.Control.ULiftable	294	303	+9 (+3.06%)
Mathlib.Data.Nat.Basic	98	101	+3 (+3.06%)
Mathlib.Algebra.Field.Defs	99	102	+3 (+3.03%)
Mathlib.Algebra.Notation.Defs	66	68	+2 (+3.03%)
Mathlib.Algebra.Notation.Lemmas	66	68	+2 (+3.03%)
Mathlib.Algebra.Ring.Hom.Defs	165	170	+5 (+3.03%)
Mathlib.Data.Char	99	102	+3 (+3.03%)
Mathlib.Tactic.ToDual	66	68	+2 (+3.03%)
Mathlib.Data.List.Basic	266	274	+8 (+3.01%)
Mathlib.Data.Nat.Sqrt	100	103	+3 (+3.00%)
Mathlib.Data.List.Enum	267	275	+8 (+3.00%)
Mathlib.Data.List.Lattice	267	275	+8 (+3.00%)
Mathlib.Data.List.ReduceOption	267	275	+8 (+3.00%)
Mathlib.Data.Int.GCD	301	310	+9 (+2.99%)
Mathlib.Order.OrderDual	134	138	+4 (+2.99%)
Mathlib.Tactic.Push	67	69	+2 (+2.99%)
Mathlib.Algebra.Group.InjSurj	101	104	+3 (+2.97%)
Mathlib.Algebra.Group.TypeTags.Basic	135	139	+4 (+2.96%)
Mathlib.Order.Compare	135	139	+4 (+2.96%)
Mathlib.Order.Max	135	139	+4 (+2.96%)
Mathlib.Data.Seq.Defs	271	279	+8 (+2.95%)
Mathlib.Data.Set.Defs	68	70	+2 (+2.94%)
Mathlib.Order.RelClasses	136	140	+4 (+2.94%)
Mathlib.Tactic.Contrapose	68	70	+2 (+2.94%)
Mathlib.Data.Nat.Log	171	176	+5 (+2.92%)
Mathlib.Data.Nat.Choose.Basic	274	282	+8 (+2.92%)
Mathlib.Order.Bounds.Defs	69	71	+2 (+2.90%)
Mathlib.Tactic.ByCases	69	71	+2 (+2.90%)
Mathlib.Tactic.ByContra	69	71	+2 (+2.90%)
Mathlib.Algebra.Homology.ComplexShape	104	107	+3 (+2.88%)
Mathlib.Lean.Expr.ExtraRecognizers	70	72	+2 (+2.86%)
Mathlib.Tactic.ToFun	70	72	+2 (+2.86%)
Mathlib.Tactic.WLOG	70	72	+2 (+2.86%)
Mathlib.Data.List.Infix	281	289	+8 (+2.85%)
Mathlib.Algebra.GroupWithZero.WithZero	317	326	+9 (+2.84%)
Mathlib.Algebra.Group.Nat.Hom	142	146	+4 (+2.82%)
Mathlib.Order.Defs.Unbundled	71	73	+2 (+2.82%)
Mathlib.Algebra.Group.Pi.Basic	107	110	+3 (+2.80%)
Mathlib.Algebra.GroupWithZero.InjSurj	107	110	+3 (+2.80%)
Mathlib.Algebra.Ring.WithZero	321	330	+9 (+2.80%)
Mathlib.Algebra.GroupWithZero.Divisibility	286	294	+8 (+2.80%)
Mathlib.Topology.ContinuousMap.Defs	143	147	+4 (+2.80%)
Mathlib.Algebra.ContinuedFractions.Basic	287	295	+8 (+2.79%)
Mathlib.Algebra.Notation.Pi.Defs	72	74	+2 (+2.78%)
Mathlib.Algebra.Prime.Defs	288	296	+8 (+2.78%)
Mathlib.Algebra.GroupWithZero.Prod	325	334	+9 (+2.77%)
Mathlib.Data.List.Lex	291	299	+8 (+2.75%)
Mathlib.Algebra.Group.WithOne.Basic	292	300	+8 (+2.74%)
Mathlib.Order.BoundedOrder.Basic	146	150	+4 (+2.74%)
Mathlib.Algebra.Group.Hom.Defs	110	113	+3 (+2.73%)
Mathlib.Algebra.Group.Ext	111	114	+3 (+2.70%)
Mathlib.Data.List.Chain	296	304	+8 (+2.70%)
Mathlib.Tactic.FinCases	373	383	+10 (+2.68%)
Mathlib.Tactic.Widget.LibraryRewrite	75	77	+2 (+2.67%)
Mathlib.Data.Sigma.Lex	76	78	+2 (+2.63%)
Mathlib.Order.Basic	114	117	+3 (+2.63%)
Mathlib.Tactic.DeriveCountable	266	273	+7 (+2.63%)
Mathlib.Tactic.GCongr.Core	76	78	+2 (+2.63%)
Mathlib.Tactic.Peel	269	276	+7 (+2.60%)
Mathlib.Data.List.Flatten	77	79	+2 (+2.60%)
Mathlib.Tactic.GCongr.CoreAttrs	77	79	+2 (+2.60%)
Mathlib.Data.List.Defs	79	81	+2 (+2.53%)
Mathlib.Data.List.TakeWhile	119	122	+3 (+2.52%)
Mathlib.Algebra.Ring.Ext	120	123	+3 (+2.50%)
Mathlib.Data.Nat.Bits	81	83	+2 (+2.47%)
Mathlib.Tactic.CancelDenoms.Core	324	332	+8 (+2.47%)
Mathlib.Order.Monotone.Basic	163	167	+4 (+2.45%)
Mathlib.Data.Nat.Size	82	84	+2 (+2.44%)
Mathlib.Order.Lattice	168	172	+4 (+2.38%)
Mathlib.Order.Monotone.Defs	126	129	+3 (+2.38%)
Mathlib.Tactic.GCongr	84	86	+2 (+2.38%)
Mathlib.Tactic.Order	84	86	+2 (+2.38%)
Mathlib.Order.BoundedOrder.Monotone	169	173	+4 (+2.37%)
Mathlib.Data.List.GetD	85	87	+2 (+2.35%)
Mathlib.Data.PNat.Defs	128	125	-3 (-2.34%)
Mathlib.Logic.Function.Basic	86	88	+2 (+2.33%)
Mathlib.Data.Sigma.Basic	87	89	+2 (+2.30%)
Mathlib.Logic.Function.Conjugate	87	89	+2 (+2.30%)
Mathlib.Tactic.Choose	87	89	+2 (+2.30%)
Mathlib.Logic.Pairwise	88	90	+2 (+2.27%)
Mathlib.Logic.Function.Iterate	89	91	+2 (+2.25%)
Mathlib.Logic.IsEmpty.Basic	89	91	+2 (+2.25%)
Mathlib.Logic.Unique	89	91	+2 (+2.25%)
Mathlib.Control.Traversable.Equiv	136	139	+3 (+2.21%)
Mathlib.Algebra.Notation.Pi.Basic	92	94	+2 (+2.17%)
Mathlib.Algebra.Group.Opposite	140	143	+3 (+2.14%)
Mathlib.Algebra.Order.Monoid.Unbundled.Defs	141	144	+3 (+2.13%)
Mathlib.Data.FunLike.Basic	94	96	+2 (+2.13%)
Mathlib.Tactic.ModCases	425	434	+9 (+2.12%)
Mathlib.Data.FunLike.Embedding	95	97	+2 (+2.11%)
Mathlib.Data.Option.Basic	95	97	+2 (+2.11%)
Mathlib.Tactic.NormNum.Basic	381	389	+8 (+2.10%)
Mathlib.Algebra.Group.Action.Pretransitive	143	146	+3 (+2.10%)
Mathlib.Tactic.NormNum.BigOperators	383	391	+8 (+2.09%)
Mathlib.Algebra.Group.Equiv.TypeTags	144	147	+3 (+2.08%)
Mathlib.Algebra.GroupWithZero.NeZero	96	98	+2 (+2.08%)
Mathlib.Data.FunLike.Equiv	96	98	+2 (+2.08%)
Mathlib.Tactic.Abel	384	392	+8 (+2.08%)
Mathlib.Tactic.Positivity.Finset	384	392	+8 (+2.08%)
Mathlib.Tactic.NoncommRing	386	394	+8 (+2.07%)
Mathlib.Tactic.NormNum.Pow	389	397	+8 (+2.06%)
Mathlib.Tactic.NormNum.PowMod	390	398	+8 (+2.05%)
Mathlib.Algebra.GroupWithZero.Opposite	147	150	+3 (+2.04%)
Mathlib.Tactic.ReduceModChar	395	403	+8 (+2.03%)
Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs	149	152	+3 (+2.01%)
Mathlib.Tactic.NormNum.Prime	409	417	+8 (+1.96%)
Mathlib.Algebra.GroupWithZero.Action.Defs	156	159	+3 (+1.92%)
Mathlib.Algebra.Ring.InjSurj	156	159	+3 (+1.92%)
Mathlib.Data.Nat.Find	104	106	+2 (+1.92%)
Mathlib.Tactic.PNatToNat	475	484	+9 (+1.89%)
Mathlib.Tactic.CategoryTheory.ToApp	425	433	+8 (+1.88%)
Mathlib.Tactic.NormNum.Inv	481	490	+9 (+1.87%)
Mathlib.Tactic.ENatToNat	535	545	+10 (+1.87%)
Mathlib.Tactic.NormNum.Eq	482	491	+9 (+1.87%)
Mathlib.Tactic.Ring.Common	483	492	+9 (+1.86%)
Mathlib.Tactic.Ring.Basic	484	493	+9 (+1.86%)
Mathlib.Tactic.CategoryTheory.BicategoryCoherence	432	440	+8 (+1.85%)
Mathlib.Tactic.Ring.RingNF	487	496	+9 (+1.85%)
Mathlib.Tactic.Monotonicity.Lemmas	325	331	+6 (+1.85%)
Mathlib.Tactic.NormNum.Abs	488	497	+9 (+1.84%)
Mathlib.Tactic.Monotonicity	327	333	+6 (+1.83%)
Mathlib.Tactic.Qify	491	500	+9 (+1.83%)
Mathlib.Data.Int.DivMod	55	56	+1 (+1.82%)
Mathlib.Order.Iterate	165	168	+3 (+1.82%)
Mathlib.Tactic.Positivity.Core	498	507	+9 (+1.81%)
Mathlib.Tactic.Finiteness	499	508	+9 (+1.80%)
Mathlib.Tactic.FieldSimp.Lemmas	389	396	+7 (+1.80%)
Mathlib.Tactic.FieldSimp.Discharger	501	510	+9 (+1.80%)
Mathlib.Data.List.TFAE	56	57	+1 (+1.79%)
Mathlib.Tactic.DeriveEncodable	395	402	+7 (+1.77%)
Mathlib.Tactic.Positivity.Basic	510	519	+9 (+1.76%)
Mathlib.Data.List.ModifyLast	57	58	+1 (+1.75%)
Mathlib.Logic.Equiv.Defs	115	117	+2 (+1.74%)
Mathlib.Tactic.NormNum.OfScientific	578	588	+10 (+1.73%)
Mathlib.Tactic.Ring.PNat	521	530	+9 (+1.73%)
Mathlib.Tactic.NormNum.Ineq	522	531	+9 (+1.72%)
Mathlib.Tactic.ProdAssoc	116	118	+2 (+1.72%)
Mathlib.Tactic.ProxyType	116	118	+2 (+1.72%)
Mathlib.Tactic.NormNum.DivMod	523	532	+9 (+1.72%)
Mathlib.Tactic.Ring	525	534	+9 (+1.71%)
Mathlib.Tactic.CancelDenoms	526	535	+9 (+1.71%)
Mathlib.Tactic.LinearCombinationPrime	526	535	+9 (+1.71%)
Mathlib.Logic.Small.Defs	117	119	+2 (+1.71%)
Mathlib.Tactic.Ring.Compare	527	536	+9 (+1.71%)
Mathlib.Tactic.Group	528	537	+9 (+1.70%)
Mathlib.Tactic.NormNum.ModEq	529	538	+9 (+1.70%)
Mathlib.Tactic.NormNum	589	599	+10 (+1.70%)
Mathlib.Data.Finite.Defs	118	120	+2 (+1.69%)
Mathlib.Data.Opposite	118	120	+2 (+1.69%)
Mathlib.Logic.UnivLE	118	120	+2 (+1.69%)
Mathlib.Tactic.DeriveFintype	118	120	+2 (+1.69%)
Mathlib.Tactic.NormNum.NatFactorial	590	600	+10 (+1.69%)
Mathlib.Tactic.NormNum.NatSqrt	590	600	+10 (+1.69%)
Mathlib.Tactic.IntervalCases	591	601	+10 (+1.69%)
Mathlib.Tactic.NormNum.GCD	591	601	+10 (+1.69%)
Mathlib.Tactic.NormNum.NatLog	591	601	+10 (+1.69%)
Mathlib.Tactic.NormNum.IsSquare	592	602	+10 (+1.69%)
Mathlib.Tactic.LinearCombination.Lemmas	474	482	+8 (+1.69%)
Mathlib.Combinatorics.Quiver.Basic	119	121	+2 (+1.68%)
Mathlib.Tactic.Simproc.VecPerm	656	667	+11 (+1.68%)
Mathlib.Tactic.Linarith.Lemmas	479	487	+8 (+1.67%)
Mathlib.Tactic.Positivity	541	550	+9 (+1.66%)
Mathlib.Logic.Equiv.Prod	121	123	+2 (+1.65%)
Mathlib.Tactic.Rify	607	617	+10 (+1.65%)
Mathlib.Tactic.Simproc.Factors	494	502	+8 (+1.62%)
Mathlib.Tactic.Linarith.Datatypes	495	503	+8 (+1.62%)
Mathlib.Data.Countable.Defs	124	126	+2 (+1.61%)
Mathlib.Tactic.Linarith.Parsing	496	504	+8 (+1.61%)
Mathlib.Tactic.Linarith.Oracle.FourierMotzkin	497	505	+8 (+1.61%)
Mathlib.Tactic.Linarith.Verification	497	505	+8 (+1.61%)
Mathlib.Logic.Equiv.Sum	125	127	+2 (+1.60%)
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm	500	508	+8 (+1.60%)
Mathlib.Tactic.Linarith.Preprocessing	503	511	+8 (+1.59%)
Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates	569	578	+9 (+1.58%)
Mathlib.Tactic.CategoryTheory.Coherence	446	453	+7 (+1.57%)
Mathlib.Tactic.Simproc.FinsetInterval	643	653	+10 (+1.56%)
Mathlib.Algebra.Group.Equiv.Defs	129	131	+2 (+1.55%)
Mathlib.Control.Monad.Cont	131	133	+2 (+1.53%)
Mathlib.Topology.Defs.Basic	134	132	-2 (-1.49%)
Mathlib.Tactic.Linarith.Frontend	539	547	+8 (+1.48%)
Mathlib.Tactic.Bound	540	548	+8 (+1.48%)
Mathlib.Tactic.Linarith	613	622	+9 (+1.47%)
Mathlib.Order.Defs.PartialOrder	69	70	+1 (+1.45%)
Mathlib.Tactic.LinearCombination	554	562	+8 (+1.44%)
Mathlib.Algebra.Group.Pi.Units	139	141	+2 (+1.44%)
Mathlib.Order.Notation	70	71	+1 (+1.43%)
Mathlib.Tactic.NormNum.NatFib	726	736	+10 (+1.38%)
Mathlib.Tactic.NormNum.Ordinal	726	736	+10 (+1.38%)
Mathlib.Order.Interval.Set.Defs	73	74	+1 (+1.37%)
Mathlib.Tactic.NormNum.IsCoprime	744	754	+10 (+1.34%)
Mathlib.Tactic.FieldSimp	527	534	+7 (+1.33%)
Mathlib.Tactic.Algebra.Lemmas	769	779	+10 (+1.30%)
Mathlib.Tactic.Algebra.Basic	770	780	+10 (+1.30%)
Mathlib.Tactic.Algebraize	854	865	+11 (+1.29%)
Mathlib.Algebra.NeZero	78	79	+1 (+1.28%)
Mathlib.Tactic.Field	554	561	+7 (+1.26%)
Mathlib.Data.Subtype	91	92	+1 (+1.10%)
Mathlib.Data.Prod.Basic	92	93	+1 (+1.09%)
Mathlib.Data.List.DropRight	279	276	-3 (-1.08%)
Mathlib.Data.List.Sigma	285	288	+3 (+1.05%)
Mathlib.Tactic.Module	959	969	+10 (+1.04%)
Mathlib.Algebra.Notation.Prod	97	98	+1 (+1.03%)
Mathlib.Tactic.ApplyFun	194	196	+2 (+1.03%)
Mathlib.Logic.Nontrivial.Basic	104	105	+1 (+0.96%)
Mathlib.Tactic.ComputeDegree	1077	1086	+9 (+0.84%)
Mathlib.Algebra.Opposites	126	127	+1 (+0.79%)
Mathlib.Tactic.NormNum.RealSqrt	1302	1312	+10 (+0.77%)
Mathlib.Algebra.Group.Action.Defs	132	133	+1 (+0.76%)
Mathlib.Algebra.AddTorsor.Defs	133	134	+1 (+0.75%)
Mathlib.Algebra.Group.Action.Faithful	133	134	+1 (+0.75%)
Mathlib.Algebra.Group.Action.Option	134	135	+1 (+0.75%)
Mathlib.Algebra.Group.Action.Sum	134	135	+1 (+0.75%)
Mathlib.Data.List.Perm.Basic	272	270	-2 (-0.74%)
Mathlib.Tactic.ComputeAsymptotics.Lemmas	1473	1483	+10 (+0.68%)
Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion	1726	1736	+10 (+0.58%)
Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis	1787	1796	+9 (+0.50%)
Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized	1788	1797	+9 (+0.50%)
Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic	1789	1798	+9 (+0.50%)
Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs	1796	1805	+9 (+0.50%)
Mathlib.Tactic.NormNum.Irrational	1905	1914	+9 (+0.47%)
Mathlib.Tactic.NormNum.LegendreSymbol	3031	3042	+11 (+0.36%)

Import changes for all files

Files	Import difference
../mathlib-ci/scripts/pr_summary/import_trans_difference.sh all
There are 8010 files with changed transitive imports taking up over 348564 characters: this is too many to display!
You can run this locally from your `mathlib4` directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

Declarations diff

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

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.

No changes to weak technical debt.

mathlib-merge-conflicts · 2026-05-17T23:42:45Z

This pull request has conflicts, please merge master and resolve them.

MichaelStollBayreuth added 30 commits May 16, 2026 21:19

after shake Mathlib.Logic.Basic

5dd8339

after shake Mathlib.Data.Nat.Init

72c464c

after shake Mathlib.Data.Int.Init

6e507ac

after shake Mathlib.Data.Num.Basic

aaf9bb2

after shake Mathlib.Data.Int.Cast.Pi

fb89b84

after shake Mathlib.Data.Tree.Basic

98b67ca

after shake Mathlib.Data.SProd

cc6534b

after shake Mathlib.Logic.Relator

b59cf0e

after shake Mathlib.Control.Basic

3ce2633

after shake Mathlib.Data.List.Triplewise

a9e67c2

after shake Mathlib.Data.Nat.MaxPowDiv

7eb1c93

after shake Mathlib.Testing.Plausible.Testable

0b44084

after shake Mathlib.Data.Tree.Get

e13523e

after shaking&fixing Mathlib.Data.TwoPointing

a913130

after shake Mathlib.Algebra.Notation

c446da5

after shaking&fixing Mathlib.Logic.Lemmas

b4584f8

after shaking&fixing Mathlib.Algebra.Notation.Defs

77d788c

after shake Mathlib.Algebra.Notation.Lemmas

fb0a595

after shake Mathlib.Algebra.Regular.Defs

df33183

after shake Mathlib.Algebra.Notation.Pi.Defs

272dd8e

after shake Mathlib.Order.Defs.PartialOrder

1003ef9

after shake Mathlib.Data.Set.Defs

455d423

after shaking&fixing Mathlib.Order.Notation

84da041

after shake Mathlib.Algebra.Group.Defs

5b82ad0

after shake Mathlib.Algebra.NeZero

e79219a

after shake Mathlib.Order.Defs.LinearOrder

d1a3903

after shake Mathlib.Order.Bounds.Defs

573e6df

after shake Mathlib.Order.Interval.Set.Defs

050b9e4

after shake Mathlib.Order.Defs.Unbundled

17b8d75

after shake Mathlib.Algebra.Group.Invertible.Defs

94009c8

MichaelStollBayreuth added 22 commits May 16, 2026 23:21

after shake Mathlib.Data.List.Chain

37ec263

after shaking&fixing Mathlib.Algebra.EuclideanDomain.Field

ac741ca

after shake Mathlib.Order.GaloisConnection.Defs

b5ea30c

after shake Mathlib.Order.Iterate

1230435

after shake Mathlib.Data.Nat.Log

8718866

after shake Mathlib.Order.BoundedOrder.Monotone

0d36761

after shake Mathlib.Order.Lattice

290dcf4

after shake Mathlib.Algebra.Ring.Units

415a009

after shake Mathlib.Algebra.FreeMonoid.Count

f4459ae

after shake Mathlib.Algebra.Group.Action.Option

95c72f8

after shake Mathlib.Algebra.Group.Action.Sum

9213858

after shake Mathlib.Algebra.Group.Action.Pretransitive

55fe7a3

after shaking&fixing Mathlib.Algebra.GroupWithZero.Action.Defs

d3066ee

after shake Mathlib.Algebra.Ring.WithZero

6ac2922

after shake Mathlib.Algebra.Divisibility.Prod

a09aff6

after shake Mathlib.Algebra.GroupWithZero.Prod

75b9d11

after shake Mathlib.Logic.Equiv.Bool

4b370aa

after shake Mathlib.Algebra.Group.Equiv.Basic

1b943cd

after shake Mathlib.Data.ULift

a25e3ee

after shake Mathlib.Control.ULiftable

1414f4c

after shaking&fixing Mathlib.Logic.Embedding.Basic

c9b1aa2

add module list and list of fixes

b28b8b5

MichaelStollBayreuth added WIP Work in progress tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip labels May 16, 2026

MichaelStollBayreuth changed the title ~~chore: run lake shake iteratively and fix problems~~ chore: run lake shake iteratively and fix problems May 16, 2026

github-actions Bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label May 16, 2026

MichaelStollBayreuth mentioned this pull request May 17, 2026

chore: run lake shake successively from the leaves #39499

Open

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 17, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

chore: run `lake shake` iteratively and fix problems#39481

chore: run `lake shake` iteratively and fix problems#39481
MichaelStollBayreuth wants to merge 301 commits into
leanprover-community:masterfrom
MichaelStollBayreuth:MS_shake_test

MichaelStollBayreuth commented May 16, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented May 16, 2026

Import changes for modified files

Declarations diff

Uh oh!

mathlib-merge-conflicts Bot commented May 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

MichaelStollBayreuth commented May 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented May 16, 2026

PR summary b28b8b58c3

Import changes for modified files

Declarations diff

Uh oh!

mathlib-merge-conflicts Bot commented May 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

MichaelStollBayreuth commented May 16, 2026 •

edited

Loading