Commit 2025-10-20 13:51 49649595

View on Github →

style: fix whitespace (#30724) Found by extending the commandStart linter to proof bodies. Extracted from #30658.

Estimated changes

Modified Mathlib/Algebra/AddConstMap/Equiv.lean

Modified Mathlib/Algebra/Category/ModuleCat/Basic.lean

Modified Mathlib/Algebra/Category/MonCat/Limits.lean

Modified Mathlib/CategoryTheory/Category/ULift.lean

added def CategoryTheory.ULiftHom.{w,

deleted def CategoryTheory.ULiftHom.{w,u}

Modified Mathlib/CategoryTheory/Comma/Over/Basic.lean

modified def CategoryTheory.Under.mapFunctor

Modified Mathlib/CategoryTheory/Filtered/Basic.lean

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean

Modified Mathlib/CategoryTheory/Limits/Types/Colimits.lean

Modified Mathlib/CategoryTheory/Monoidal/Functor.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Factorization.lean

Modified Mathlib/CategoryTheory/Skeletal.lean

Modified Mathlib/Data/Finset/Lattice/Fold.lean

Modified Mathlib/Data/Set/Monotone.lean

Modified Mathlib/GroupTheory/Congruence/Hom.lean

Modified Mathlib/GroupTheory/NoncommPiCoprod.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Basic.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Factors.lean

Modified Mathlib/GroupTheory/Perm/Fin.lean

Modified Mathlib/GroupTheory/Perm/Finite.lean

Modified Mathlib/LinearAlgebra/BilinearMap.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

Modified Mathlib/Probability/ProbabilityMassFunction/Binomial.lean

Modified Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean

Modified Mathlib/RingTheory/DedekindDomain/Instances.lean

Modified Mathlib/RingTheory/DualNumber.lean

Modified Mathlib/RingTheory/Etale/Field.lean

Modified Mathlib/RingTheory/LaurentSeries.lean

Modified Mathlib/RingTheory/LocalProperties/Semilocal.lean

Modified Mathlib/RingTheory/Polynomial/Eisenstein/Distinguished.lean

Modified Mathlib/RingTheory/TwoSidedIdeal/Lattice.lean

modified theorem TwoSidedIdeal.mem_top

Modified Mathlib/RingTheory/WittVector/Frobenius.lean

Modified Mathlib/Topology/Algebra/ClopenNhdofOne.lean

Modified Mathlib/Topology/CWComplex/Classical/Subcomplex.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling/Successor.lean

Modified Mathlib/Topology/ContinuousMap/Bounded/ArzelaAscoli.lean

Modified Mathlib/Topology/Covering.lean

Modified Mathlib/Topology/EMetricSpace/PairReduction.lean

Modified Mathlib/Topology/Order/HullKernel.lean

Modified Mathlib/Topology/UniformSpace/Ascoli.lean