chore: whitespace fixes (#25956)

Found by #24465.

Author: adomani

Mathlib/Algebra/DirectSum/Internal.lean

@@ -468,7 +468,7 @@ variable [CanonicallyOrderedAdd ι]
 /-- The difference with `DirectSum.listProd_apply_eq_zero` is that the indices at which
 the terms of the list are zero is allowed to vary. -/
 theorem listProd_apply_eq_zero' {l : List ((⨁ i, A i) × ι)}
-    (hl : ∀ xn ∈ l, ∀ k < xn.2, xn.1 k = 0) ⦃n : ι⦄ (hn : n < (l.map Prod.snd).sum)  :
+    (hl : ∀ xn ∈ l, ∀ k < xn.2, xn.1 k = 0) ⦃n : ι⦄ (hn : n < (l.map Prod.snd).sum) :
     (l.map Prod.fst).prod n = 0 := by
   induction l generalizing n with
   | nil => simp [(zero_le n).not_gt] at hn
@@ -500,7 +500,7 @@ variable {A : ι → σ} [SetLike.GradedMonoid A]
 /-- The difference with `DirectSum.multisetProd_apply_eq_zero` is that the indices at which
 the terms of the multiset are zero is allowed to vary. -/
 theorem multisetProd_apply_eq_zero' {s : Multiset ((⨁ i, A i) × ι)}
-    (hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0) ⦃n : ι⦄ (hn : n < (s.map Prod.snd).sum)  :
+    (hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0) ⦃n : ι⦄ (hn : n < (s.map Prod.snd).sum) :
     (s.map Prod.fst).prod n = 0 := by
   have := listProd_apply_eq_zero' (l := s.toList) (by simpa using hs)
     (by simpa [← Multiset.sum_coe, ← Multiset.map_coe])
@@ -516,7 +516,7 @@ theorem multisetProd_apply_eq_zero {s : Multiset (⨁ i, A i)} {m : ι}
 /-- The difference with `DirectSum.finsetProd_apply_eq_zero` is that the indices at which
 the terms of the multiset are zero is allowed to vary. -/
 theorem finsetProd_apply_eq_zero' {s : Finset ((⨁ i, A i) × ι)}
-    (hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0) ⦃n : ι⦄ (hn : n < ∑ xn ∈ s, xn.2)  :
+    (hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0) ⦃n : ι⦄ (hn : n < ∑ xn ∈ s, xn.2) :
     (∏ xn ∈ s, xn.1) n = 0 := by
   simpa using listProd_apply_eq_zero' (l := s.toList) (by simpa using hs) (by simpa)
 

Mathlib/Analysis/Analytic/Order.lean

@@ -339,7 +339,7 @@ namespace AnalyticOnNhd
 variable {U : Set 𝕜} {f : 𝕜 → E}
 
 /-- The set where an analytic function has infinite order is clopen in its domain of analyticity. -/
-theorem isClopen_setOf_analyticOrderAt_eq_top  (hf : AnalyticOnNhd 𝕜 f U) :
+theorem isClopen_setOf_analyticOrderAt_eq_top (hf : AnalyticOnNhd 𝕜 f U) :
     IsClopen {u : U | analyticOrderAt f u = ⊤} := by
   constructor
   · rw [← isOpen_compl_iff, isOpen_iff_forall_mem_open]

Mathlib/Analysis/RCLike/TangentCone.lean

@@ -17,7 +17,7 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [h𝕜 : IsRCLikeNormedFi
 {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E]
 {s : Set E} {x : E}
 
-theorem tangentConeAt_real_subset_isRCLikeNormedField  :
+theorem tangentConeAt_real_subset_isRCLikeNormedField :
     tangentConeAt ℝ s x ⊆ tangentConeAt 𝕜 s x := by
   letI := h𝕜.rclike
   rintro y ⟨c, d, d_mem, c_lim, hcd⟩

Mathlib/CategoryTheory/Bicategory/Monad/Basic.lean

@@ -47,7 +47,7 @@ abbrev Comonad.comul {a : B} {t : a ⟶ a} [Comonad t] : t ⟶ t ≫ t := Comon_
 
 namespace Comonad
 
-variable {a: B}
+variable {a : B}
 
 /- Comonad laws -/
 section

Mathlib/CategoryTheory/FiberedCategory/HomLift.lean

@@ -172,7 +172,7 @@ variable {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f 
 instance comp_id_lift : p.IsHomLift f (𝟙 a ≫ φ) := by
   simp_all
 
-instance id_comp_lift  : p.IsHomLift f (φ ≫ 𝟙 b) := by
+instance id_comp_lift : p.IsHomLift f (φ ≫ 𝟙 b) := by
   simp_all
 
 instance lift_id_comp : p.IsHomLift (𝟙 R ≫ f) φ := by

Mathlib/CategoryTheory/Limits/Preserves/Bifunctor.lean

@@ -127,7 +127,7 @@ a colimit of `uncurry.obj (whiskeringLeft₂ C|>.obj K₁|>.obj K₂|>.obj G)` a
 noncomputable def isoObjCoconePointsOfIsColimit
     {c₁ : Cocone K₁} (hc₁ : IsColimit c₁)
     {c₂ : Cocone K₂} (hc₂ : IsColimit c₂)
-    {c₃ : Cocone <| uncurry.obj (whiskeringLeft₂ C|>.obj K₁|>.obj K₂|>.obj G)}
+    {c₃ : Cocone <| uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G)}
     (hc₃ : IsColimit c₃) :
     (G.obj c₁.pt).obj c₂.pt ≅ c₃.pt :=
   IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves₂ G hc₁ hc₂) hc₃
@@ -136,7 +136,7 @@ section
 
 variable {c₁ : Cocone K₁} (hc₁ : IsColimit c₁)
   {c₂ : Cocone K₂} (hc₂ : IsColimit c₂)
-  {c₃ : Cocone <| uncurry.obj (whiskeringLeft₂ C|>.obj K₁|>.obj K₂|>.obj G)}
+  {c₃ : Cocone <| uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G)}
   (hc₃ : IsColimit c₃)
 
 /-- Characterize the inverse direction of the isomorphism
@@ -255,7 +255,7 @@ a limit of `uncurry.obj (whiskeringLeft₂ C|>.obj K₁|>.obj K₂|>.obj G)` and
 noncomputable def isoObjConePointsOfIsLimit
     {c₁ : Cone K₁} (hc₁ : IsLimit c₁)
     {c₂ : Cone K₂} (hc₂ : IsLimit c₂)
-    {c₃ : Cone <| uncurry.obj (whiskeringLeft₂ C|>.obj K₁|>.obj K₂|>.obj G)}
+    {c₃ : Cone <| uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G)}
     (hc₃ : IsLimit c₃) :
     (G.obj c₁.pt).obj c₂.pt ≅ c₃.pt :=
   IsLimit.conePointUniqueUpToIso (isLimitOfPreserves₂ G hc₁ hc₂) hc₃
@@ -264,7 +264,7 @@ section
 
 variable {c₁ : Cone K₁} (hc₁ : IsLimit c₁)
   {c₂ : Cone K₂} (hc₂ : IsLimit c₂)
-  {c₃ : Cone <| uncurry.obj (whiskeringLeft₂ C|>.obj K₁|>.obj K₂|>.obj G)}
+  {c₃ : Cone <| uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G)}
   (hc₃ : IsLimit c₃)
 
 /-- Characterize the forward direction of the isomorphism

Mathlib/CategoryTheory/Monoidal/Internal/FunctorCategory.lean

@@ -53,7 +53,7 @@ def functorObjObj (A : C ⥤ D) [Mon_Class A] (X : C) : Mon_ D where
 
 /-- A monoid object in a functor category induces a functor to the category of monoid objects. -/
 @[simps]
-def functorObj (A : C ⥤ D) [Mon_Class A]  : C ⥤ Mon_ D where
+def functorObj (A : C ⥤ D) [Mon_Class A] : C ⥤ Mon_ D where
   obj := functorObjObj A
   map f :=
     { hom := A.map f

Mathlib/Combinatorics/Quiver/Path.lean

@@ -217,7 +217,7 @@ def decidableEqBddPathsZero (v w : V) : DecidableEq (BoundedPaths v w 0) :=
 /-- Given decidable equality on paths of length up to `n`, we can construct
 decidable equality on paths of length up to `n + 1`. -/
 def decidableEqBddPathsOfDecidableEq (n : ℕ) (h₁ : DecidableEq V)
-    (h₂ : ∀ (v w : V), DecidableEq (v ⟶  w)) (h₃ : ∀ (v w : V), DecidableEq (BoundedPaths v w n))
+    (h₂ : ∀ (v w : V), DecidableEq (v ⟶ w)) (h₃ : ∀ (v w : V), DecidableEq (BoundedPaths v w n))
     (v w : V) : DecidableEq (BoundedPaths v w (n + 1)) :=
   fun ⟨p, hp⟩ ⟨q, hq⟩ =>
     match v, w, p, q with

Mathlib/Deprecated/RingHom.lean

@@ -27,7 +27,7 @@ variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} (f : α →+* β)
 
 /-- `f : α →+* β` has a trivial codomain iff its range is `{0}`. -/
 @[deprecated "Use range_eq_singleton_iff and codomain_trivial_iff_range_trivial"
-    (since := "2025-06-09") ]
+    (since := "2025-06-09")]
 theorem codomain_trivial_iff_range_eq_singleton_zero : (0 : β) = 1 ↔ Set.range f = {0} :=
   f.codomain_trivial_iff_range_trivial.trans
     ⟨fun h =>
@@ -39,7 +39,7 @@ end
 section Semiring
 
 variable [Semiring α] [Semiring β]
-@[deprecated map_dvd (since := "2025-06-09") ]
+@[deprecated map_dvd (since := "2025-06-09")]
 protected theorem map_dvd (f : α →+* β) {a b : α} : a ∣ b → f a ∣ f b :=
   map_dvd f
 

Mathlib/Order/RelClasses.lean

@@ -659,11 +659,11 @@ theorem ssuperset_imp_ssuperset (h₁ : a ⊆ c) (h₂ : d ⊆ b) : a ⊃ b →
   ssubset_imp_ssubset h₂ h₁
 
 @[gcongr]
-theorem ssuperset_imp_ssuperset_left  (h : a ⊆ b) : c ⊃ b → c ⊃ a :=
+theorem ssuperset_imp_ssuperset_left (h : a ⊆ b) : c ⊃ b → c ⊃ a :=
   ssubset_of_subset_of_ssubset h
 
 @[gcongr]
-theorem ssuperset_imp_ssuperset_right  (h : a ⊆ b) : a ⊃ c → b ⊃ c :=
+theorem ssuperset_imp_ssuperset_right (h : a ⊆ b) : a ⊃ c → b ⊃ c :=
   ssubset_imp_ssubset_right h
 
 /-- See if the term is `a ⊂ b` and the goal is `a ⊆ b`. -/