chore(whitespace): some more changes in whitespace (#22840)

Found by #22760.

Author: adomani

Mathlib/Algebra/Central/Basic.lean

@@ -23,7 +23,7 @@ universe u v
 
 namespace Algebra.IsCentral
 
-variable (K : Type u) [CommSemiring K] (D D': Type v) [Semiring D] [Algebra K D]
+variable (K : Type u) [CommSemiring K] (D D' : Type v) [Semiring D] [Algebra K D]
   [h : IsCentral K D] [Semiring D'] [Algebra K D']
 
 @[simp]

Mathlib/Algebra/Group/Action/Equidecomp.lean

@@ -50,7 +50,7 @@ We take this as our definition as it is easier to work with. It is implemented a
 
 -/
 
-variable {X G : Type*} {A B C: Set X}
+variable {X G : Type*} {A B C : Set X}
 
 open Function Set Pointwise PartialEquiv
 

Mathlib/Algebra/Group/Submonoid/Units.lean

@@ -305,7 +305,7 @@ units of `M`. -/
 noncomputable def ofUnitsTopEquiv : (⊤ : Subgroup Mˣ).ofUnits ≃* Mˣ :=
   (⊤ : Subgroup Mˣ).ofUnitsEquivType.trans topEquiv
 
-variable {G : Type*}  [Group G]
+variable {G : Type*} [Group G]
 
 @[to_additive]
 lemma mem_units_iff_val_mem (H : Subgroup G) (x : Gˣ) : x ∈ H.units ↔ (x : G) ∈ H := by

Mathlib/Algebra/Module/LinearMap/Basic.lean

@@ -50,7 +50,7 @@ theorem _root_.DomMulAct.mk_smul_linearMap_apply (a : S') (f : M →ₛₗ[σ₁
     (DomMulAct.mk a • f) x = f (a • x) :=
   rfl
 
-theorem  _root_.DomMulAct.coe_smul_linearMap (a : S'ᵈᵐᵃ) (f : M →ₛₗ[σ₁₂] M') :
+theorem _root_.DomMulAct.coe_smul_linearMap (a : S'ᵈᵐᵃ) (f : M →ₛₗ[σ₁₂] M') :
     (a • f : M →ₛₗ[σ₁₂] M') = a • (f : M → M') :=
   rfl
 

Mathlib/Algebra/Quaternion.lean

@@ -92,7 +92,7 @@ def equivTuple {R : Type*} (c₁ c₂ c₃: R) : ℍ[R,c₁,c₂,c₃] ≃ (Fin
   right_inv f := by ext ⟨_, _ | _ | _ | _ | _ | ⟨⟩⟩ <;> rfl
 
 @[simp]
-theorem equivTuple_apply {R : Type*} (c₁ c₂ c₃: R) (x : ℍ[R,c₁,c₂,c₃]) :
+theorem equivTuple_apply {R : Type*} (c₁ c₂ c₃ : R) (x : ℍ[R,c₁,c₂,c₃]) :
     equivTuple c₁ c₂ c₃ x = ![x.re, x.imI, x.imJ, x.imK] :=
   rfl
 

Mathlib/CategoryTheory/Limits/Final.lean

@@ -437,7 +437,7 @@ variable {C : Type v} [Category.{v} C] {D : Type u₁} [Category.{v} D] (F : C 
 
 namespace Final
 
-theorem zigzag_of_eqvGen_quot_rel {F : C ⥤ D} {d : D} {f₁ f₂ : ΣX, d ⟶ F.obj X}
+theorem zigzag_of_eqvGen_quot_rel {F : C ⥤ D} {d : D} {f₁ f₂ : Σ X, d ⟶ F.obj X}
     (t : Relation.EqvGen (Types.Quot.Rel.{v, v} (F ⋙ coyoneda.obj (op d))) f₁ f₂) :
     Zigzag (StructuredArrow.mk f₁.2) (StructuredArrow.mk f₂.2) := by
   induction t with

Mathlib/Data/Seq/Seq.lean

@@ -918,7 +918,7 @@ theorem terminatedAt_map_iff {f : α → β} {s : Seq α} {n : ℕ} :
   simp [TerminatedAt]
 
 @[simp]
-theorem terminates_map_iff {f : α → β} {s : Seq α}  :
+theorem terminates_map_iff {f : α → β} {s : Seq α} :
     (map f s).Terminates ↔ s.Terminates := by
   simp [Terminates]
 

Mathlib/LinearAlgebra/Vandermonde.lean

@@ -118,18 +118,19 @@ theorem vandermonde_transpose_mul_vandermonde (v : Fin n → R) (i j) :
   simp only [vandermonde_apply, Matrix.mul_apply, Matrix.transpose_apply, pow_add]
 
 theorem rectVandermonde_apply_zero_right {α : Type*} {v w : α → R} {i : α} (hw : w i = 0) :
-    rectVandermonde v w (n+1) i = Pi.single (Fin.last n) ((v i) ^ n) := by
+    rectVandermonde v w (n + 1) i = Pi.single (Fin.last n) ((v i) ^ n) := by
   ext j
   obtain rfl | hlt := j.le_last.eq_or_lt
   · simp [rectVandermonde_apply]
   rw [rectVandermonde_apply, Pi.single_eq_of_ne hlt.ne, hw, zero_pow, mul_zero]
   simpa [Nat.sub_eq_zero_iff_le] using hlt
 
-theorem projVandermonde_apply_of_ne_zero {v w : Fin (n+1) → K} {i j : Fin (n+1)} (hw : w i ≠ 0) :
+theorem projVandermonde_apply_of_ne_zero
+    {v w : Fin (n + 1) → K} {i j : Fin (n + 1)} (hw : w i ≠ 0) :
     projVandermonde v w i j = (v i) ^ j.1 * (w i) ^ n / (w i) ^ j.1 := by
   rw [projVandermonde_apply, eq_div_iff (by simp [hw]), mul_assoc, ← pow_add, rev_add_cast]
 
-theorem projVandermonde_apply_zero_right {v w : Fin (n+1) → R} {i : Fin (n+1)} (hw : w i = 0) :
+theorem projVandermonde_apply_zero_right {v w : Fin (n + 1) → R} {i : Fin (n + 1)} (hw : w i = 0) :
     projVandermonde v w i = Pi.single (Fin.last n) ((v i) ^ n)  := by
   ext j
   obtain rfl | hlt := j.le_last.eq_or_lt
@@ -165,7 +166,7 @@ private theorem det_projVandermonde_of_field (v w : Fin n → K) :
   /- Let `W` be obtained from the matrix by subtracting `r = (v 0) / (w 0)` times each column
   from the next column, starting from the penultimate column. This doesn't change the determinant.-/
   set r := v 0 / w 0 with hr
-  set W : Matrix (Fin (n+1)) (Fin (n+1)) K := .of fun i ↦ (cons (projVandermonde v w i 0)
+  set W : Matrix (Fin (n + 1)) (Fin (n + 1)) K := .of fun i ↦ (cons (projVandermonde v w i 0)
     (fun j ↦ projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc))
   -- deleting the first row and column of `W` gives a row-scaling of a Vandermonde matrix.
   have hW_eq : (W.submatrix succ succ) = .of fun i j ↦ (v (succ i) - r * w (succ i)) *

Mathlib/MeasureTheory/OuterMeasure/BorelCantelli.lean

@@ -86,7 +86,7 @@ theorem ae_eventually_not_mem {s : ℕ → Set α} (hs : (∑' i, μ (s i)) ≠
     ∀ᵐ x ∂μ, ∀ᶠ n in atTop, x ∉ s n :=
   measure_setOf_frequently_eq_zero hs
 
-theorem measure_liminf_cofinite_eq_zero [Infinite ι]  {s : ι → Set α} (h : ∑' i, μ (s i) ≠ ∞) :
+theorem measure_liminf_cofinite_eq_zero [Infinite ι] {s : ι → Set α} (h : ∑' i, μ (s i) ≠ ∞) :
     μ (liminf s cofinite) = 0 := by
   rw [← le_zero_iff, ← measure_limsup_cofinite_eq_zero h]
   exact measure_mono liminf_le_limsup

Mathlib/RingTheory/Finiteness/Subalgebra.lean

@@ -20,7 +20,7 @@ open Submodule
 
 variable {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
 
-theorem fg_bot_toSubmodule  : (⊥ : Subalgebra R A).toSubmodule.FG :=
+theorem fg_bot_toSubmodule : (⊥ : Subalgebra R A).toSubmodule.FG :=
   ⟨{1}, by simp [Algebra.toSubmodule_bot, one_eq_span]⟩
 
 instance finite_bot : Module.Finite R (⊥ : Subalgebra R A) :=