chore: fix more whitespace formatting (leanprover-community#33342)

Found by extending the commandStart linter to proof bodies. Extracted from leanprover-community#30658.

Author: grunweg

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

@@ -324,7 +324,7 @@ instance {J : Type*} [Category* J] {F : J ⥤ TopModuleCat.{v} R}
     PreservesLimit F (forget₂ _ TopCat) :=
   preservesLimit_of_preserves_limit_cone (isLimit (limit.isLimit _))
     (TopCat.isLimitConeOfForget (F := F ⋙ forget₂ _ TopCat)
-      ((forget _).mapCone (getLimitCone (F ⋙ forget₂ _ (ModuleCat.{v} R))).1:)
+      ((forget _).mapCone (getLimitCone (F ⋙ forget₂ _ (ModuleCat.{v} R))).1 :)
       (isLimitOfPreserves (forget (ModuleCat R)) (limit.isLimit _)))
 
 instance {J : Type*} [Category* J]

Mathlib/Algebra/Lie/Sl2.lean

@@ -143,7 +143,7 @@ lemma mem_toLieSubalgebra_iff {x : L} {t : IsSl2Triple h e f} :
 namespace HasPrimitiveVectorWith
 
 variable {m : M} {μ : R} {t : IsSl2Triple h e f}
-local notation "ψ" n => ((toEnd R L M f) ^ n) m
+local notation "ψ " n => ((toEnd R L M f) ^ n) m
 
 -- Although this is true by definition, we include this lemma (and the assumption) to mirror the API
 -- for `lie_h_pow_toEnd_f` and `lie_e_pow_succ_toEnd_f`.

Mathlib/Algebra/Pointwise/Stabilizer.lean

@@ -242,8 +242,8 @@ variable {G : Type*} [CommGroup G] (s : Set G)
 @[to_additive (attr := simp)]
 lemma mul_stabilizer_self : s * stabilizer G s = s := by rw [mul_comm, stabilizer_mul_self]
 
-local notation " Q " => G ⧸ stabilizer G s
-local notation " q " => ((↑) : G → Q)
+local notation "Q" => G ⧸ stabilizer G s
+local notation "q" => ((↑) : G → Q)
 
 @[to_additive]
 lemma stabilizer_image_coe_quotient : stabilizer Q (q '' s) = ⊥ := by

Mathlib/Algebra/Polynomial/CoeffMem.lean

@@ -24,7 +24,7 @@ of `q`.
 namespace Polynomial
 variable {ι R S : Type*} [CommRing R] [Ring S] [Algebra R S]
 
-local notation "deg("p")" => natDegree p
+local notation3 "deg("p")" => natDegree p
 local notation3 "coeffs("p")" => Set.range (coeff p)
 local notation3 "spanCoeffs("p")" => 1 ⊔ Submodule.span R coeffs(p)
 

Mathlib/Algebra/Polynomial/Roots.lean

@@ -663,7 +663,7 @@ lemma eq_of_natDegree_lt_card_of_eval_eq {R} [CommRing R] [IsDomain R]
     (p q : R[X]) {ι} [Fintype ι] {f : ι → R} (hf : Function.Injective f)
     (heval : ∀ i : ι, eval (f i) p = eval (f i) q)
     (hcard : max p.natDegree q.natDegree < Fintype.card ι) : p = q := by
-  rw [←sub_eq_zero]
+  rw [← sub_eq_zero]
   apply eq_zero_of_natDegree_lt_card_of_eval_eq_zero _ hf
   · simpa [sub_eq_zero]
   · grind [natDegree_sub_le]

Mathlib/Algebra/QuadraticDiscriminant.lean

@@ -70,7 +70,7 @@ theorem quadratic_eq_zero_iff_discrim_eq_sq [NeZero (2 : R)] [NoZeroDivisors R]
   linear_combination -h
 
 /-- A quadratic has no root if its discriminant has no square root. -/
-theorem quadratic_ne_zero_of_discrim_ne_sq (h : ∀ s : R, discrim a b c ≠ s^2) (x : R) :
+theorem quadratic_ne_zero_of_discrim_ne_sq (h : ∀ s : R, discrim a b c ≠ s ^ 2) (x : R) :
     a * (x * x) + b * x + c ≠ 0 :=
   mt discrim_eq_sq_of_quadratic_eq_zero (h _)
 

Mathlib/Algebra/Vertex/VertexOperator.lean

@@ -69,7 +69,7 @@ theorem coeff_eq_ncoeff (A : VertexOperator R V)
 @[deprecated (since := "2025-08-30")] alias ncoeff_smul := map_smul
 
 theorem ncoeff_eq_zero_of_lt_order (A : VertexOperator R V) (n : ℤ) (x : V)
-    (h : -n - 1 < HahnSeries.order ((HahnModule.of R).symm (A x))) : (A [[n]]) x = 0 := by
+    (h : -n - 1 < HahnSeries.order ((HahnModule.of R).symm (A x))) : (A[[n]]) x = 0 := by
   simp only [ncoeff, HVertexOperator.coeff, LinearMap.coe_mk, AddHom.coe_mk]
   exact HahnSeries.coeff_eq_zero_of_lt_order h
 
@@ -96,7 +96,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 : ℤ) :
-    (of_coeff f hf) [[n]] = f (-n - 1) := by
+    (of_coeff f hf)[[n]] = f (-n - 1) := by
   ext v
   rw [ncoeff_apply, coeff_apply_apply, of_coeff_apply_coeff]
 

Mathlib/AlgebraicGeometry/AffineSpace.lean

@@ -39,7 +39,7 @@ universe v u
 variable (n : Type v) (S : Scheme.{max u v})
 
 local notation3 "ℤ[" n "]" => CommRingCat.of (MvPolynomial n (ULift ℤ))
-local notation3 "ℤ[" n "].{" u "," v "}" => CommRingCat.of (MvPolynomial n (ULift.{max u v} ℤ))
+local notation3 "ℤ[" n "].{" u ", " v "}" => CommRingCat.of (MvPolynomial n (ULift.{max u v} ℤ))
 
 /-- `𝔸(n; S)` is the affine `n`-space over `S`.
 Note that `n` is an arbitrary index type (e.g. `Fin m`). -/
@@ -49,7 +49,7 @@ def AffineSpace (n : Type v) (S : Scheme.{max u v}) : Scheme.{max u v} :=
 namespace AffineSpace
 
 /-- `𝔸(n; S)` is the affine `n`-space over `S`. -/
-scoped[AlgebraicGeometry] notation "𝔸("n"; "S")" => AffineSpace n S
+scoped[AlgebraicGeometry] notation "𝔸(" n "; " S ")" => AffineSpace n S
 
 variable {n} in
 lemma of_mvPolynomial_int_ext {R} {f g : ℤ[n] ⟶ R} (h : ∀ i, f (.X i) = g (.X i)) : f = g := by

Mathlib/Analysis/Analytic/Constructions.lean

@@ -449,7 +449,7 @@ lemma FormalMultilinearSeries.le_radius_pi (h : ∀ i, r ≤ (p i).radius) :
     ⟨∑ i, C i, Finset.sum_nonneg (fun i _ ↦ (C_pos i).le),
       fun i ↦ Finset.single_le_sum (fun j _ ↦ (C_pos j).le) (Finset.mem_univ _)⟩
   apply le_radius_of_bound _ D (fun n ↦ ?_)
-  rcases le_or_gt ((r' : ℝ)^n) 0 with hr' | hr'
+  rcases le_or_gt ((r' : ℝ) ^ n) 0 with hr' | hr'
   · exact le_trans (mul_nonpos_of_nonneg_of_nonpos (by positivity) hr') D_nonneg
   · simp only [pi]
     rw [← le_div_iff₀ hr', ContinuousMultilinearMap.opNorm_pi,

Mathlib/Analysis/Calculus/LogDeriv.lean

@@ -87,7 +87,7 @@ lemma logDeriv_fun_zpow {f : 𝕜 → 𝕜'} {x : 𝕜} (hdf : DifferentiableAt
   rcases eq_or_ne n 0 with rfl | hn; · simp
   rcases eq_or_ne (f x) 0 with hf | hf
   · simp [logDeriv_apply, zero_zpow, *]
-  · rw [logDeriv_apply, ← comp_def (·^n), deriv_comp _ (differentiableAt_zpow.2 <| .inl hf) hdf,
+  · rw [logDeriv_apply, ← comp_def (· ^ n), deriv_comp _ (differentiableAt_zpow.2 <| .inl hf) hdf,
       deriv_zpow, logDeriv_apply]
     simp [field, zpow_sub_one₀ hf]