Commit 2025-10-21 20:48 1f2d45d9

View on Github →

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

Estimated changes

Modified Mathlib/Order/Bounds/Image.lean

Modified Mathlib/Order/Filter/Cocardinal.lean

Modified Mathlib/Order/Heyting/Basic.lean

Modified Mathlib/Order/KonigLemma.lean

Modified Mathlib/Order/Monotone/Basic.lean

modified theorem StrictMono.add_le_nat

Modified Mathlib/Order/PiLex.lean

Modified Mathlib/Order/RelClasses.lean

Modified Mathlib/Order/SetNotation.lean

modified theorem Set.sSup_eq_sUnion

Modified Mathlib/Order/WithBot.lean

modified theorem WithTop.coe_untopD_le