chore: whitespace still (#24501)

adomani · riccardobrasca · commit cf424e95790f · 2025-05-07T15:45:44.000+02:00
Mostly whitespace changes found by the linter at #24465.
diff --git a/Archive/Imo/Imo2019Q4.lean b/Archive/Imo/Imo2019Q4.lean
@@ -35,7 +35,7 @@ open Finset
 namespace Imo2019Q4
 
 theorem upper_bound {k n : ℕ} (hk : k > 0)
-    (h : (k ! : ℤ) = ∏ i ∈ range n, ((2:ℤ) ^ n - (2:ℤ) ^ i)) : n < 6 := by
+    (h : (k ! : ℤ) = ∏ i ∈ range n, ((2 : ℤ) ^ n - (2 : ℤ) ^ i)) : n < 6 := by
   have h2 : ∑ i ∈ range n, i < k := by
     suffices emultiplicity 2 (k ! : ℤ) = ↑(∑ i ∈ range n, i : ℕ) by
       rw [← Nat.cast_lt (α := ℕ∞), ← this]; change emultiplicity ((2 : ℕ) : ℤ) _ < _
diff --git a/Mathlib/GroupTheory/CoprodI.lean b/Mathlib/GroupTheory/CoprodI.lean
@@ -85,7 +85,7 @@ variable {ι : Type*} (M : ι → Type*) [∀ i, Monoid (M i)]
 
 /-- A relation on the free monoid on alphabet `Σ i, M i`,
 relating `⟨i, 1⟩` with `1` and `⟨i, x⟩ * ⟨i, y⟩` with `⟨i, x * y⟩`. -/
-inductive Monoid.CoprodI.Rel : FreeMonoid (Σi, M i) → FreeMonoid (Σi, M i) → Prop
+inductive Monoid.CoprodI.Rel : FreeMonoid (Σ i, M i) → FreeMonoid (Σ i, M i) → Prop
   | of_one (i : ι) : Monoid.CoprodI.Rel (FreeMonoid.of ⟨i, 1⟩) 1
   | of_mul {i : ι} (x y : M i) :
     Monoid.CoprodI.Rel (FreeMonoid.of ⟨i, x⟩ * FreeMonoid.of ⟨i, y⟩) (FreeMonoid.of ⟨i, x * y⟩)
diff --git a/Mathlib/GroupTheory/PushoutI.lean b/Mathlib/GroupTheory/PushoutI.lean
@@ -494,7 +494,7 @@ noncomputable def consRecOn {motive : NormalWord d → Sort _} (w : NormalWord d
     (empty : motive empty)
     (cons : ∀ (i : ι) (g : G i) (w : NormalWord d) (hmw : w.fstIdx ≠ some i)
       (_hgn : g ∈ d.set i) (hgr : g ∉ (φ i).range) (_hw1 : w.head = 1),
-      motive w →  motive (cons g w hmw hgr))
+      motive w → motive (cons g w hmw hgr))
     (base : ∀ (h : H) (w : NormalWord d), w.head = 1 → motive w → motive
       (base φ h • w)) : motive w := by
   rcases w with ⟨w, head, h3⟩
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean b/Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean
@@ -296,7 +296,7 @@ variable {C} [Ring C] [Algebra R C]
 product can be assembled from maps on each component that (anti)commute on pure elements of the
 corresponding graded algebras. -/
 def lift (f : A →ₐ[R] C) (g : B →ₐ[R] C)
-    (h_anti_commutes : ∀ ⦃i j⦄ (a : 𝒜 i) (b : ℬ j), f a * g b = (-1 : ℤˣ)^(j * i) • (g b * f a)) :
+    (h_anti_commutes : ∀ ⦃i j⦄ (a : 𝒜 i) (b : ℬ j), f a * g b = (-1 : ℤˣ) ^ (j * i) • (g b * f a)) :
     (𝒜 ᵍ⊗[R] ℬ) →ₐ[R] C :=
   AlgHom.ofLinearMap
     (LinearMap.mul' R C
diff --git a/Mathlib/ModelTheory/Order.lean b/Mathlib/ModelTheory/Order.lean
@@ -365,7 +365,7 @@ instance : @OrderedStructure L M _ (L.leOfStructure M) _ := by
 -- because it will match with any `LE` typeclass search
 @[local instance]
 def decidableLEOfStructure
-    [h : DecidableRel (fun (a b : M) => Structure.RelMap (leSymb : L.Relations 2) ![a,b])] :
+    [h : DecidableRel (fun (a b : M) => Structure.RelMap (leSymb : L.Relations 2) ![a, b])] :
     letI := L.leOfStructure M
     DecidableLE M := h
 
@@ -385,7 +385,7 @@ def partialOrderOfModels [h : M ⊨ L.partialOrderTheory] : PartialOrder M where
 
 /-- Any model of a theory of linear orders is a linear order. -/
 def linearOrderOfModels [h : M ⊨ L.linearOrderTheory]
-    [DecidableRel (fun (a b : M) => Structure.RelMap (leSymb : L.Relations 2) ![a,b])] :
+    [DecidableRel (fun (a b : M) => Structure.RelMap (leSymb : L.Relations 2) ![a, b])] :
     LinearOrder M where
   __ := L.partialOrderOfModels M
   le_total := Relations.realize_total.1 ((Theory.model_iff _).1 h _
diff --git a/Mathlib/NumberTheory/FactorisationProperties.lean b/Mathlib/NumberTheory/FactorisationProperties.lean
@@ -136,7 +136,7 @@ theorem Prime.not_perfect (h : Prime p) : ¬ Perfect p := by
   exact not_imp_not.mpr (Perfect.pseudoperfect)
 
 /-- Any natural number power of a prime is deficient -/
-theorem Prime.deficient_pow  (h : Prime n) : Deficient (n ^ m) := by
+theorem Prime.deficient_pow (h : Prime n) : Deficient (n ^ m) := by
   rcases Nat.eq_zero_or_pos m with (rfl | _)
   · simpa using deficient_one
   · have h1 : (n ^ m).properDivisors = image (n ^ ·) (range m) := by
diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean
@@ -347,7 +347,7 @@ def realSpaceToLogSpace : realSpace K →ₗ[ℝ] {w : InfinitePlace K // w ≠
   map_add' := fun _ _ ↦ funext fun _ ↦ by simpa [sum_add_distrib] using by ring
   map_smul' := fun _ _ ↦ funext fun _ ↦ by simpa [← mul_sum] using by ring
 
-theorem realSpaceToLogSpace_apply (x :realSpace K) (w : {w : InfinitePlace K // w ≠ w₀}) :
+theorem realSpaceToLogSpace_apply (x : realSpace K) (w : {w : InfinitePlace K // w ≠ w₀}) :
     realSpaceToLogSpace x w = x w - w.1.mult * (∑ w', x w') * (Module.finrank ℚ K : ℝ)⁻¹ := rfl
 
 theorem realSpaceToLogSpace_expMap_symm {x : K} (hx : x ≠ 0) :
diff --git a/Mathlib/RingTheory/Binomial.lean b/Mathlib/RingTheory/Binomial.lean
@@ -462,7 +462,7 @@ end
 open Finset
 
 /-- Pochhammer version of Chu-Vandermonde identity -/
-theorem descPochhammer_smeval_add [Ring R] {r s : R} (k : ℕ) (h: Commute r s) :
+theorem descPochhammer_smeval_add [Ring R] {r s : R} (k : ℕ) (h : Commute r s) :
     (descPochhammer ℤ k).smeval (r + s) = ∑ ij ∈ antidiagonal k,
     Nat.choose k ij.1 * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s) := by
   induction k with
diff --git a/Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean b/Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean
@@ -37,7 +37,7 @@ variable {R : Type*} [CommRing R] [IsDomain R] {I : Ideal R}
 that uses the ideal of `R ⧸ I ^ (n + 1)`, compose with
 `Ideal.powQuotPowSuccLinearEquivMapMkPowSuccPow`. -/
 noncomputable
-def quotEquivPowQuotPowSucc (h : I.IsPrincipal) (h': I ≠ ⊥) (n : ℕ) :
+def quotEquivPowQuotPowSucc (h : I.IsPrincipal) (h' : I ≠ ⊥) (n : ℕ) :
     (R ⧸ I) ≃ₗ[R] (I ^ n : Ideal R) ⧸ (I • ⊤ : Submodule R (I ^ n : Ideal R)) := by
   let f : (I ^ n : Ideal R) →ₗ[R] (I ^ n : Ideal R) ⧸ (I • ⊤ : Submodule R (I ^ n : Ideal R)) :=
     Submodule.mkQ _
diff --git a/Mathlib/RingTheory/LocalRing/Subring.lean b/Mathlib/RingTheory/LocalRing/Subring.lean
@@ -30,7 +30,7 @@ theorem of_injective [IsLocalRing S] {f : R →+* S} (hf : Function.Injective f)
 
 /-- If in a sub(semi)ring `R` of a local (semi)ring `S` every element is either
 invertible or a zero divisor, then `R` is local. -/
-theorem of_subring [IsLocalRing S]  {R : Subsemiring S} (h : ∀ a, a ∈ R⁰ → IsUnit a) :
+theorem of_subring [IsLocalRing S] {R : Subsemiring S} (h : ∀ a, a ∈ R⁰ → IsUnit a) :
     IsLocalRing R :=
   of_injective R.subtype_injective h
 
diff --git a/Mathlib/RingTheory/Regular/RegularSequence.lean b/Mathlib/RingTheory/Regular/RegularSequence.lean
@@ -329,7 +329,7 @@ def recIterModByRegularWithRing
       [Module R M] → (r : R) → (rs : List R) → (h1 : IsSMulRegular M r) →
       (h2 : IsWeaklyRegular (QuotSMulTop r M)
               (rs.map (Ideal.Quotient.mk (Ideal.span {r})))) →
-      (ih : motive (R⧸Ideal.span {r}) (QuotSMulTop r M)
+      (ih : motive (R ⧸ Ideal.span {r}) (QuotSMulTop r M)
               (rs.map (Ideal.Quotient.mk (Ideal.span {r}))) h2) →
             motive R M (r :: rs) (cons' h1 h2)) :
     {R : Type u} → [CommRing R] → {M : Type v} → [AddCommGroup M] →
@@ -351,7 +351,7 @@ def ndrecWithRing
       [Module R M] → (r : R) → (rs : List R) → IsSMulRegular M r →
       IsWeaklyRegular (QuotSMulTop r M)
         (rs.map (Ideal.Quotient.mk (Ideal.span {r}))) →
-      motive (R⧸Ideal.span {r}) (QuotSMulTop r M)
+      motive (R ⧸ Ideal.span {r}) (QuotSMulTop r M)
         (rs.map (Ideal.Quotient.mk (Ideal.span {r}))) → motive R M (r :: rs))
     {R} [CommRing R] {M} [AddCommGroup M] [Module R M] {rs} :
     IsWeaklyRegular M rs → motive R M rs :=
@@ -460,7 +460,7 @@ def recIterModByRegularWithRing
       [Module R M] → (r : R) → (rs : List R) → (h1 : IsSMulRegular M r) →
       (h2 : IsRegular (QuotSMulTop r M)
               (rs.map (Ideal.Quotient.mk (Ideal.span {r})))) →
-      (ih : motive (R⧸Ideal.span {r}) (QuotSMulTop r M)
+      (ih : motive (R ⧸ Ideal.span {r}) (QuotSMulTop r M)
               (rs.map (Ideal.Quotient.mk (Ideal.span {r}))) h2) →
             motive R M (r :: rs) (cons' h1 h2))
     {R} [CommRing R] {M} [AddCommGroup M] [Module R M] {rs}
@@ -486,7 +486,7 @@ def ndrecIterModByRegularWithRing
       IsSMulRegular M r →
       IsRegular (QuotSMulTop r M)
         (rs.map (Ideal.Quotient.mk (Ideal.span {r}))) →
-      motive (R⧸Ideal.span {r}) (QuotSMulTop r M)
+      motive (R ⧸ Ideal.span {r}) (QuotSMulTop r M)
         (rs.map (Ideal.Quotient.mk (Ideal.span {r}))) →
       motive R M (r :: rs))
     {R} [CommRing R] {M} [AddCommGroup M] [Module R M] {rs} :
diff --git a/Mathlib/RingTheory/TwoSidedIdeal/Operations.lean b/Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
@@ -410,7 +410,7 @@ instance : CanLift (Ideal R) (TwoSidedIdeal R) TwoSidedIdeal.asIdeal (·.IsTwoSi
 end Ideal
 
 /-- A two-sided ideal is simply a left ideal that is two-sided. -/
-@[simps] def TwoSidedIdeal.orderIsoIsTwoSided  {R : Type*} [Ring R] :
+@[simps] def TwoSidedIdeal.orderIsoIsTwoSided {R : Type*} [Ring R] :
     TwoSidedIdeal R ≃o {I : Ideal R // I.IsTwoSided} where
   toFun I := ⟨I.asIdeal, inferInstance⟩
   invFun I := have := I.2; I.1.toTwoSided
diff --git a/Mathlib/SetTheory/Surreal/Multiplication.lean b/Mathlib/SetTheory/Surreal/Multiplication.lean
@@ -150,7 +150,7 @@ lemma P1_of_lt (h₁ : P3 x₃ x₂ y₂ y₃) (h₂ : P3 x₁ x₃ y₂ y₁) :
   convert add_lt_add h₁ h₂ using 1 <;> abel
 
 /-- The type of lists of arguments for P1, P2, and P4. -/
-inductive Args : Type (u+1)
+inductive Args : Type (u + 1)
   | P1 (x y : PGame.{u}) : Args
   | P24 (x₁ x₂ y : PGame.{u}) : Args
 
diff --git a/Mathlib/Tactic/FunProp/ContDiff.lean b/Mathlib/Tactic/FunProp/ContDiff.lean
@@ -80,7 +80,7 @@ the smallest possible value i.e. `n=m+1`.
 
 In conjunction with `ContDiff.of_le` we can recover the full power of the original theorem. -/
 theorem ContDiff.differentiable_iteratedDeriv' {m : ℕ} {f : K → F}
-    (hf : ContDiff K (m+1) f) : Differentiable K (iteratedDeriv m f) :=
+    (hf : ContDiff K (m + 1) f) : Differentiable K (iteratedDeriv m f) :=
   ContDiff.differentiable_iteratedDeriv m hf (Nat.cast_lt.mpr m.lt_succ_self)
 
 end deriv
diff --git a/Mathlib/Topology/CWComplex/Classical/Basic.lean b/Mathlib/Topology/CWComplex/Classical/Basic.lean
@@ -116,7 +116,7 @@ def CWComplex.mk.{u} {X : Type u} [TopologicalSpace X] (C : Set X)
     (continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (map n i).symm (map n i).target)
     (pairwiseDisjoint' :
       (univ : Set (Σ n, cell n)).PairwiseDisjoint (fun ni ↦ map ni.1 ni.2 '' ball 0 1))
-    (mapsTo: ∀ n i, ∃ I : Π m, Finset (cell m),
+    (mapsTo : ∀ n i, ∃ I : Π m, Finset (cell m),
       MapsTo (map n i) (sphere 0 1) (⋃ (m < n) (j ∈ I m), map m j '' closedBall 0 1))
     (closed' : ∀ (A : Set X), (asubc : A ⊆ C) →
       (∀ n j, IsClosed (A ∩ map n j '' closedBall 0 1)) → IsClosed A)
