Commit 2025-12-23 19:14 26440c82

View on Github →

fix: whitespace formatting (#33234) Discovered by extended the commandStart linter to proof bodies in #30658. Correct the pretty-printing of the introv tactic.

Estimated changes

Modified Mathlib/Algebra/GradedMonoid.lean

Modified Mathlib/Algebra/Lie/Basic.lean

Modified Mathlib/Algebra/Order/BigOperators/Expect.lean

Modified Mathlib/Algebra/Polynomial/Coeff.lean

Modified Mathlib/Combinatorics/Enumerative/Bell.lean

Modified Mathlib/Data/Nat/BitIndices.lean

modified theorem Nat.bitIndices_two_pow

modified theorem Nat.two_pow_le_of_mem_bitIndices

Modified Mathlib/Data/Nat/Digits/Defs.lean

Modified Mathlib/Data/Real/Basic.lean

Modified Mathlib/Data/Set/Insert.lean

modified theorem Set.powerset_singleton

Modified Mathlib/Data/Sym/Basic.lean

Modified Mathlib/NumberTheory/ClassNumber/AdmissibleAbsoluteValue.lean

Modified Mathlib/NumberTheory/Padics/PadicVal/Basic.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

modified theorem Cardinal.le_powerlt

Modified Mathlib/Tactic/Basic.lean