Commit 2025-03-10 22:05 cf6f2de6

View on Github →

chore: more whitespace fixes (#22808) Found by #22760.

Estimated changes

Modified Mathlib/Data/DFinsupp/BigOperators.lean

Modified Mathlib/Data/Finset/Preimage.lean

modified theorem Finset.sigma_image_fst_preimage_mk

modified theorem Finset.sigma_preimage_mk

modified theorem Finset.sigma_preimage_mk_of_subset

Modified Mathlib/Data/Finset/Sigma.lean

modified theorem Finset.mem_sigma

modified theorem Finset.sigmaLift_mono

modified theorem Finset.sigma_eq_biUnion

Modified Mathlib/Data/Set/Constructions.lean

modified theorem FiniteInter.mk₂

Modified Mathlib/Data/Sym/Basic.lean

modified def Sym.filterNe

modified theorem Sym.filter_ne_fill

modified theorem Sym.sigma_sub_ext

Modified Mathlib/Data/W/Basic.lean

modified theorem WType.elim_injective

Modified Mathlib/GroupTheory/Perm/Sign.lean

modified theorem Equiv.Perm.mem_finPairsLT

Modified Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean

modified theorem Ordinal.lift_down

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

Modified Mathlib/Tactic/IntervalCases.lean

modified theorem Mathlib.Tactic.IntervalCases.of_le_left

modified theorem Mathlib.Tactic.IntervalCases.of_le_right

modified theorem Mathlib.Tactic.IntervalCases.of_lt_left

modified theorem Mathlib.Tactic.IntervalCases.of_lt_right

modified theorem Mathlib.Tactic.IntervalCases.of_not_le_left

modified theorem Mathlib.Tactic.IntervalCases.of_not_le_right

modified theorem Mathlib.Tactic.IntervalCases.of_not_lt_left

modified theorem Mathlib.Tactic.IntervalCases.of_not_lt_right

Modified Mathlib/Tactic/LinearCombination/Lemmas.lean

modified theorem Mathlib.Tactic.LinearCombination.add_eq_eq

modified theorem Mathlib.Tactic.LinearCombination.eq_of_add_pow

modified theorem Mathlib.Tactic.LinearCombination.eq_of_eq

modified theorem Mathlib.Tactic.LinearCombination.le_of_eq

modified theorem Mathlib.Tactic.LinearCombination.le_of_le

modified theorem Mathlib.Tactic.LinearCombination.le_of_lt

modified theorem Mathlib.Tactic.LinearCombination.lt_of_eq

modified theorem Mathlib.Tactic.LinearCombination.lt_of_le

modified theorem Mathlib.Tactic.LinearCombination.lt_of_lt