Commit 2025-12-17 21:56 0a79887f

View on Github →

chore(misc): fix whitespace (#33004) Found by extending the commandStart linter to proof bodies.

Estimated changes

Modified Mathlib/Condensed/Basic.lean

Modified Mathlib/Condensed/Functors.lean

Modified Mathlib/Condensed/Light/TopCatAdjunction.lean

Modified Mathlib/Condensed/TopComparison.lean

Modified Mathlib/Deprecated/Sort.lean

modified theorem List.Sorted.filter

modified theorem List.sorted_singleton

Modified Mathlib/Dynamics/Ergodic/Conservative.lean

Modified Mathlib/Dynamics/Ergodic/MeasurePreserving.lean

Modified Mathlib/Dynamics/PeriodicPts/Defs.lean

Modified Mathlib/Dynamics/PeriodicPts/Lemmas.lean

Modified Mathlib/Probability/ConditionalProbability.lean

modified theorem ProbabilityTheory.cond_apply'

modified theorem ProbabilityTheory.cond_apply_self

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Cardinal/CountableCover.lean

Modified Mathlib/SetTheory/Cardinal/Subfield.lean

Modified Mathlib/SetTheory/Cardinal/ToNat.lean

Modified Mathlib/SetTheory/Lists.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean