chore(whitespace): yet some more whitespace changes (#22854)

Found by #22760.

Author: adomani

Mathlib/Algebra/Ring/Subring/IntPolynomial.lean

@@ -36,7 +36,7 @@ namespace Polynomial
 variable (P : K[X]) (hP : ∀ n : ℕ, P.coeff n ∈ R)
 
 @[simp]
-theorem int_coeff_eq  (n : ℕ) : ↑((P.int R hP).coeff n) = P.coeff n := rfl
+theorem int_coeff_eq (n : ℕ) : ↑((P.int R hP).coeff n) = P.coeff n := rfl
 
 @[simp]
 theorem int_leadingCoeff_eq : ↑(P.int R hP).leadingCoeff = P.leadingCoeff := rfl

Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean

@@ -301,7 +301,7 @@ theorem ofFinsupp_eq_one {a} :
     (⟨a⟩ : SkewMonoidAlgebra k G) = 1 ↔ a = Finsupp.single 1 1 := by
   rw [← ofFinsupp_one, ofFinsupp_inj]
 
-theorem single_one_one  : single 1 (1 : k) = 1 := rfl
+theorem single_one_one : single 1 (1 : k) = 1 := rfl
 
 theorem one_def : (1 : SkewMonoidAlgebra k G) = single 1 1 := rfl
 

Mathlib/Algebra/Star/Unitary.lean

@@ -122,7 +122,7 @@ def toUnits : unitary R →* Rˣ where
 theorem toUnits_injective : Function.Injective (toUnits : unitary R → Rˣ) := fun _ _ h =>
   Subtype.ext <| Units.ext_iff.mp h
 
-theorem _root_.IsUnit.mem_unitary_of_star_mul_self  {u : R} (hu : IsUnit u)
+theorem _root_.IsUnit.mem_unitary_of_star_mul_self {u : R} (hu : IsUnit u)
     (h_mul : star u * u = 1) : u ∈ unitary R := by
   refine unitary.mem_iff.mpr ⟨h_mul, ?_⟩
   lift u to Rˣ using hu

Mathlib/Algebra/Vertex/HVertexOperator.lean

@@ -100,7 +100,7 @@ end Coeff
 section Products
 
 variable {Γ Γ' : Type*} [OrderedCancelAddCommMonoid Γ] [OrderedCancelAddCommMonoid Γ'] {R : Type*}
-  [CommRing R] {U V W : Type*} [AddCommGroup U] [Module R U][AddCommGroup V] [Module R V]
+  [CommRing R] {U V W : Type*} [AddCommGroup U] [Module R U] [AddCommGroup V] [Module R V]
   [AddCommGroup W] [Module R W] (A : HVertexOperator Γ R V W) (B : HVertexOperator Γ' R U V)
 
 open HahnModule

Mathlib/Algebra/Vertex/VertexOperator.lean

@@ -91,7 +91,7 @@ theorem of_coeff_apply_coeff (f : ℤ → Module.End R V)
 
 @[simp]
 theorem ncoeff_of_coeff (f : ℤ → Module.End R V)
-    (hf : ∀(x : V), ∃(n : ℤ), ∀(m : ℤ), m < n → (f m) x = 0) (n : ℤ) :
+    (hf : ∀ (x : V), ∃ (n : ℤ), ∀ (m : ℤ), m < n → (f m) x = 0) (n : ℤ) :
     (of_coeff f hf) [[n]] = f (-n - 1) := by
   ext v
   rw [ncoeff, coeff_apply, of_coeff_apply_coeff]

Mathlib/CategoryTheory/Category/Quiv.lean

@@ -120,7 +120,7 @@ def homEquivOfIso {V W : Quiv} (e : V ≅ W) {X Y : V} :
 end
 
 section
-variable {V W : Type u } [Quiver V] [Quiver W]
+variable {V W : Type u} [Quiver V] [Quiver W]
   (e : V ≃ W) (he : ∀ X Y : V, (X ⟶ Y) ≃ (e X ⟶ e Y))
 
 include he in

Mathlib/CategoryTheory/Sigma/Basic.lean

@@ -25,25 +25,25 @@ variable {I : Type w₁} {C : I → Type u₁} [∀ i, Category.{v₁} (C i)]
 /-- The type of morphisms of a disjoint union of categories: for `X : C i` and `Y : C j`, a morphism
 `(i, X) ⟶ (j, Y)` if `i = j` is just a morphism `X ⟶ Y`, and if `i ≠ j` there are no such morphisms.
 -/
-inductive SigmaHom : (Σi, C i) → (Σi, C i) → Type max w₁ v₁ u₁
+inductive SigmaHom : (Σ i, C i) → (Σ i, C i) → Type max w₁ v₁ u₁
   | mk : ∀ {i : I} {X Y : C i}, (X ⟶ Y) → SigmaHom ⟨i, X⟩ ⟨i, Y⟩
 
 namespace SigmaHom
 
 /-- The identity morphism on an object. -/
-def id : ∀ X : Σi, C i, SigmaHom X X
+def id : ∀ X : Σ i, C i, SigmaHom X X
   | ⟨_, _⟩ => mk (𝟙 _)
 -- Porting note: reordered universes
 
-instance (X : Σi, C i) : Inhabited (SigmaHom X X) :=
+instance (X : Σ i, C i) : Inhabited (SigmaHom X X) :=
   ⟨id X⟩
 
 /-- Composition of sigma homomorphisms. -/
-def comp : ∀ {X Y Z : Σi, C i}, SigmaHom X Y → SigmaHom Y Z → SigmaHom X Z
+def comp : ∀ {X Y Z : Σ i, C i}, SigmaHom X Y → SigmaHom Y Z → SigmaHom X Z
   | _, _, _, mk f, mk g => mk (f ≫ g)
 -- Porting note: reordered universes
 
-instance : CategoryStruct (Σi, C i) where
+instance : CategoryStruct (Σ i, C i) where
   Hom := SigmaHom
   id := id
   comp f g := comp f g
@@ -52,36 +52,36 @@ instance : CategoryStruct (Σi, C i) where
 lemma comp_def (i : I) (X Y Z : C i) (f : X ⟶ Y) (g : Y ⟶ Z) : comp (mk f) (mk g) = mk (f ≫ g) :=
   rfl
 
-lemma assoc : ∀ {X Y Z W : Σi, C i} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W), (f ≫ g) ≫ h = f ≫ g ≫ h
+lemma assoc : ∀ {X Y Z W : Σ i, C i} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W), (f ≫ g) ≫ h = f ≫ g ≫ h
   | _, _, _, _, mk _, mk _, mk _ => congr_arg mk (Category.assoc _ _ _)
 
-lemma id_comp : ∀ {X Y : Σi, C i} (f : X ⟶ Y), 𝟙 X ≫ f = f
+lemma id_comp : ∀ {X Y : Σ i, C i} (f : X ⟶ Y), 𝟙 X ≫ f = f
   | _, _, mk _ => congr_arg mk (Category.id_comp _)
 
-lemma comp_id : ∀ {X Y : Σi, C i} (f : X ⟶ Y), f ≫ 𝟙 Y = f
+lemma comp_id : ∀ {X Y : Σ i, C i} (f : X ⟶ Y), f ≫ 𝟙 Y = f
   | _, _, mk _ => congr_arg mk (Category.comp_id _)
 
 end SigmaHom
 
-instance sigma : Category (Σi, C i) where
+instance sigma : Category (Σ i, C i) where
   id_comp := SigmaHom.id_comp
   comp_id := SigmaHom.comp_id
   assoc := SigmaHom.assoc
 
 /-- The inclusion functor into the disjoint union of categories. -/
 @[simps map]
-def incl (i : I) : C i ⥤ Σi, C i where
+def incl (i : I) : C i ⥤ Σ i, C i where
   obj X := ⟨i, X⟩
   map := SigmaHom.mk
 
 @[simp]
 lemma incl_obj {i : I} (X : C i) : (incl i).obj X = ⟨i, X⟩ :=
   rfl
 
-instance (i : I) : Functor.Full (incl i : C i ⥤ Σi, C i) where
+instance (i : I) : Functor.Full (incl i : C i ⥤ Σ i, C i) where
   map_surjective := fun ⟨f⟩ => ⟨f, rfl⟩
 
-instance (i : I) : Functor.Faithful (incl i : C i ⥤ Σi, C i) where
+instance (i : I) : Functor.Faithful (incl i : C i ⥤ Σ i, C i) where
   map_injective {_ _ _ _} h := by injection h
 
 section
@@ -92,19 +92,19 @@ variable {D : Type u₂} [Category.{v₂} D] (F : ∀ i, C i ⥤ D)
 To build a natural transformation over the sigma category, it suffices to specify it restricted to
 each subcategory.
 -/
-def natTrans {F G : (Σi, C i) ⥤ D} (h : ∀ i : I, incl i ⋙ F ⟶ incl i ⋙ G) : F ⟶ G where
+def natTrans {F G : (Σ i, C i) ⥤ D} (h : ∀ i : I, incl i ⋙ F ⟶ incl i ⋙ G) : F ⟶ G where
   app := fun ⟨j, X⟩ => (h j).app X
   naturality := by
     rintro ⟨j, X⟩ ⟨_, _⟩ ⟨f⟩
     apply (h j).naturality
 
 @[simp]
-lemma natTrans_app {F G : (Σi, C i) ⥤ D} (h : ∀ i : I, incl i ⋙ F ⟶ incl i ⋙ G) (i : I)
+lemma natTrans_app {F G : (Σ i, C i) ⥤ D} (h : ∀ i : I, incl i ⋙ F ⟶ incl i ⋙ G) (i : I)
     (X : C i) : (natTrans h).app ⟨i, X⟩ = (h i).app X :=
   rfl
 
 /-- (Implementation). An auxiliary definition to build the functor `desc`. -/
-def descMap : ∀ X Y : Σi, C i, (X ⟶ Y) → ((F X.1).obj X.2 ⟶ (F Y.1).obj Y.2)
+def descMap : ∀ X Y : Σ i, C i, (X ⟶ Y) → ((F X.1).obj X.2 ⟶ (F Y.1).obj Y.2)
   | _, _, SigmaHom.mk g => (F _).map g
 -- Porting note: reordered universes
 
@@ -117,7 +117,7 @@ this property.
 This witnesses that the sigma-type is the coproduct in Cat.
 -/
 @[simps obj]
-def desc : (Σi, C i) ⥤ D where
+def desc : (Σ i, C i) ⥤ D where
   obj X := (F X.1).obj X.2
   map g := descMap F _ _ g
   map_id := by
@@ -149,26 +149,26 @@ lemma inclDesc_inv_app (i : I) (X : C i) : (inclDesc F i).inv.app X = 𝟙 ((F i
 /-- If `q` when restricted to each subcategory `C i` agrees with `F i`, then `q` is isomorphic to
 `desc F`.
 -/
-def descUniq (q : (Σi, C i) ⥤ D) (h : ∀ i, incl i ⋙ q ≅ F i) : q ≅ desc F :=
+def descUniq (q : (Σ i, C i) ⥤ D) (h : ∀ i, incl i ⋙ q ≅ F i) : q ≅ desc F :=
   NatIso.ofComponents (fun ⟨i, X⟩ => (h i).app X) <| by
     rintro ⟨i, X⟩ ⟨_, _⟩ ⟨f⟩
     apply (h i).hom.naturality f
 
 @[simp]
-lemma descUniq_hom_app (q : (Σi, C i) ⥤ D) (h : ∀ i, incl i ⋙ q ≅ F i) (i : I) (X : C i) :
+lemma descUniq_hom_app (q : (Σ i, C i) ⥤ D) (h : ∀ i, incl i ⋙ q ≅ F i) (i : I) (X : C i) :
     (descUniq F q h).hom.app ⟨i, X⟩ = (h i).hom.app X :=
   rfl
 
 @[simp]
-lemma descUniq_inv_app (q : (Σi, C i) ⥤ D) (h : ∀ i, incl i ⋙ q ≅ F i) (i : I) (X : C i) :
+lemma descUniq_inv_app (q : (Σ i, C i) ⥤ D) (h : ∀ i, incl i ⋙ q ≅ F i) (i : I) (X : C i) :
     (descUniq F q h).inv.app ⟨i, X⟩ = (h i).inv.app X :=
   rfl
 
 /--
 If `q₁` and `q₂` when restricted to each subcategory `C i` agree, then `q₁` and `q₂` are isomorphic.
 -/
 @[simps]
-def natIso {q₁ q₂ : (Σi, C i) ⥤ D} (h : ∀ i, incl i ⋙ q₁ ≅ incl i ⋙ q₂) : q₁ ≅ q₂ where
+def natIso {q₁ q₂ : (Σ i, C i) ⥤ D} (h : ∀ i, incl i ⋙ q₁ ≅ incl i ⋙ q₂) : q₁ ≅ q₂ where
   hom := natTrans fun i => (h i).hom
   inv := natTrans fun i => (h i).inv
 
@@ -179,7 +179,7 @@ section
 variable (C) {J : Type w₂} (g : J → I)
 
 /-- A function `J → I` induces a functor `Σ j, C (g j) ⥤ Σ i, C i`. -/
-def map : (Σj : J, C (g j)) ⥤ Σi : I, C i :=
+def map : (Σj : J, C (g j)) ⥤ Σ i : I, C i :=
   desc fun j => incl (g j)
 
 @[simp]
@@ -201,7 +201,7 @@ variable (I)
 
 /-- The functor `Sigma.map` applied to the identity function is just the identity functor. -/
 @[simps!]
-def mapId : map C (id : I → I) ≅ 𝟭 (Σi, C i) :=
+def mapId : map C (id : I → I) ≅ 𝟭 (Σ i, C i) :=
   natIso fun i => NatIso.ofComponents fun _ => Iso.refl _
 
 variable {I} {K : Type w₃}
@@ -223,7 +223,7 @@ variable {D : I → Type u₁} [∀ i, Category.{v₁} (D i)]
 
 /-- Assemble an `I`-indexed family of functors into a functor between the sigma types.
 -/
-def sigma (F : ∀ i, C i ⥤ D i) : (Σi, C i) ⥤ Σi, D i :=
+def sigma (F : ∀ i, C i ⥤ D i) : (Σ i, C i) ⥤ Σ i, D i :=
   desc fun i => F i ⋙ incl i
 
 end Functor

Mathlib/Combinatorics/SimpleGraph/Matching.lean

@@ -53,7 +53,7 @@ assert_not_exists Field TwoSidedIdeal
 open Function
 
 namespace SimpleGraph
-variable {V W : Type*} {G G': SimpleGraph V} {M M' : Subgraph G} {v w : V}
+variable {V W : Type*} {G G' : SimpleGraph V} {M M' : Subgraph G} {v w : V}
 
 namespace Subgraph
 

Mathlib/Combinatorics/SimpleGraph/Path.lean

@@ -1266,7 +1266,7 @@ def IsBridge (G : SimpleGraph V) (e : Sym2 V) : Prop :=
 theorem isBridge_iff {u v : V} :
     G.IsBridge s(u, v) ↔ G.Adj u v ∧ ¬(G \ fromEdgeSet {s(u, v)}).Reachable u v := Iff.rfl
 
-theorem reachable_delete_edges_iff_exists_walk {v w v' w': V} :
+theorem reachable_delete_edges_iff_exists_walk {v w v' w' : V} :
     (G \ fromEdgeSet {s(v, w)}).Reachable v' w' ↔ ∃ p : G.Walk v' w', ¬s(v, w) ∈ p.edges := by
   constructor
   · rintro ⟨p⟩

Mathlib/Data/Matrix/Invertible.lean

@@ -117,7 +117,7 @@ section Woodbury
 
 variable [Fintype m] [DecidableEq m] [Ring α]
     (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α)
-    [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A * U)]
+    [Invertible A] [Invertible C] [Invertible (⅟ C + V * ⅟ A * U)]
 
 -- No spaces around multiplication signs for better clarity
 lemma add_mul_mul_invOf_mul_eq_one :