Commit 2025-12-15 15:28 f385661b

View on Github →

chore(SetTheory): fix whitespace (#32899) Extracted from https://github.com/leanprover-community/mathlib4/pull/30658. Found by extending the commandStart linter to proof bodies.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Arithmetic.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Cardinal/CountableCover.lean

Modified Mathlib/SetTheory/Cardinal/ENat.lean

Modified Mathlib/SetTheory/Cardinal/Order.lean

Modified Mathlib/SetTheory/Cardinal/Regular.lean

Modified Mathlib/SetTheory/Cardinal/Subfield.lean

Modified Mathlib/SetTheory/Game/Ordinal.lean

modified theorem Ordinal.toPGame_leftMoves

Modified Mathlib/SetTheory/Ordinal/Basic.lean

modified theorem Cardinal.lift_ord

modified theorem Ordinal.card_univ