style: fix multiple spaces before colon (#7411)

Purely cosmetic PR

Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

@@ -144,7 +144,7 @@ lemma ofHoms_v_comp_d (ψ : ∀ (p : ℤ), F.X p ⟶ G.X p) (p q q' : ℤ) (hpq
   rw [ofHoms_v]
 
 @[simp]
-lemma d_comp_ofHoms_v (ψ : ∀ (p : ℤ), F.X p ⟶ G.X p) (p' p q  : ℤ) (hpq : p + 0 = q) :
+lemma d_comp_ofHoms_v (ψ : ∀ (p : ℤ), F.X p ⟶ G.X p) (p' p q : ℤ) (hpq : p + 0 = q) :
     F.d p' p ≫ (ofHoms ψ).v p q hpq = F.d p' q ≫ ψ q := by
   rw [add_zero] at hpq
   subst hpq
@@ -171,7 +171,7 @@ lemma ofHom_v_comp_d (φ : F ⟶ G) (p q q' : ℤ) (hpq : p + 0 = q) :
 by simp only [ofHom, ofHoms_v_comp_d]
 
 @[simp]
-lemma d_comp_ofHom_v (φ : F ⟶ G) (p' p q  : ℤ) (hpq : p + 0 = q) :
+lemma d_comp_ofHom_v (φ : F ⟶ G) (p' p q : ℤ) (hpq : p + 0 = q) :
     F.d p' p ≫ (ofHom φ).v p q hpq = F.d p' q ≫ φ.f q := by
   simp only [ofHom, d_comp_ofHoms_v]
 

Mathlib/Algebra/Tropical/Lattice.lean

@@ -62,7 +62,7 @@ instance instConditionallyCompleteLatticeTropical [ConditionallyCompleteLattice
     ConditionallyCompleteLattice (Tropical R) :=
   { @instInfTropical R _, @instSupTropical R _,
     instLatticeTropical with
-    le_csSup  := fun _s _x hs hx ↦
+    le_csSup := fun _s _x hs hx ↦
       le_csSup (untrop_monotone.map_bddAbove hs) (Set.mem_image_of_mem untrop hx)
     csSup_le := fun _s _x hs hx ↦
       csSup_le (hs.image untrop) (untrop_monotone.mem_upperBounds_image hx)

Mathlib/Analysis/Normed/Group/HomCompletion.lean

@@ -13,7 +13,7 @@ import Mathlib.Analysis.Normed.Group.Completion
 
 Given two (semi) normed groups `G` and `H` and a normed group hom `f : NormedAddGroupHom G H`,
 we build and study a normed group hom
-`f.completion  : NormedAddGroupHom (completion G) (completion H)` such that the diagram
+`f.completion : NormedAddGroupHom (completion G) (completion H)` such that the diagram
 
 ```
                    f

Mathlib/CategoryTheory/Abelian/NonPreadditive.lean

@@ -450,7 +450,7 @@ def preadditive : Preadditive C where
       add_zero := add_zero
       neg := fun f => -f
       add_left_neg := neg_add_self
-      sub_eq_add_neg  := fun f g => (add_neg f g).symm -- Porting note: autoParam failed
+      sub_eq_add_neg := fun f g => (add_neg f g).symm -- Porting note: autoParam failed
       add_comm := add_comm }
   add_comp := add_comp
   comp_add := comp_add

Mathlib/CategoryTheory/Bicategory/Free.lean

@@ -60,7 +60,7 @@ instance quiver : Quiver.{max u v + 1} (FreeBicategory B) where
   Hom := fun a b : B => Hom a b
 
 instance categoryStruct : CategoryStruct.{max u v} (FreeBicategory B) where
-  id  := fun a : B => Hom.id a
+  id   := fun a : B => Hom.id a
   comp := @fun _ _ _ => Hom.comp
 
 /-- Representatives of 2-morphisms in the free bicategory. -/

Mathlib/CategoryTheory/Category/Factorisation.lean

@@ -29,7 +29,7 @@ variable {C : Type u} [Category.{v} C]
 and the condition that their composition equals `f`. -/
 structure Factorisation {X Y : C} (f : X ⟶ Y) where
   /-- The midpoint of the factorisation. -/
-  mid  : C
+  mid : C
   /-- The morphism into the factorisation midpoint. -/
   ι   : X ⟶ mid
   /-- The morphism out of the factorisation midpoint. -/

Mathlib/CategoryTheory/Iso.lean

@@ -89,7 +89,7 @@ theorem ext ⦃α β : X ≅ Y⦄ (w : α.hom = β.hom) : α = β :=
   calc
     α.inv = α.inv ≫ β.hom ≫ β.inv   := by rw [Iso.hom_inv_id, Category.comp_id]
     _     = (α.inv ≫ α.hom) ≫ β.inv := by rw [Category.assoc, ← w]
-    _     = β.inv                   := by rw [Iso.inv_hom_id, Category.id_comp]
+    _     = β.inv                    := by rw [Iso.inv_hom_id, Category.id_comp]
 #align category_theory.iso.ext CategoryTheory.Iso.ext
 
 /-- Inverse isomorphism. -/

Mathlib/CategoryTheory/Over.lean

@@ -524,7 +524,7 @@ instance epi_right_of_epi {f g : Under X} (k : f ⟶ g) [Epi k] : Epi k.right :=
   let l' : g ⟶ mk (g.hom ≫ m) := homMk l (by
     dsimp; rw [← Under.w k, Category.assoc, a, Category.assoc])
   -- Porting note: add type ascription here to `homMk m`
-  suffices l' = (homMk m  : g ⟶ mk (g.hom ≫ m)) by apply congrArg CommaMorphism.right this
+  suffices l' = (homMk m : g ⟶ mk (g.hom ≫ m)) by apply congrArg CommaMorphism.right this
   rw [← cancel_epi k]; ext; apply a
 #align category_theory.under.epi_right_of_epi CategoryTheory.Under.epi_right_of_epi
 

Mathlib/CategoryTheory/Shift/Basic.lean

@@ -714,7 +714,7 @@ lemma map_hasShiftOfFullyFaithful_add_hom_app (a b : A) (X : C) :
 lemma map_hasShiftOfFullyFaithful_add_inv_app (a b : A) (X : C) :
     F.map ((hasShiftOfFullyFaithful_add F s i a b).inv.app X) =
       (i b).hom.app ((s a).obj X) ≫ ((i a).hom.app X)⟦b⟧' ≫
-        (shiftFunctorAdd D a b).inv.app (F.obj X) ≫ (i (a + b)).inv.app X  := by
+        (shiftFunctorAdd D a b).inv.app (F.obj X) ≫ (i (a + b)).inv.app X := by
   dsimp [hasShiftOfFullyFaithful_add]
   simp
 #align category_theory.map_has_shift_of_fully_faithful_add_inv_app CategoryTheory.map_hasShiftOfFullyFaithful_add_inv_app

Mathlib/CategoryTheory/Shift/Localization.lean

@@ -57,7 +57,7 @@ variable [W.IsCompatibleWithShift A]
 /-- When `L : C ⥤ D` is a localization functor with respect to a morphism property `W`
 that is compatible with the shift by a monoid `A` on `C`, this is the induced
 shift on the category `D`. -/
-noncomputable def HasShift.localized  : HasShift D A :=
+noncomputable def HasShift.localized : HasShift D A :=
   HasShift.induced L A
     (fun a => Localization.lift (shiftFunctor C a ⋙ L)
       (MorphismProperty.IsCompatibleWithShift.shiftFunctor_comp_inverts L W a) L)

Mathlib/CategoryTheory/Whiskering.lean

@@ -12,7 +12,7 @@ import Mathlib.CategoryTheory.Functor.FullyFaithful
 /-!
 # Whiskering
 
-Given a functor `F  : C ⥤ D` and functors `G H : D ⥤ E` and a natural transformation `α : G ⟶ H`,
+Given a functor `F : C ⥤ D` and functors `G H : D ⥤ E` and a natural transformation `α : G ⟶ H`,
 we can construct a new natural transformation `F ⋙ G ⟶ F ⋙ H`,
 called `whiskerLeft F α`. This is the same as the horizontal composition of `𝟙 F` with `α`.
 

Mathlib/Data/Finset/Pointwise.lean

@@ -854,7 +854,7 @@ section Monoid
 variable [Monoid α] {s t : Finset α} {a : α} {m n : ℕ}
 
 @[to_additive (attr := simp, norm_cast)]
-theorem coe_pow (s : Finset α) (n : ℕ) : ↑(s ^ n) = (s : Set α) ^ n  := by
+theorem coe_pow (s : Finset α) (n : ℕ) : ↑(s ^ n) = (s : Set α) ^ n := by
   change ↑(npowRec n s) = (s: Set α) ^ n
   induction' n with n ih
   · rw [npowRec, pow_zero, coe_one]

Mathlib/Data/Nat/GCD/Basic.lean

@@ -93,7 +93,7 @@ theorem gcd_self_add_right (m n : ℕ) : gcd m (m + n) = gcd m n := by
 @[simp]
 theorem gcd_sub_self_left {m n : ℕ} (h : m ≤ n) : gcd (n - m) m = gcd n m := by
   calc
-    gcd (n - m) m = gcd (n - m + m) m  := by rw [← gcd_add_self_left (n - m) m]
+    gcd (n - m) m = gcd (n - m + m) m := by rw [← gcd_add_self_left (n - m) m]
                 _ = gcd n m := by rw [Nat.sub_add_cancel h]
 
 @[simp]

Mathlib/FieldTheory/Finite/GaloisField.lean

@@ -65,7 +65,7 @@ variable (p : ℕ) [Fact p.Prime] (n : ℕ)
 /-- A finite field with `p ^ n` elements.
 Every field with the same cardinality is (non-canonically)
 isomorphic to this field. -/
-def GaloisField  := SplittingField (X ^ p ^ n - X : (ZMod p)[X])
+def GaloisField := SplittingField (X ^ p ^ n - X : (ZMod p)[X])
 -- deriving Field -- Porting note: see https://github.com/leanprover-community/mathlib4/issues/5020
 #align galois_field GaloisField
 

Mathlib/GroupTheory/FreeGroup/Basic.lean

@@ -1087,7 +1087,7 @@ instance : LawfulMonad FreeGroup.{u} := LawfulMonad.mk'
       (fun x => by intros; iterate 2 rw [pure_bind])
       (fun x ih => by intros; (iterate 3 rw [inv_bind]); rw [ih])
       (fun x y ihx ihy => by intros; (iterate 3 rw [mul_bind]); rw [ihx, ihy]))
-  (bind_pure_comp  := fun f x =>
+  (bind_pure_comp := fun f x =>
     FreeGroup.induction_on x (by rw [one_bind, map_one]) (fun x => by rw [pure_bind, map_pure])
       (fun x ih => by rw [inv_bind, map_inv, ih]) fun x y ihx ihy => by
       rw [mul_bind, map_mul, ihx, ihy])

Mathlib/LinearAlgebra/DFinsupp.lean

@@ -221,7 +221,7 @@ theorem sum_mapRange_index.linearMap [∀ (i : ι) (x : β₁ i), Decidable (x 
     {l : Π₀ i, β₁ i} :
     -- Porting note: Needed to add (M := ...) below
     (DFinsupp.lsum ℕ (M := β₂)) h (mapRange.linearMap f l)
-      = (DFinsupp.lsum ℕ (M := β₁)) (fun i => (h i).comp (f i)) l  := by
+      = (DFinsupp.lsum ℕ (M := β₁)) (fun i => (h i).comp (f i)) l := by
   simpa [DFinsupp.sumAddHom_apply] using sum_mapRange_index fun i => by simp
 #align dfinsupp.sum_map_range_index.linear_map DFinsupp.sum_mapRange_index.linearMap
 

Mathlib/MeasureTheory/Group/Action.lean

@@ -123,7 +123,7 @@ theorem smulInvariantMeasure_map [SMul M α] [SMul M β]
     _ = μ ((f <| m • ·) ⁻¹' S) := by simp_rw [hsmul]
     _ = μ ((m • ·) ⁻¹' (f ⁻¹' S)) := by rw [←preimage_preimage]
     _ = μ (f ⁻¹' S) := by rw [SMulInvariantMeasure.measure_preimage_smul m (hS.preimage hf)]
-    _ = map f μ S  := (map_apply hf hS).symm
+    _ = map f μ S := (map_apply hf hS).symm
 
 @[to_additive]
 instance smulInvariantMeasure_map_smul [SMul M α] [SMul N α] [SMulCommClass N M α]

Mathlib/Order/Basic.lean

@@ -735,7 +735,7 @@ instance instPartialOrder (α : Type*) [PartialOrder α] : PartialOrder αᵒᵈ
 
 instance instLinearOrder (α : Type*) [LinearOrder α] : LinearOrder αᵒᵈ where
   __ := inferInstanceAs (PartialOrder αᵒᵈ)
-  le_total     := λ a b : α => le_total b a
+  le_total := λ a b : α => le_total b a
   max := fun a b ↦ (min a b : α)
   min := fun a b ↦ (max a b : α)
   min_def := fun a b ↦ show (max .. : α) = _ by rw [max_comm, max_def]; rfl

Mathlib/Order/Booleanisation.lean

@@ -122,7 +122,7 @@ instance instCompl : HasCompl (Booleanisation α) where
 * `aᶜ \ b` is `(a ⊔ b)ᶜ`
 * `aᶜ \ bᶜ` is `b \ a` -/
 instance instSDiff : SDiff (Booleanisation α) where
-  sdiff x y  := match x, y with
+  sdiff x y := match x, y with
     | lift a, lift b => lift (a \ b)
     | lift a, comp b => lift (a ⊓ b)
     | comp a, lift b => comp (a ⊔ b)

Mathlib/Order/Hom/CompleteLattice.lean

@@ -256,7 +256,7 @@ instance : sSupHomClass (sSupHom α β) α β
 
 -- Porting note: times out
 @[simp]
-theorem toFun_eq_coe {f : sSupHom α β} : f.toFun = ⇑f  :=
+theorem toFun_eq_coe {f : sSupHom α β} : f.toFun = ⇑f :=
   rfl
 #align Sup_hom.to_fun_eq_coe sSupHom.toFun_eq_coe
 

Mathlib/RingTheory/Ideal/Operations.lean

@@ -260,7 +260,7 @@ submodule `M'` of `x`, we only need to show that `r ^ n • x ∈ M'` for some `
 theorem mem_of_span_eq_top_of_smul_pow_mem (M' : Submodule R M) (s : Set R) (hs : Ideal.span s = ⊤)
     (x : M) (H : ∀ r : s, ∃ n : ℕ, ((r : R) ^ n : R) • x ∈ M') : x ∈ M' := by
   obtain ⟨s', hs₁, hs₂⟩ := (Ideal.span_eq_top_iff_finite _).mp hs
-  replace H : ∀ r : s', ∃ n : ℕ, ((r : R) ^ n  : R) • x ∈ M' := fun r => H ⟨_, hs₁ r.2⟩
+  replace H : ∀ r : s', ∃ n : ℕ, ((r : R) ^ n : R) • x ∈ M' := fun r => H ⟨_, hs₁ r.2⟩
   choose n₁ n₂ using H
   let N := s'.attach.sup n₁
   have hs' := Ideal.span_pow_eq_top (s' : Set R) hs₂ N

Mathlib/RingTheory/Localization/Basic.lean

@@ -424,7 +424,7 @@ theorem mk'_mul_mk'_eq_one' (x : R) (y : M) (h : x ∈ M) : mk' S x y * mk' S (y
   mk'_mul_mk'_eq_one ⟨x, h⟩ _
 #align is_localization.mk'_mul_mk'_eq_one' IsLocalization.mk'_mul_mk'_eq_one'
 
-theorem smul_mk' (x y : R) (m : M) : x • mk' S y m = mk' S (x * y) m  := by
+theorem smul_mk' (x y : R) (m : M) : x • mk' S y m = mk' S (x * y) m := by
   nth_rw 2 [← one_mul m]
   rw [mk'_mul, mk'_one, Algebra.smul_def]
 

Mathlib/SetTheory/Lists.lean

@@ -402,7 +402,7 @@ mutual
           by decreasing_tactic
         Subset.decidable l₂ l₁
       exact decidable_of_iff' _ Equiv.antisymm_iff
-  instance Subset.decidable  : ∀ l₁ l₂ : Lists' α true, Decidable (l₁ ⊆ l₂)
+  instance Subset.decidable : ∀ l₁ l₂ : Lists' α true, Decidable (l₁ ⊆ l₂)
     | Lists'.nil, l₂ => isTrue Lists'.Subset.nil
     | @Lists'.cons' _ b a l₁, l₂ => by
       haveI :=
@@ -414,7 +414,7 @@ mutual
           by decreasing_tactic
         Subset.decidable l₁ l₂
       exact decidable_of_iff' _ (@Lists'.cons_subset _ ⟨_, _⟩ _ _)
-  instance mem.decidable  : ∀ (a : Lists α) (l : Lists' α true), Decidable (a ∈ l)
+  instance mem.decidable : ∀ (a : Lists α) (l : Lists' α true), Decidable (a ∈ l)
     | a, Lists'.nil => isFalse <| by rintro ⟨_, ⟨⟩, _⟩
     | a, Lists'.cons' b l₂ => by
       haveI :=

Mathlib/Tactic/Explode.lean

@@ -64,15 +64,15 @@ partial def explodeCore (e : Expr) (depth : Nat) (entries : Entries) (start : Bo
       let mut rdeps := []
       for arg in args, i in [0:args.size] do
         let (argEntry, entries'') := entries'.add arg
-          { type    := ← addMessageContext <| ← Meta.inferType arg
-            depth   := depth
-            status  :=
+          { type     := ← addMessageContext <| ← Meta.inferType arg
+            depth    := depth
+            status   :=
               if start
               then Status.sintro
               else if i == 0 then Status.intro else Status.cintro
-            thm     := ← addMessageContext <| arg
-            deps    := []
-            useAsDep  := ← select arg }
+            thm      := ← addMessageContext <| arg
+            deps     := []
+            useAsDep := ← select arg }
         entries' := entries''
         rdeps := some argEntry.line! :: rdeps
       let (bodyEntry?, entries) ←

Mathlib/Tactic/Simps/Basic.lean

@@ -90,7 +90,7 @@ def mkSimpContextResult (cfg : Meta.Simp.Config := {}) (simpOnly := false) (kind
     getSimpTheorems
   let congrTheorems ← getSimpCongrTheorems
   let ctx : Simp.Context := {
-    config      := cfg
+    config       := cfg
     simpTheorems := #[simpTheorems], congrTheorems
   }
   if !hasStar then

Mathlib/Testing/SlimCheck/Testable.lean

@@ -217,7 +217,7 @@ def addInfo (x : String) (h : q → p) (r : TestResult p)
 
 /-- Add some formatting to the information recorded by `addInfo`. -/
 def addVarInfo [Repr γ] (var : String) (x : γ) (h : q → p) (r : TestResult p)
-    (p : PSum Unit (p → q) := PSum.inl ()) : TestResult q  :=
+    (p : PSum Unit (p → q) := PSum.inl ()) : TestResult q :=
   addInfo s!"{var} := {repr x}" h r p
 
 def isFailure : TestResult p → Bool

Mathlib/Topology/Algebra/ValuedField.lean

@@ -171,7 +171,7 @@ instance (priority := 100) completable : CompletableTopField K :=
         simp only [mem_setOf_eq]
         specialize H₁ x x_in₁ y y_in₁
         replace x_in₀ := H₀ x x_in₀
-        replace  := H₀ y y_in₀
+        replace := H₀ y y_in₀
         clear H₀
         apply Valuation.inversion_estimate
         · have : (v x : Γ₀) ≠ 0 := by

Mathlib/Topology/Order/Category/AlexDisc.lean

@@ -57,7 +57,7 @@ end AlexDisc
 
 /-- Sends a topological space to its specialisation order. -/
 @[simps]
-def alexDiscEquivPreord  : AlexDisc ≌ Preord where
+def alexDiscEquivPreord : AlexDisc ≌ Preord where
   functor := forget₂ _ _ ⋙ topToPreord
   inverse := { obj := λ X ↦ AlexDisc.of (WithUpperSet X), map := WithUpperSet.map }
   unitIso := NatIso.ofComponents λ X ↦ AlexDisc.Iso.mk $ by