Commit 2025-06-04 14:26 27268254

View on Github →

chore: more whitespace fixes (#25437) Found by the linter in #24465.

Estimated changes

Modified Mathlib/Algebra/Group/Action/Sigma.lean

Modified Mathlib/Algebra/Group/Ext.lean

Modified Mathlib/Algebra/Group/Submonoid/MulAction.lean

Modified Mathlib/Algebra/Ring/InjSurj.lean

Modified Mathlib/Combinatorics/Quiver/ConnectedComponent.lean

Modified Mathlib/Control/Monad/Writer.lean

Modified Mathlib/Data/Set/Function.lean

Modified Mathlib/Data/Set/Lattice.lean

modified def Set.sigmaToiUnion

Modified Mathlib/Data/Set/Lattice/Image.lean

modified theorem Set.image2_sInter_left_subset

Modified Mathlib/Data/Set/Sigma.lean

modified theorem Set.exists_sigma_iff

Modified Mathlib/Data/Sigma/Basic.lean

modified theorem PSigma.«forall»

modified theorem Sigma.«exists»

modified theorem Sigma.«forall»

Modified Mathlib/Data/Sigma/Order.lean

modified theorem Sigma.le_def

modified theorem Sigma.lt_def

Modified Mathlib/GroupTheory/GroupAction/Hom.lean

modified structure AddActionHom

Modified Mathlib/Order/Basic.lean

modified def AsLinearOrder

Modified Mathlib/Order/Heyting/Hom.lean

Modified Mathlib/Tactic/CategoryTheory/Coherence/Datatypes.lean

modified def Mathlib.Tactic.BicategoryLike.mkContext

Modified Mathlib/Tactic/CategoryTheory/Coherence/PureCoherence.lean

modified def Mathlib.Tactic.BicategoryLike.normalize

Modified Mathlib/Tactic/Explode/Datatypes.lean

Modified Mathlib/Tactic/FunProp/Core.lean

Modified Mathlib/Tactic/FunProp/StateList.lean

Modified Mathlib/Tactic/FunProp/Theorems.lean

Modified Mathlib/Tactic/TFAE.lean

Modified Mathlib/Tactic/WLOG.lean

Modified Mathlib/Topology/Compactness/CompactlyCoherentSpace.lean