thorimur · Oct 9, 2026 · Oct 5, 2026 · Oct 9, 2026
diff --git a/Mathlib/Algebra/Algebra/Basic.lean b/Mathlib/Algebra/Algebra/Basic.lean
@@ -11,8 +11,8 @@ public import Mathlib.Algebra.Module.Submodule.Ker
 public import Mathlib.Algebra.Module.ULift
 public import Mathlib.Algebra.Ring.CharZero
 public import Mathlib.Algebra.Ring.Subring.Basic
-public import Mathlib.Data.Nat.Cast.Order.Basic
 public import Mathlib.Data.Int.CharZero
+public import Mathlib.Data.Nat.Cast.Order.Basic
 
 import Mathlib.Algebra.Ring.Hom.InjSurj
 

diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Matrix.lean b/Mathlib/Algebra/Algebra/Subalgebra/Matrix.lean
@@ -5,8 +5,8 @@ Authors: Bryan Wang
 -/
 module
 
-public import Mathlib.Data.Matrix.Basic
 public import Mathlib.Algebra.Algebra.Subalgebra.Basic
+public import Mathlib.Data.Matrix.Basic
 
 /-!
 # Matrix subalgebras

diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Operations.lean b/Mathlib/Algebra/Algebra/Subalgebra/Operations.lean
@@ -6,8 +6,8 @@ Authors: Andrew Yang, Antoine Chambert-Loir
 module
 
 public import Mathlib.Algebra.Algebra.Subalgebra.Basic
-public import Mathlib.RingTheory.Ideal.Maps
 public import Mathlib.Algebra.Ring.Action.Submonoid
+public import Mathlib.RingTheory.Ideal.Maps
 
 /-!
 # More operations on subalgebras

diff --git a/Mathlib/Algebra/Algebra/Unitization.lean b/Mathlib/Algebra/Algebra/Unitization.lean
@@ -5,10 +5,10 @@ Authors: Jireh Loreaux
 -/
 module
 
+public import Mathlib.Algebra.Module.TransferInstance
 public import Mathlib.Algebra.Star.Module
-public import Mathlib.Algebra.Star.StarProjection
 public import Mathlib.Algebra.Star.NonUnitalSubalgebra
-public import Mathlib.Algebra.Module.TransferInstance
+public import Mathlib.Algebra.Star.StarProjection
 
 import Mathlib.Tactic.Abel
 

diff --git a/Mathlib/Algebra/BigOperators/Expect.lean b/Mathlib/Algebra/BigOperators/Expect.lean
@@ -7,13 +7,13 @@ module
 
 public import Mathlib.Algebra.Algebra.Rat
 public import Mathlib.Algebra.BigOperators.GroupWithZero.Action
+public import Mathlib.Algebra.Group.Pointwise.Finset.Basic
 public import Mathlib.Algebra.Module.Pi
 public import Mathlib.Data.Finset.Density
 public import Mathlib.Data.Fintype.BigOperators
-public import Mathlib.Algebra.Group.Pointwise.Finset.Basic
 
-import Mathlib.Algebra.BigOperators.Ring.Finset
 import Mathlib.Algebra.BigOperators.Group.Finset.Indicator
+import Mathlib.Algebra.BigOperators.Ring.Finset
 
 /-!
 # Average over a finset

diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
@@ -5,11 +5,11 @@ Authors: Johannes Hölzl
 -/
 module
 
+public meta import Mathlib.Tactic.ToDual
 public import Mathlib.Algebra.Group.Equiv.Opposite
 public import Mathlib.Algebra.Group.TypeTags.Basic
 public import Mathlib.Data.Fintype.Sets
 public import Mathlib.Data.Multiset.Bind
-public meta import Mathlib.Tactic.ToDual
 
 /-!
 # Big operators

diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Gaps.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Gaps.lean
@@ -5,8 +5,8 @@ Authors: Yizheng Zhu
 -/
 module
 
-public import Mathlib.Order.Interval.Finset.Gaps
 public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
+public import Mathlib.Order.Interval.Finset.Gaps
 /-!
 # Sum of gaps
 

diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Pi.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Pi.lean
@@ -5,8 +5,8 @@ Authors: Johannes Hölzl
 -/
 module
 
-public import Mathlib.Data.Fintype.Pi
 public import Mathlib.Algebra.BigOperators.Group.Finset.Defs
+public import Mathlib.Data.Fintype.Pi
 
 
 /-!

diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Preimage.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Preimage.lean
@@ -5,8 +5,8 @@ Authors: Johannes Hölzl
 -/
 module
 
-public import Mathlib.Data.Finset.Preimage
 public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
+public import Mathlib.Data.Finset.Preimage
 
 /-!
 # Sums and products over preimages of finite sets.

diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Sigma.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Sigma.lean
@@ -5,8 +5,8 @@ Authors: Johannes Hölzl
 -/
 module
 
-public import Mathlib.Data.Finset.Sigma
 public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
+public import Mathlib.Data.Finset.Sigma
 
 /-!
 # Product and sums indexed by finite sets in sigma types.

diff --git a/Mathlib/Algebra/BigOperators/Group/List/Basic.lean b/Mathlib/Algebra/BigOperators/Group/List/Basic.lean
@@ -5,16 +5,16 @@ Authors: Johannes Hölzl, Floris van Doorn, Sébastien Gouëzel, Alex J. Best
 -/
 module
 
-public import Mathlib.Algebra.Group.Hom.Defs
 public import Mathlib.Algebra.BigOperators.Group.List.Defs
-public import Mathlib.Data.List.TakeDrop
-public import Mathlib.Data.List.Perm.Basic
 public import Mathlib.Algebra.Group.Basic
 public import Mathlib.Algebra.Group.Commute.Defs
-public import Mathlib.Algebra.Group.Nat.Defs
+public import Mathlib.Algebra.Group.Hom.Defs
 public import Mathlib.Algebra.Group.Int.Defs
-public import Mathlib.Order.Basic
+public import Mathlib.Algebra.Group.Nat.Defs
 public import Mathlib.Data.List.Basic
+public import Mathlib.Data.List.Perm.Basic
+public import Mathlib.Data.List.TakeDrop
+public import Mathlib.Order.Basic
 
 import Mathlib.Algebra.Divisibility.Basic
 

diff --git a/Mathlib/Algebra/BigOperators/Group/List/Defs.lean b/Mathlib/Algebra/BigOperators/Group/List/Defs.lean
@@ -5,8 +5,8 @@ Authors: Johannes Hölzl, Floris van Doorn, Sébastien Gouëzel, Alex J. Best
 -/
 module
 
-public import Mathlib.Algebra.Group.Monoid
 public import Batteries.Data.List.Lemmas
+public import Mathlib.Algebra.Group.Monoid
 
 /-!
 # Sums and products from lists

diff --git a/Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean b/Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
@@ -11,9 +11,9 @@ public import Mathlib.Algebra.Group.Int.Units
 public import Mathlib.Data.List.Dedup
 public import Mathlib.Data.List.Flatten
 public import Mathlib.Data.List.Pairwise
+public import Mathlib.Data.List.ProdSigma
 public import Mathlib.Data.List.Range
 public import Mathlib.Data.List.Rotate
-public import Mathlib.Data.List.ProdSigma
 
 /-!
 # Sums and products from lists

diff --git a/Mathlib/Algebra/BigOperators/NatAntidiagonal.lean b/Mathlib/Algebra/BigOperators/NatAntidiagonal.lean
@@ -5,8 +5,8 @@ Authors: Aaron Anderson
 -/
 module
 
-public import Mathlib.Data.Finset.NatAntidiagonal
 public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
+public import Mathlib.Data.Finset.NatAntidiagonal
 
 /-!
 # Big operators for `NatAntidiagonal`

diff --git a/Mathlib/Algebra/BigOperators/Option.lean b/Mathlib/Algebra/BigOperators/Option.lean
@@ -5,8 +5,8 @@ Authors: Yury Kudryashov
 -/
 module
 
-public import Mathlib.Data.Finset.Option
 public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
+public import Mathlib.Data.Finset.Option
 
 /-!
 # Lemmas about products and sums over finite sets in `Option α`

diff --git a/Mathlib/Algebra/BigOperators/Ring/List.lean b/Mathlib/Algebra/BigOperators/Ring/List.lean
@@ -5,11 +5,11 @@ Authors: Johannes Hölzl, Floris van Doorn, Sébastien Gouëzel, Alex J. Best
 -/
 module
 
+public import Mathlib.Algebra.BigOperators.Group.List.Basic
 public import Mathlib.Algebra.GroupWithZero.Commute
 public import Mathlib.Algebra.GroupWithZero.Divisibility
-public import Mathlib.Algebra.Ring.Divisibility.Basic
 public import Mathlib.Algebra.Ring.Commute
-public import Mathlib.Algebra.BigOperators.Group.List.Basic
+public import Mathlib.Algebra.Ring.Divisibility.Basic
 
 /-!
 # Big operators on a list in rings

diff --git a/Mathlib/Algebra/BigOperators/RingEquiv.lean b/Mathlib/Algebra/BigOperators/RingEquiv.lean
@@ -5,8 +5,8 @@ Authors: Johannes Hölzl, Callum Sutton, Yury Kudryashov
 -/
 module
 
-public import Mathlib.Algebra.Ring.Equiv
 public import Mathlib.Algebra.BigOperators.Group.Finset.Defs
+public import Mathlib.Algebra.Ring.Equiv
 
 import Mathlib.Algebra.Ring.Opposite
 

diff --git a/Mathlib/Algebra/Category/AlgCat/Basic.lean b/Mathlib/Algebra/Category/AlgCat/Basic.lean
@@ -5,9 +5,9 @@ Authors: Kim Morrison
 -/
 module
 
-public import Mathlib.Algebra.FreeAlgebra
-public import Mathlib.Algebra.Category.Ring.Basic
 public import Mathlib.Algebra.Category.ModuleCat.Basic
+public import Mathlib.Algebra.Category.Ring.Basic
+public import Mathlib.Algebra.FreeAlgebra
 
 /-!
 # Category instance for algebras over a commutative ring

diff --git a/Mathlib/Algebra/Category/BialgCat/Basic.lean b/Mathlib/Algebra/Category/BialgCat/Basic.lean
@@ -5,8 +5,8 @@ Authors: Amelia Livingston
 -/
 module
 
-public import Mathlib.Algebra.Category.CoalgCat.Basic
 public import Mathlib.Algebra.Category.AlgCat.Basic
+public import Mathlib.Algebra.Category.CoalgCat.Basic
 public import Mathlib.RingTheory.Bialgebra.Equiv
 
 /-!

diff --git a/Mathlib/Algebra/Category/Grp/Biproducts.lean b/Mathlib/Algebra/Category/Grp/Biproducts.lean
@@ -5,8 +5,8 @@ Authors: Kim Morrison
 -/
 module
 
-public import Mathlib.CategoryTheory.Preadditive.Biproducts
 public import Mathlib.Algebra.Category.Grp.Limits
+public import Mathlib.CategoryTheory.Preadditive.Biproducts
 
 /-!
 # The category of abelian groups has finite biproducts

diff --git a/Mathlib/Algebra/Category/Grp/EnoughInjectives.lean b/Mathlib/Algebra/Category/Grp/EnoughInjectives.lean
@@ -7,8 +7,8 @@ module
 
 public import Mathlib.Algebra.Module.CharacterModule
 
-import Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
 import Mathlib.Algebra.Category.Grp.EpiMono
+import Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
 
 /-!
 

diff --git a/Mathlib/Algebra/Category/Grp/Shrink.lean b/Mathlib/Algebra/Category/Grp/Shrink.lean
@@ -6,8 +6,8 @@ Authors: Christian Merten
 module
 
 public import Mathlib.Algebra.Category.Grp.Basic
-public import Mathlib.CategoryTheory.ShrinkYoneda
 public import Mathlib.Algebra.Group.Shrink
+public import Mathlib.CategoryTheory.ShrinkYoneda
 
 /-!
 # Shrinking a functor to `GrpCat`

diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean
@@ -5,8 +5,8 @@ Authors: Robert A. Spencer, Markus Himmel
 -/
 module
 
-public import Mathlib.Algebra.Category.ModuleCat.Semi
 public import Mathlib.Algebra.Category.Grp.Preadditive
+public import Mathlib.Algebra.Category.ModuleCat.Semi
 public import Mathlib.CategoryTheory.Linear.Basic
 public import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
 public import Mathlib.LinearAlgebra.BilinearMap

diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
@@ -5,10 +5,10 @@ Authors: Jujian Zhang
 -/
 module
 
-public import Mathlib.Algebra.Category.ModuleCat.EpiMono
+public import Mathlib.Algebra.Algebra.RestrictScalars
 public import Mathlib.Algebra.Category.ModuleCat.Colimits
+public import Mathlib.Algebra.Category.ModuleCat.EpiMono
 public import Mathlib.Algebra.Category.ModuleCat.Limits
-public import Mathlib.Algebra.Algebra.RestrictScalars
 public import Mathlib.CategoryTheory.Adjunction.Mates
 public import Mathlib.CategoryTheory.Linear.LinearFunctor
 public import Mathlib.LinearAlgebra.TensorProduct.Tower

diff --git a/Mathlib/Algebra/Category/ModuleCat/Colimits.lean b/Mathlib/Algebra/Category/ModuleCat/Colimits.lean
@@ -5,8 +5,8 @@ Authors: Kim Morrison, Joël Riou
 -/
 module
 
-public import Mathlib.Algebra.Category.ModuleCat.Basic
 public import Mathlib.Algebra.Category.Grp.Colimits
+public import Mathlib.Algebra.Category.ModuleCat.Basic
 public import Mathlib.LinearAlgebra.DFinsupp
 
 /-!

diff --git a/Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean b/Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean
@@ -5,8 +5,8 @@ Authors: Joël Riou
 -/
 module
 
-public import Mathlib.Algebra.Category.ModuleCat.Presheaf.OfCommRing
 public import Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
+public import Mathlib.Algebra.Category.ModuleCat.Presheaf.OfCommRing
 
 /-!
 # The presheaf of differentials of a presheaf of modules

diff --git a/Mathlib/Algebra/Category/ModuleCat/EpiMono.lean b/Mathlib/Algebra/Category/ModuleCat/EpiMono.lean
@@ -5,9 +5,9 @@ Authors: Kim Morrison
 -/
 module
 
-public import Mathlib.LinearAlgebra.Quotient.Basic
 public import Mathlib.Algebra.Category.ModuleCat.Basic
 public import Mathlib.CategoryTheory.ConcreteCategory.EpiMono
+public import Mathlib.LinearAlgebra.Quotient.Basic
 
 /-!
 # Monomorphisms in `Module R`

diff --git a/Mathlib/Algebra/Category/ModuleCat/ExteriorPower.lean b/Mathlib/Algebra/Category/ModuleCat/ExteriorPower.lean
@@ -5,8 +5,8 @@ Authors: Joël Riou
 -/
 module
 
-public import Mathlib.LinearAlgebra.ExteriorPower.Basic
 public import Mathlib.Algebra.Category.ModuleCat.Basic
+public import Mathlib.LinearAlgebra.ExteriorPower.Basic
 
 /-!
 # The exterior powers as functors on the category of modules

diff --git a/Mathlib/Algebra/Category/ModuleCat/Free.lean b/Mathlib/Algebra/Category/ModuleCat/Free.lean
@@ -5,8 +5,8 @@ Authors: Dagur Asgeirsson
 -/
 module
 
-public import Mathlib.LinearAlgebra.Dimension.Free
 public import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
+public import Mathlib.LinearAlgebra.Dimension.Free
 
 /-!
 # Exact sequences with free modules

diff --git a/Mathlib/Algebra/Category/ModuleCat/Injective.lean b/Mathlib/Algebra/Category/ModuleCat/Injective.lean
@@ -5,9 +5,9 @@ Authors: Jujian Zhang
 -/
 module
 
+public import Mathlib.Algebra.Category.ModuleCat.EpiMono
 public import Mathlib.Algebra.Module.Injective
 public import Mathlib.CategoryTheory.Preadditive.Injective.Basic
-public import Mathlib.Algebra.Category.ModuleCat.EpiMono
 
 /-!
 # Injective objects in the category of $R$-modules

diff --git a/Mathlib/Algebra/Category/ModuleCat/Limits.lean b/Mathlib/Algebra/Category/ModuleCat/Limits.lean
@@ -5,8 +5,8 @@ Authors: Kim Morrison
 -/
 module
 
-public import Mathlib.Algebra.Category.ModuleCat.Basic
 public import Mathlib.Algebra.Category.Grp.Limits
+public import Mathlib.Algebra.Category.ModuleCat.Basic
 public import Mathlib.Algebra.Colimit.Module
 public import Mathlib.Algebra.Module.Shrink -- shake: keep (Module R (Shrink.{w, max v w} ↥(sectionsSubmodule F))), cf. lean#13417
 

diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
@@ -6,9 +6,9 @@ Authors: Kevin Buzzard, Kim Morrison, Jakob von Raumer
 module
 
 public import Mathlib.Algebra.Category.ModuleCat.Basic
-public import Mathlib.LinearAlgebra.TensorProduct.Associator
 public import Mathlib.CategoryTheory.Monoidal.Linear
 public import Mathlib.CategoryTheory.Monoidal.Transport
+public import Mathlib.LinearAlgebra.TensorProduct.Associator
 
 /-!
 # The monoidal category structure on R-modules

diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean
@@ -5,9 +5,9 @@ Authors: Kevin Buzzard, Kim Morrison, Jakob von Raumer
 -/
 module
 
-public import Mathlib.CategoryTheory.Monoidal.Closed.Basic
-public import Mathlib.CategoryTheory.Linear.Yoneda
 public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
+public import Mathlib.CategoryTheory.Linear.Yoneda
+public import Mathlib.CategoryTheory.Monoidal.Closed.Basic
 
 /-!
 # The monoidal closed structure on `Module R`.

diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean
@@ -5,8 +5,8 @@ Authors: Kevin Buzzard, Kim Morrison, Jakob von Raumer
 -/
 module
 
-public import Mathlib.CategoryTheory.Monoidal.Braided.Basic
 public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
+public import Mathlib.CategoryTheory.Monoidal.Braided.Basic
 
 /-!
 # The symmetric monoidal structure on `Module R`.

diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean
@@ -5,8 +5,8 @@ Authors: Johan Commelin, Joel Riou
 -/
 module
 
-public import Mathlib.Algebra.Category.ModuleCat.Presheaf
 public import Mathlib.Algebra.Category.ModuleCat.Adjunctions
+public import Mathlib.Algebra.Category.ModuleCat.Presheaf
 
 /-!
 # The free presheaf of modules on a presheaf of sets

diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean
@@ -5,8 +5,8 @@ Authors: Dagur Asgeirsson, Jack McKoen, Joël Riou
 -/
 module
 
-public import Mathlib.Algebra.Category.ModuleCat.Presheaf.OfCommRing
 public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
+public import Mathlib.Algebra.Category.ModuleCat.Presheaf.OfCommRing
 
 /-!
 # The monoidal category structure on presheaves of modules
-Original file line number
+Diff line change
@@ Expand Up / @@ -5,8 +5,8 @@ Authors: Johannes Hölzl @@
     -/
     module
-    public import Mathlib.Data.Fintype.Pi
     public import Mathlib.Algebra.BigOperators.Group.Finset.Defs
+    public import Mathlib.Data.Fintype.Pi
     /-!
@@ Expand Down @@