chore(Topology): fix whitespace (#32963)

Found by extending the commandStart linter to proof bodies.

Author: harahu

Mathlib/Topology/Algebra/Algebra.lean

@@ -146,7 +146,7 @@ instance : AlgHomClass (A →A[R] B) R A B where
 theorem toAlgHom_eq_coe (f : A →A[R] B) : f.toAlgHom = f := rfl
 
 @[simp, norm_cast]
-theorem coe_inj {f g : A →A[R] B} : (f : A →ₐ[R] B) = g ↔ f = g :=   by
+theorem coe_inj {f g : A →A[R] B} : (f : A →ₐ[R] B) = g ↔ f = g := by
   cases f; cases g; simp only [mk.injEq]; exact Eq.congr_right rfl
 
 @[simp]
@@ -294,14 +294,14 @@ theorem one_def : (1 : A →A[R] A) = ContinuousAlgHom.id R A := rfl
 theorem id_apply (x : A) : ContinuousAlgHom.id R A x = x := rfl
 
 @[simp, norm_cast]
-theorem coe_id : ((ContinuousAlgHom.id R A) : A →ₐ[R] A) = AlgHom.id R A:= rfl
+theorem coe_id : ((ContinuousAlgHom.id R A) : A →ₐ[R] A) = AlgHom.id R A := rfl
 
 @[simp, norm_cast]
-theorem coe_id' : ⇑(ContinuousAlgHom.id R A ) = _root_.id := rfl
+theorem coe_id' : ⇑(ContinuousAlgHom.id R A) = _root_.id := rfl
 
 @[simp, norm_cast]
 theorem coe_eq_id {f : A →A[R] A} :
-    (f : A →ₐ[R] A) = AlgHom.id R A ↔ f = ContinuousAlgHom.id R A:= by
+    (f : A →ₐ[R] A) = AlgHom.id R A ↔ f = ContinuousAlgHom.id R A := by
   rw [← coe_id, coe_inj]
 
 @[simp]
@@ -490,11 +490,11 @@ theorem coe_codRestrict_apply (f : A →A[R] B) (p : Subalgebra R B) (h : ∀ x,
 /-- Restrict the codomain of a continuous algebra homomorphism `f` to `f.range`. -/
 @[reducible]
 def rangeRestrict (f : A →A[R] B) :=
-  f.codRestrict (@AlgHom.range R A B  _ _ _ _ _ f) (@AlgHom.mem_range_self R A B  _ _ _ _ _ f)
+  f.codRestrict (@AlgHom.range R A B _ _ _ _ _ f) (@AlgHom.mem_range_self R A B _ _ _ _ _ f)
 
 @[simp]
 theorem coe_rangeRestrict (f : A →A[R] B) :
-    (f.rangeRestrict : A →ₐ[R] (@AlgHom.range R A B  _ _ _ _ _ f)) =
+    (f.rangeRestrict : A →ₐ[R] (@AlgHom.range R A B _ _ _ _ _ f)) =
       (f : A →ₐ[R] B).rangeRestrict :=
   rfl
 

Mathlib/Topology/Algebra/AsymptoticCone.lean

@@ -369,13 +369,13 @@ of direction `v` starting from `p` is contained in `s`. -/
 theorem Convex.smul_vadd_mem_of_mem_nhds_of_mem_asymptoticCone {c : k} {v p : V}
     (hs : Convex k s) (hc : 0 ≤ c) (hp : s ∈ 𝓝 p) (hv : v ∈ asymptoticCone k s) :
     c • v +ᵥ p ∈ s := by
-  rw [mem_asymptoticCone_iff, asymptoticNhds_eq_smul_vadd v (c • v +ᵥ p),  vadd_pure,
+  rw [mem_asymptoticCone_iff, asymptoticNhds_eq_smul_vadd v (c • v +ᵥ p), vadd_pure,
     frequently_map, ← map₂_smul, ← map_prod_eq_map₂, frequently_map] at hv
   refine frequently_const.mp (hv.mp ?_)
-  have : Tendsto (fun u => - (c • u : V) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p) :=
+  have : Tendsto (fun u => -(c • u : V) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p) :=
     Continuous.tendsto' (by fun_prop) _ _ (by simp)
   filter_upwards [tendsto_fst.eventually <| eventually_gt_atTop 0, this.comp tendsto_snd hp]
-    with ⟨t, u⟩ (ht : 0 < t) (hu : - (c • u) +ᵥ c • v +ᵥ p ∈ s) (h : t • u +ᵥ c • v +ᵥ p ∈ s)
+    with ⟨t, u⟩ (ht : 0 < t) (hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s) (h : t • u +ᵥ c • v +ᵥ p ∈ s)
   apply hs.segment_subset hu h
   simp_rw [mem_segment_iff_sameRay, ← vsub_eq_sub]
   rw [vsub_vadd_eq_vsub_sub, vsub_self, zero_sub, neg_neg, vadd_vsub]

Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean

@@ -209,7 +209,7 @@ abbrev ofProfinite (G : Profinite) [Group G] [IsTopologicalGroup G] :
 profinite additive group. -/]
 def pi {α : Type u} (β : α → ProfiniteGrp) : ProfiniteGrp :=
   let pitype := Profinite.pi fun (a : α) => (β a).toProfinite
-  letI (a : α): Group (β a).toProfinite := (β a).group
+  letI (a : α) : Group (β a).toProfinite := (β a).group
   letI : Group pitype := Pi.group
   letI : IsTopologicalGroup pitype := Pi.topologicalGroup
   ofProfinite pitype

Mathlib/Topology/Algebra/Field.lean

@@ -160,7 +160,7 @@ open Topology
 
 theorem IsLocalMin.inv {f : α → β} {a : α} (h1 : IsLocalMin f a) (h2 : ∀ᶠ z in 𝓝 a, 0 < f z) :
     IsLocalMax f⁻¹ a := by
-  filter_upwards [h1, h2] with z h3 h4 using(inv_le_inv₀ h4 h2.self_of_nhds).mpr h3
+  filter_upwards [h1, h2] with z h3 h4 using (inv_le_inv₀ h4 h2.self_of_nhds).mpr h3
 
 end LocalExtr
 

Mathlib/Topology/Algebra/InfiniteSum/ConditionalInt.lean

@@ -118,7 +118,7 @@ lemma symmetricIcc_eq_symmetricIoo_int : symmetricIcc ℤ = symmetricIoo ℤ :=
   simp only [← Nat.map_cast_int_atTop, Filter.map_map, Filter.mem_map, mem_atTop_sets, ge_iff_le,
     Set.mem_preimage, comp_apply]
   refine ⟨fun ⟨a, ha⟩ ↦ ⟨a + 1, fun b hb ↦ ?_⟩, fun ⟨a, ha⟩ ↦ ⟨a - 1, fun b hb ↦ ?_⟩⟩ <;>
-  [ convert ha (b - 1) (by grind) using 1; convert ha (b + 1) (by grind) using 1 ] <;>
+  [convert ha (b - 1) (by grind) using 1; convert ha (b + 1) (by grind) using 1] <;>
   simpa [Finset.ext_iff] using by grind
 
 @[to_additive]

Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean

@@ -320,7 +320,7 @@ theorem hasSum_unop {f : β → αᵐᵒᵖ} {a : αᵐᵒᵖ} :
   ⟨HasSum.op, HasSum.unop⟩
 
 @[simp]
-theorem summable_op : (Summable (fun a ↦ op (f a)) L) ↔ Summable f L:=
+theorem summable_op : (Summable (fun a ↦ op (f a)) L) ↔ Summable f L :=
   ⟨Summable.unop, Summable.op⟩
 
 theorem summable_unop {f : β → αᵐᵒᵖ} : (Summable (fun a ↦ unop (f a)) L) ↔ Summable f L :=

Mathlib/Topology/Algebra/InfiniteSum/Group.lean

@@ -46,7 +46,7 @@ theorem Multipliable.of_inv (hf : Multipliable (fun b ↦ (f b)⁻¹) L) : Multi
   simpa only [inv_inv] using hf.inv
 
 @[to_additive]
-theorem multipliable_inv_iff : (Multipliable (fun b ↦ (f b)⁻¹) L) ↔ Multipliable f L:=
+theorem multipliable_inv_iff : (Multipliable (fun b ↦ (f b)⁻¹) L) ↔ Multipliable f L :=
   ⟨Multipliable.of_inv, Multipliable.inv⟩
 
 @[to_additive]

Mathlib/Topology/Algebra/InfiniteSum/Module.lean

@@ -125,7 +125,7 @@ protected theorem ContinuousLinearMap.hasSum {f : ι → M} (φ : M →SL[σ] M
 alias HasSum.mapL := ContinuousLinearMap.hasSum
 
 protected theorem ContinuousLinearMap.summable {f : ι → M} (φ : M →SL[σ] M₂) (hf : Summable f L) :
-    Summable (fun b : ι ↦ φ (f b)) L:=
+    Summable (fun b : ι ↦ φ (f b)) L :=
   (hf.hasSum.mapL φ).summable
 
 alias Summable.mapL := ContinuousLinearMap.summable

Mathlib/Topology/Algebra/InfiniteSum/Ring.lean

@@ -84,7 +84,7 @@ theorem HasSum.div_const (h : HasSum f a L) (b : α) : HasSum (fun i ↦ f i / b
 theorem Summable.div_const (h : Summable f L) (b : α) : Summable (fun i ↦ f i / b) L :=
   (h.hasSum.div_const _).summable
 
-theorem hasSum_mul_left_iff (h : a₂ ≠ 0) : HasSum (fun i ↦ a₂ * f i) (a₂ * a₁) L ↔ HasSum f a₁ L:=
+theorem hasSum_mul_left_iff (h : a₂ ≠ 0) : HasSum (fun i ↦ a₂ * f i) (a₂ * a₁) L ↔ HasSum f a₁ L :=
   ⟨fun H ↦ by simpa only [inv_mul_cancel_left₀ h] using H.mul_left a₂⁻¹, HasSum.mul_left _⟩
 
 theorem hasSum_mul_right_iff (h : a₂ ≠ 0) : HasSum (fun i ↦ f i * a₂) (a₁ * a₂) L ↔ HasSum f a₁ L :=
@@ -97,7 +97,7 @@ theorem hasSum_div_const_iff (h : a₂ ≠ 0) :
 theorem summable_mul_left_iff (h : a ≠ 0) : (Summable (fun i ↦ a * f i) L) ↔ Summable f L :=
   ⟨fun H ↦ by simpa only [inv_mul_cancel_left₀ h] using H.mul_left a⁻¹, fun H ↦ H.mul_left _⟩
 
-theorem summable_mul_right_iff (h : a ≠ 0) : (Summable (fun i ↦ f i * a) L) ↔ Summable f L:=
+theorem summable_mul_right_iff (h : a ≠ 0) : (Summable (fun i ↦ f i * a) L) ↔ Summable f L :=
   ⟨fun H ↦ by simpa only [mul_inv_cancel_right₀ h] using H.mul_right a⁻¹, fun H ↦ H.mul_right _⟩
 
 theorem summable_div_const_iff (h : a ≠ 0) : (Summable (fun i ↦ f i / a) L) ↔ Summable f L := by
@@ -129,7 +129,7 @@ theorem Summable.const_div (h : Summable (fun x ↦ 1 / f x) L) (b : α) :
   (h.hasSum.const_div b).summable
 
 theorem hasSum_const_div_iff (h : a₂ ≠ 0) :
-    HasSum (fun i ↦ a₂ / f i) (a₂ * a₁) L ↔ HasSum (1/ f) a₁ L := by
+    HasSum (fun i ↦ a₂ / f i) (a₂ * a₁) L ↔ HasSum (1 / f) a₁ L := by
   simpa only [div_eq_mul_inv, one_mul] using hasSum_mul_left_iff h
 
 theorem summable_const_div_iff (h : a ≠ 0) :

Mathlib/Topology/Algebra/InfiniteSum/TsumUniformlyOn.lean

@@ -33,7 +33,7 @@ section UniformlyOn
 variable {α β F : Type*} [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ}
 
 theorem HasSumUniformlyOn.of_norm_le_summable {f : α → β → F} (hu : Summable u) {s : Set β}
-    (hfu : ∀ n x, x ∈ s → ‖f n x‖ ≤ u n) : HasSumUniformlyOn f (fun x ↦ ∑' n, f n x) s :=  by
+    (hfu : ∀ n x, x ∈ s → ‖f n x‖ ≤ u n) : HasSumUniformlyOn f (fun x ↦ ∑' n, f n x) s := by
   simp [hasSumUniformlyOn_iff_tendstoUniformlyOn, tendstoUniformlyOn_tsum hu hfu]
 
 theorem HasSumUniformlyOn.of_norm_le_summable_eventually {ι : Type*} {f : ι → β → F} {u : ι → ℝ}
@@ -101,7 +101,7 @@ theorem iteratedDerivWithin_tsum {f : ι → 𝕜 → F} (m : ℕ) (hs : IsOpen
   | zero => simp
   | succ m hm =>
     simp_rw [iteratedDerivWithin_succ]
-    rw [← derivWithin_tsum hs hx _  _ (fun n r hr ↦ hf2 n m r (by lia) hr)]
+    rw [← derivWithin_tsum hs hx _ _ (fun n r hr ↦ hf2 n m r (by lia) hr)]
     · exact derivWithin_congr (fun t ht ↦ hm ht (fun k hk1 hkm ↦ h k hk1 (by lia))
           (fun k r e hr he ↦ hf2 k r e (by lia) he)) (hm hx (fun k hk1 hkm ↦ h k hk1 (by lia))
           (fun k r e hr he ↦ hf2 k r e (by lia) he))