chore: fix whitespace (#33155)

Found by extending the commandStart linter to proof bodies.

Author: harahu

Mathlib/FieldTheory/Extension.lean

@@ -158,7 +158,7 @@ theorem union_isExtendible [alg : Algebra.IsAlgebraic F E]
     · exact (this _ _ <| (hc.total π₁.2 π₂.2).resolve_left h).symm
     refine .inl (le_iff.mpr ⟨?_, algHom_ext_of_eq_adjoin _ (eq _) ?_⟩)
     · rw [eq, eq]; exact adjoin.mono _ _ _ (Set.union_subset_union_left _ h.1)
-    rintro x (hx|hx)
+    rintro x (hx | hx)
     · change (θ π₂).emb (inclusion (ge π₂).1 <| inclusion h.1 ⟨x, hx⟩) =
         (θ π₁).emb (inclusion (ge π₁).1 ⟨x, hx⟩)
       rw [(ge π₁).2, (ge π₂).2, h.2]

Mathlib/FieldTheory/JacobsonNoether.lean

@@ -122,9 +122,9 @@ theorem exists_separable_and_not_isCentral (H : k ≠ (⊤ : Subring D)) :
     change a * ha.choose - ha.choose * a ≠ 0
     simpa only [ne_eq, sub_eq_zero] using Ne.symm ha.choose_spec
   -- We find a maximum natural number `n` such that `(a * x - x * a) ^ n b ≠ 0`.
-  obtain ⟨n, hn, hb⟩ : ∃ n, 0 < n ∧ (ad k D a)^[n] b ≠ 0 ∧ (ad k D a)^[n+1] b = 0 := by
+  obtain ⟨n, hn, hb⟩ : ∃ n, 0 < n ∧ (ad k D a)^[n] b ≠ 0 ∧ (ad k D a)^[n + 1] b = 0 := by
     obtain ⟨m, -, hm2⟩ := exist_pow_eq_zero_of_le p ha insep
-    have h_exist : ∃ n, 0 < n ∧ (ad k D a)^[n+1] b = 0 := ⟨p ^ m,
+    have h_exist : ∃ n, 0 < n ∧ (ad k D a)^[n + 1] b = 0 := ⟨p ^ m,
       ⟨expChar_pow_pos D p m, by rw [hm2 (p ^ m + 1) (Nat.le_add_right _ _), Pi.zero_apply]⟩⟩
     classical
     refine ⟨Nat.find h_exist, ⟨(Nat.find_spec h_exist).1, ?_, (Nat.find_spec h_exist).2⟩⟩

Mathlib/FieldTheory/PurelyInseparable/Basic.lean

@@ -664,7 +664,7 @@ lemma IsPurelyInseparable.exists_pow_pow_mem_range_tensorProduct_of_expChar
     [IsPurelyInseparable k K] (q : ℕ) [ExpChar k q] (x : R ⊗[k] K) :
     ∃ n, x ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range := by
   nontriviality (R ⊗[k] K)
-  obtain (hq|hq) := expChar_is_prime_or_one k q
+  obtain (hq | hq) := expChar_is_prime_or_one k q
   induction x with
   | zero => exact ⟨0, 0, by simp⟩
   | add x y h h' =>
@@ -691,6 +691,6 @@ lemma IsPurelyInseparable.exists_pow_mem_range_tensorProduct [IsPurelyInseparabl
   let q := ringExpChar k
   obtain ⟨n, hr⟩ := exists_pow_pow_mem_range_tensorProduct_of_expChar q x
   refine ⟨q ^ n, pow_pos ?_ _, hr⟩
-  obtain (hq|hq) := expChar_is_prime_or_one k q <;> simp [hq, Nat.Prime.pos]
+  obtain (hq | hq) := expChar_is_prime_or_one k q <;> simp [hq, Nat.Prime.pos]
 
 end

Mathlib/GroupTheory/ArchimedeanDensely.lean

@@ -129,10 +129,10 @@ noncomputable def LinearOrderedCommGroup.closure_equiv_closure {G G' : Type*}
     have ypos : 1 < y' := by
       simp [hy', eq_comm, ← hxy, hx]
     have hxc : closure {x} = closure {x'} := by
-      rcases max_cases x x⁻¹ with H|H <;>
+      rcases max_cases x x⁻¹ with H | H <;>
       simp [hx', H.left]
     have hyc : closure {y} = closure {y'} := by
-      rcases max_cases y y⁻¹ with H|H <;>
+      rcases max_cases y y⁻¹ with H | H <;>
       simp [hy', H.left]
     refine ⟨⟨⟨
       fun a ↦ ⟨y' ^ ((mem_closure_singleton).mp
@@ -182,7 +182,7 @@ lemma Subgroup.isLeast_of_closure_iff_eq_mabs {a b : G} :
       rw [← zpow_right_inj this.right, zpow_mul', hm, zpow_one]
     rw [Int.mul_eq_one_iff_eq_one_or_neg_one] at key
     rw [eq_comm]
-    rcases key with ⟨rfl, rfl⟩|⟨rfl, rfl⟩ <;>
+    rcases key with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ <;>
     simp [this.right.le, this.right, mabs]
   · wlog ha : 1 ≤ a generalizing a
     · convert @this (a⁻¹) ?_ (by simpa using le_of_not_ge ha) using 4
@@ -269,7 +269,7 @@ lemma LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered (G : Type*)
     [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] :
     Nonempty (G ≃+o ℤ) ↔ ¬ DenselyOrdered G := by
   suffices ∀ (_ : G ≃+o ℤ), ¬ DenselyOrdered G by
-    rcases LinearOrderedAddCommGroup.discrete_or_denselyOrdered G with ⟨⟨h⟩⟩|h
+    rcases LinearOrderedAddCommGroup.discrete_or_denselyOrdered G with ⟨⟨h⟩⟩ | h
     · simpa [this h] using ⟨h⟩
     · simp only [h, not_true_eq_false, iff_false, not_nonempty_iff]
       exact ⟨fun H ↦ (this H) h⟩

Mathlib/GroupTheory/Coxeter/Basic.lean

@@ -453,13 +453,13 @@ lemma listTake_alternatingWord (i j : B) (p k : ℕ) (h : k < 2 * p) :
         simp only [Nat.not_even_iff_odd.mpr (Even.add_one h_even), ↓reduceIte]
         rw [← List.take_concat_get (by simp; lia), alternatingWord_succ, ← hk]
         apply congr_arg
-        rw [getElem_alternatingWord i j (2*p) k (by lia)]
+        rw [getElem_alternatingWord i j (2 * p) k (by lia)]
         simp [(by apply Nat.even_add.mpr; simp [h_even] : Even (2 * p + k))]
       · simp only [h_even, ↓reduceIte] at hk
         simp only [Odd.add_one (by simpa using h_even), ↓reduceIte]
         rw [← List.take_concat_get (by simp; lia), alternatingWord_succ, hk]
         apply congr_arg
-        rw [getElem_alternatingWord i j (2*p) k (by lia)]
+        rw [getElem_alternatingWord i j (2 * p) k (by lia)]
         simp [(by apply Nat.odd_add.mpr; simp [h_even] : Odd (2 * p + k))]
 
 lemma listTake_succ_alternatingWord (i j : B) (p : ℕ) (k : ℕ) (h : k + 1 < 2 * p) :

Mathlib/GroupTheory/Coxeter/Inversion.lean

@@ -481,7 +481,7 @@ theorem getElem_leftInvSeq_alternatingWord
     simp only [getElem_succ_leftInvSeq_alternatingWord cs i j p k h, hk _ _ (by lia),
       MulAut.conj_apply, inv_simple, alternatingWord_succ' j i, even_two, Even.mul_right,
       ↓reduceIte, wordProd_cons]
-    rw [(by ring: 2 * (k + 1) = 2 * k + 1 + 1), alternatingWord_succ j i, wordProd_concat]
+    rw [(by ring : 2 * (k + 1) = 2 * k + 1 + 1), alternatingWord_succ j i, wordProd_concat]
     simp [mul_assoc]
 
 end CoxeterSystem

Mathlib/GroupTheory/Perm/Cycle/PossibleTypes.lean

@@ -106,7 +106,7 @@ theorem Equiv.Perm.exists_with_cycleType_iff {m : Multiset ℕ} :
       apply List.map_congr_left
       intro x hx; simp only [Function.comp_apply]
       rw [List.support_formPerm_of_nodup x (hp_nodup x hx)]
-      ·-- length
+      · -- length
         rw [List.toFinset_card_of_nodup (hp_nodup x hx)]
       · -- length >= 1
         grind

Mathlib/GroupTheory/QuotientGroup/Basic.lean

@@ -271,7 +271,7 @@ noncomputable def quotientInfEquivProdNormalizerQuotient (H N : Subgroup G)
   letI := Subgroup.normal_subgroupOf_of_le_normalizer hLE
   letI := Subgroup.normal_subgroupOf_sup_of_le_normalizer hLE
   let
-    φ :-- φ is the natural homomorphism H →* (HN)/N.
+    φ : -- φ is the natural homomorphism H →* (HN)/N.
       H →*
       _ ⧸ N.subgroupOf (H ⊔ N) :=
     (mk' <| N.subgroupOf (H ⊔ N)).comp (inclusion le_sup_left)

Mathlib/GroupTheory/SpecificGroups/Alternating/MaximalSubgroups.lean

@@ -178,7 +178,7 @@ theorem subgroup_eq_top_of_isPreprimitive (h4 : 4 < Nat.card α)
   rw [eq_top_iff, ← Subgroup.map_subtype_le_map_subtype,
     ← MonoidHom.range_eq_map, Subgroup.range_subtype]
   -- By Jordan's theorem, it suffices to prove that G acts primitively
-  apply alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem  _ hg3
+  apply alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem _ hg3
   · use ⟨g, hg3.mem_alternatingGroup⟩
     simpa only [SetLike.mem_coe, Subgroup.subtype_apply, and_true] using hG hg
   · let φ := (alternatingGroup α).subtype.subgroupMap G