felixpernegger · Jul 24, 2026 · Jul 24, 2026 · Jul 24, 2026 · Jul 24, 2026 · Jul 25, 2026
diff --git a/Mathlib/Algebra/AddConstMap/Basic.lean b/Mathlib/Algebra/AddConstMap/Basic.lean
@@ -9,6 +9,7 @@ public import Mathlib.Algebra.Group.Action.Pi
 public import Mathlib.Algebra.Group.End
 public import Mathlib.Algebra.Module.NatInt
 public import Mathlib.Algebra.Order.Archimedean.Basic
+
 import Mathlib.Algebra.Order.Group.Basic
 
 /-!

diff --git a/Mathlib/Algebra/AffineMonoid/Embedding.lean b/Mathlib/Algebra/AffineMonoid/Embedding.lean
@@ -9,12 +9,12 @@ public import Mathlib.GroupTheory.Finiteness
 public import Mathlib.GroupTheory.FreeAbelianGroup
 public import Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
 public import Mathlib.LinearAlgebra.Dimension.Finrank
+public import Mathlib.LinearAlgebra.Dimension.Free
 
 import Mathlib.Algebra.EuclideanDomain.Int
 import Mathlib.GroupTheory.MonoidLocalization.Finite
 import Mathlib.LinearAlgebra.Dimension.Free
 import Mathlib.LinearAlgebra.FreeModule.PID
-public import Mathlib.LinearAlgebra.Dimension.Free
 
 /-!
 # Affine monoids embed into `ℤⁿ`

diff --git a/Mathlib/Algebra/CharP/MixedCharZero.lean b/Mathlib/Algebra/CharP/MixedCharZero.lean
@@ -11,6 +11,7 @@ public import Mathlib.Algebra.IsPrimePow
 public import Mathlib.RingTheory.Ideal.Maximal
 public import Mathlib.RingTheory.Ideal.Quotient.Defs
 public import Mathlib.RingTheory.LocalRing.Defs
+
 import Mathlib.Algebra.CharP.LocalRing
 
 /-!

diff --git a/Mathlib/Algebra/Group/ModEq.lean b/Mathlib/Algebra/Group/ModEq.lean
@@ -6,6 +6,7 @@ Authors: Yaël Dillies
 module
 
 public import Mathlib.Algebra.Group.Hom.Defs
+
 import Mathlib.Algebra.Group.Torsion
 import Mathlib.Tactic.TermCongr
 import Mathlib.Tactic.Use

diff --git a/Mathlib/Algebra/Order/Antidiag/FinsuppEquiv.lean b/Mathlib/Algebra/Order/Antidiag/FinsuppEquiv.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Order.Antidiag.Finsupp
 public import Mathlib.Data.Finsupp.Basic
 public import Mathlib.Data.Finsupp.Multiset
+
 import Mathlib.Data.Sym.Card
 
 /-!

diff --git a/Mathlib/Algebra/Order/Archimedean/Real/Hom.lean b/Mathlib/Algebra/Order/Archimedean/Real/Hom.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Order.Archimedean.Hom  -- shake: keep (Subsingleton (ℝ →+*o ℝ)), cf. lean#13417
 public import Mathlib.Analysis.Real.Sqrt
+
 import Mathlib.Algebra.Order.CompleteField
 
 /-!

diff --git a/Mathlib/Algebra/Order/GroupWithZero/Basic.lean b/Mathlib/Algebra/Order/GroupWithZero/Basic.lean
@@ -11,9 +11,9 @@ public import Mathlib.Algebra.Order.GroupWithZero.Defs
 public import Mathlib.Algebra.Order.ZeroLEOne
 public import Mathlib.Tactic.Bound.Attribute
 public import Mathlib.Tactic.Monotonicity.Attr
+public import Mathlib.Data.Int.Order.Basic
 
 import Mathlib.Data.Set.Function
-public import Mathlib.Data.Int.Order.Basic
 
 /-!
 # Lemmas on the monotone multiplication typeclasses

diff --git a/Mathlib/Algebra/Order/Ring/Interval.lean b/Mathlib/Algebra/Order/Ring/Interval.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Order.Ring.Defs
 public import Mathlib.Data.Int.Interval
+
 import Mathlib.Algebra.Order.Ring.Cast
 
 /-! # Intervals of integers in strict ordered rings

diff --git a/Mathlib/Algebra/Order/ToIntervalMod.lean b/Mathlib/Algebra/Order/ToIntervalMod.lean
@@ -10,6 +10,7 @@ public import Mathlib.Algebra.Order.Archimedean.Basic
 public import Mathlib.Algebra.Ring.Periodic
 public import Mathlib.Data.Int.SuccPred
 public import Mathlib.Order.Circular
+
 import Mathlib.Algebra.Order.Interval.Set.Group
 import Mathlib.GroupTheory.QuotientGroup.ModEq
 

diff --git a/Mathlib/Algebra/Polynomial/RingDivision.lean b/Mathlib/Algebra/Polynomial/RingDivision.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Polynomial.AlgebraMap
 public import Mathlib.Algebra.Polynomial.Div
 public import Mathlib.RingTheory.Coprime.Basic
+
 import Mathlib.Tactic.ComputeDegree
 
 /-!

diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplex.lean b/Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplex.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
 public import Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
+
 import Mathlib.Order.Fin.InsertNth
 import Mathlib.Order.Fin.Prod
 import Mathlib.Order.Preorder.Finite

diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean b/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean
@@ -13,6 +13,7 @@ public import Mathlib.Logic.Equiv.Fin.Basic
 public import Mathlib.Order.Fin.Finset
 public import Mathlib.Order.Fin.SuccAboveOrderIso
 public import Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
+
 import Mathlib.Order.Preorder.Finite
 
 /-!

diff --git a/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean b/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
@@ -6,6 +6,7 @@ Authors: Anatole Dedecker
 module
 
 public import Mathlib.Analysis.Normed.Module.Basic
+
 import Mathlib.Analysis.Asymptotics.Theta
 public import Mathlib.Analysis.Asymptotics.Defs
 

diff --git a/Mathlib/Analysis/Asymptotics/TVS.lean b/Mathlib/Analysis/Asymptotics/TVS.lean
@@ -10,9 +10,10 @@ public import Mathlib.Analysis.LocallyConvex.BalancedCoreHull
 public import Mathlib.Analysis.Normed.Module.Seminorm.Basic
 public import Mathlib.Analysis.Asymptotics.Defs
 public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
-import Mathlib.Tactic.Peel
 public import Mathlib.Topology.Instances.ENNReal.Lemmas
 
+import Mathlib.Tactic.Peel
+
 /-!
 # Asymptotics in a Topological Vector Space
 

diff --git a/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean b/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
@@ -9,6 +9,7 @@ public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
 public import Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
 public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
 public import Mathlib.Topology.ApproximateUnit
+
 import Mathlib.Algebra.Order.Interval.Set.Group
 
 /-! # Nonnegative contractions in a C⋆-algebra form an approximate unit

diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Projection.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Projection.lean
@@ -6,6 +6,7 @@ Authors: Monica Omar
 module
 
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
+
 import Mathlib.FieldTheory.IsAlgClosed.Spectrum
 
 /-! # Continuous functional calculus and projections

diff --git a/Mathlib/Analysis/CStarAlgebra/Fuglede.lean b/Mathlib/Analysis/CStarAlgebra/Fuglede.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Analysis.Normed.Algebra.Exponential
 public import Mathlib.Analysis.CStarAlgebra.Classes
+
 import Mathlib.Analysis.CStarAlgebra.Exponential
 import Mathlib.Analysis.CStarAlgebra.Unitization
 import Mathlib.Analysis.Complex.Liouville

diff --git a/Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean b/Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean
@@ -9,6 +9,7 @@ public import Mathlib.Analysis.CStarAlgebra.Module.Defs
 public import Mathlib.Analysis.CStarAlgebra.Module.Synonym
 public import Mathlib.Analysis.InnerProductSpace.Basic
 public import Mathlib.Topology.MetricSpace.Bilipschitz
+
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
 
 /-! # Constructions of Hilbert C⋆-modules

diff --git a/Mathlib/Analysis/CStarAlgebra/Module/Defs.lean b/Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
@@ -5,14 +5,15 @@ Authors: Frédéric Dupuis
 -/
 module
 
-public import Mathlib.Analysis.InnerProductSpace.Defs
-import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
 public import Mathlib.Analysis.CStarAlgebra.Classes
+public import Mathlib.Analysis.InnerProductSpace.Defs
 public import Mathlib.Analysis.Normed.Operator.Bilinear
 public import Mathlib.Analysis.SpecialFunctions.Bernstein
 public import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 public import Mathlib.Tactic.NormNum.GCD
 
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
+
 /-!
 # Hilbert C⋆-modules
 

diff --git a/Mathlib/Analysis/Calculus/ContDiff/Operations.lean b/Mathlib/Analysis/Calculus/ContDiff/Operations.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Analysis.Calculus.ContDiff.Comp
 public import Mathlib.Analysis.Calculus.Deriv.Inverse
 public import Mathlib.Topology.OpenPartialHomeomorph.IsImage
+
 import Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
 
 /-!

diff --git a/Mathlib/Analysis/Calculus/Deriv/Inverse.lean b/Mathlib/Analysis/Calculus/Deriv/Inverse.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Analysis.Calculus.Deriv.Comp
 public import Mathlib.Analysis.Calculus.FDeriv.Equiv
+
 import Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
 
 /-!

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean
@@ -9,6 +9,7 @@ public import Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
 public import Mathlib.Analysis.Calculus.FDeriv.Defs
 public import Mathlib.Analysis.Normed.Operator.Asymptotics
 public import Mathlib.Analysis.Calculus.TangentCone.Basic
+
 import Mathlib.Analysis.Asymptotics.Lemmas
 import Mathlib.Analysis.Calculus.TangentCone.DimOne
 

diff --git a/Mathlib/Analysis/Calculus/FDeriv/OfCompLeft.lean b/Mathlib/Analysis/Calculus/FDeriv/OfCompLeft.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Analysis.Calculus.FDeriv.Basic
 public import Mathlib.Topology.OpenPartialHomeomorph.Defs
+
 import Mathlib.Topology.OpenPartialHomeomorph.Continuity
 
 /-!

diff --git a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean
@@ -6,6 +6,7 @@ Authors: Yury Kudryashov, Sébastien Gouëzel
 module
 
 public import Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
+
 import Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
 public import Mathlib.Algebra.Order.Field.Power
 public import Mathlib.Analysis.Calculus.FDeriv.Congr

diff --git a/Mathlib/Analysis/Calculus/TangentCone/DimOne.lean b/Mathlib/Analysis/Calculus/TangentCone/DimOne.lean
@@ -6,9 +6,10 @@ Authors: Sébastien Gouëzel, Yury Kudryashov
 module
 
 public import Mathlib.Analysis.Calculus.TangentCone.Defs
+public import Mathlib.Analysis.Normed.Field.Basic
+
 import Mathlib.Analysis.Calculus.TangentCone.Basic
 import Mathlib.Analysis.Normed.Group.Uniform
-public import Mathlib.Analysis.Normed.Field.Basic
 
 /-!
 # Unique differentiability property of a set in the base field

diff --git a/Mathlib/Analysis/Calculus/TangentCone/Pi.lean b/Mathlib/Analysis/Calculus/TangentCone/Pi.lean
@@ -6,6 +6,7 @@ Authors: Sébastien Gouëzel
 module
 
 public import Mathlib.Analysis.Calculus.TangentCone.Basic
+
 import Mathlib.Topology.Algebra.Module.Basic
 
 /-!

diff --git a/Mathlib/Analysis/Calculus/TangentCone/Prod.lean b/Mathlib/Analysis/Calculus/TangentCone/Prod.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Analysis.Calculus.TangentCone.Defs
 public import Mathlib.LinearAlgebra.Prod
 public import Mathlib.Topology.Algebra.Monoid
+
 import Mathlib.Analysis.Calculus.TangentCone.Basic
 
 /-!

diff --git a/Mathlib/Analysis/Calculus/TangentCone/Seq.lean b/Mathlib/Analysis/Calculus/TangentCone/Seq.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Analysis.Calculus.TangentCone.Basic
 public import Mathlib.Topology.Algebra.MulAction
 public import Mathlib.Analysis.Normed.Module.Basic
+
 import Mathlib.Analysis.SpecificLimits.Normed
 
 /-!

diff --git a/Mathlib/Analysis/Complex/BranchLogRoot.lean b/Mathlib/Analysis/Complex/BranchLogRoot.lean
@@ -10,6 +10,7 @@ public import Mathlib.Analysis.Complex.Basic
 public import Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
 public import Mathlib.Analysis.Complex.Exponential
 public import Mathlib.Analysis.Complex.UnitDisc.Basic
+
 import Mathlib.Analysis.Complex.CoveringMap
 import Mathlib.Topology.Homotopy.Lifting
 

diff --git a/Mathlib/Analysis/Complex/Isometry.lean b/Mathlib/Analysis/Complex/Isometry.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Analysis.Complex.Circle
 public import Mathlib.LinearAlgebra.Determinant
 public import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
+
 import Mathlib.Tactic.SuppressCompilation
 
 /-!

diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/FixedPoints.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/FixedPoints.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
 public import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
+
 import Mathlib.Algebra.QuadraticDiscriminant
 
 /-!

diff --git a/Mathlib/Analysis/Convex/FunctionTopology.lean b/Mathlib/Analysis/Convex/FunctionTopology.lean
@@ -6,10 +6,11 @@ Authors: Frédéric Dupuis
 module
 
 public import Mathlib.Analysis.Convex.Function
-import Mathlib.Topology.Algebra.Monoid
 public import Mathlib.Topology.Algebra.ConstMulAction
 public import Mathlib.Topology.Algebra.Monoid.Defs
 
+import Mathlib.Topology.Algebra.Monoid
+
 /-!
 # Topological properties of the set of convex/concave functions
 

diff --git a/Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean b/Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
@@ -10,6 +10,7 @@ public import Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
 public import Mathlib.Analysis.SpecialFunctions.Complex.Circle
 public import Mathlib.GroupTheory.FiniteAbelian.Basic
 public import Mathlib.Topology.Instances.AddCircle.Real
+
 import Mathlib.Algebra.Field.ModEq
 
 /-!

diff --git a/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean b/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Analysis.InnerProductSpace.Basic
 public import Mathlib.Analysis.InnerProductSpace.PiL2
 public import Mathlib.LinearAlgebra.Matrix.PosDef
+
 import Mathlib.Analysis.Matrix.Order
 
 /-! # Gram Matrices

diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Analysis.InnerProductSpace.Adjoint
 public import Mathlib.RingTheory.TensorProduct.Finite
+
 import Mathlib.Analysis.InnerProductSpace.GramMatrix
 import Mathlib.Analysis.InnerProductSpace.Positive
 import Mathlib.Algebra.Order.Star.Real

diff --git a/Mathlib/Analysis/Matrix/Hermitian.lean b/Mathlib/Analysis/Matrix/Hermitian.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Analysis.InnerProductSpace.PiL2
 public import Mathlib.LinearAlgebra.Matrix.Hermitian
+
 import Mathlib.Analysis.InnerProductSpace.Adjoint
 
 /-!

diff --git a/Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean b/Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Analysis.Normed.Algebra.Spectrum
 public import Mathlib.Analysis.Calculus.Deriv.Basic
 public import Mathlib.Analysis.Normed.Operator.Mul
+
 import Mathlib.Analysis.Complex.Polynomial.Basic
 import Mathlib.Analysis.Analytic.RadiusLiminf
 

diff --git a/Mathlib/Analysis/Normed/Field/Lemmas.lean b/Mathlib/Analysis/Normed/Field/Lemmas.lean
@@ -9,6 +9,7 @@ public import Mathlib.Analysis.Normed.Field.Basic
 public import Mathlib.Analysis.Normed.Group.Rat
 public import Mathlib.Analysis.Normed.Ring.Lemmas
 public import Mathlib.Topology.MetricSpace.DilationEquiv
+
 import Mathlib.Analysis.Normed.MulAction
 
 /-!

diff --git a/Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean b/Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean
@@ -6,6 +6,7 @@ Authors: Sophie Morel
 module
 
 public import Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
+
 import Mathlib.LinearAlgebra.Isomorphisms
 
 /-!

diff --git a/Mathlib/Analysis/RCLike/ContinuousMap.lean b/Mathlib/Analysis/RCLike/ContinuousMap.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Analysis.RCLike.Basic
 public import Mathlib.Topology.ContinuousMap.Compact
 public import Mathlib.Topology.ContinuousMap.Ordered
+
 import Mathlib.Topology.ContinuousMap.Units
 
 /-! # Mapping `C(X, ℝ)` to `C(X, 𝕜)` and back

diff --git a/Mathlib/Analysis/RCLike/Sqrt.lean b/Mathlib/Analysis/RCLike/Sqrt.lean
@@ -6,9 +6,9 @@ Authors: Monica Omar
 module
 
 public import Mathlib.Analysis.SpecialFunctions.Pow.Complex
+public import Mathlib.LinearAlgebra.Basis.VectorSpace
 
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
-public import Mathlib.LinearAlgebra.Basis.VectorSpace
 
 /-!
 # Square root on `RCLike`

diff --git a/Mathlib/Analysis/SpecialFunctions/Choose.lean b/Mathlib/Analysis/SpecialFunctions/Choose.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Analysis.SpecificLimits.Basic
 public import Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
 public import Mathlib.Data.Nat.Cast.Field
+
 import Mathlib.Analysis.Asymptotics.Theta
 
 /-!

diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean
@@ -6,6 +6,7 @@ Authors: Jeremy Tan
 module
 
 public import Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
+
 import Mathlib.Algebra.Order.Interval.Set.Group
 
 /-!

diff --git a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Abs.lean b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Abs.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
 public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
+
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
 import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
 

diff --git a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog/Basic.lean b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog/Basic.lean
@@ -10,6 +10,7 @@ public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
 public import Mathlib.Topology.ContinuousMap.ContinuousSqrt
 public import Mathlib.Analysis.SpecialFunctions.Log.Basic
+
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
 
 /-!
-Original file line number
+Diff line change
@@ Expand Up / @@ -7,6 +7,7 @@ module @@
     public import Mathlib.Algebra.Order.Archimedean.Hom  -- shake: keep (Subsingleton (ℝ →+*o ℝ)), cf. lean#13417
     public import Mathlib.Analysis.Real.Sqrt
     import Mathlib.Algebra.Order.CompleteField
     /-!
@@ Expand Down @@