[Merged by Bors] - style(misc): fix whitespace

Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean

@@ -222,7 +222,7 @@ theorem nonUniforms_bot (hε : 0 < ε) : (⊥ : Finpartition A).nonUniforms G ε
   rintro ⟨u, v⟩
   simp only [mk_mem_nonUniforms, parts_bot, mem_map, not_and,
     Classical.not_not, exists_imp]; dsimp
-  rintro x ⟨_, rfl⟩ y ⟨_,rfl⟩ _
+  rintro x ⟨_, rfl⟩ y ⟨_, rfl⟩ _
   rwa [SimpleGraph.isUniform_singleton]
 
 /-- A finpartition of a graph's vertex set is `ε`-uniform (aka `ε`-regular) iff the proportion of
@@ -291,7 +291,7 @@ lemma IsEquipartition.card_interedges_sparsePairs_le' (hP : P.IsEquipartition)
   gcongr
   calc
     (_ : ℕ) ≤ _ := sum_le_card_nsmul P.parts.offDiag (fun i ↦ #i.1 * #i.2)
-            ((#A / #P.parts + 1)^2 : ℕ) ?_
+            ((#A / #P.parts + 1) ^ 2 : ℕ) ?_
     _ ≤ (#P.parts * (#A / #P.parts) + #P.parts) ^ 2 := ?_
     _ ≤ _ := by gcongr; apply Nat.mul_div_le
   · simp only [Prod.forall, and_imp, mem_offDiag, sq]
@@ -305,7 +305,7 @@ lemma IsEquipartition.card_interedges_sparsePairs_le (hP : P.IsEquipartition) (h
     #((P.sparsePairs G ε).biUnion fun (U, V) ↦ G.interedges U V) ≤ 4 * ε * #A ^ 2 := by
   calc
     _ ≤ _ := hP.card_interedges_sparsePairs_le' hε
-    _ ≤ ε * (#A + #A)^2 := by gcongr; exact P.card_parts_le_card
+    _ ≤ ε * (#A + #A) ^ 2 := by gcongr; exact P.card_parts_le_card
     _ = _ := by ring
 
 private lemma aux {i j : ℕ} (hj : 0 < j) : j * (j - 1) * (i / j + 1) ^ 2 < (i + j) ^ 2 := by
@@ -343,7 +343,7 @@ lemma IsEquipartition.card_biUnion_offDiag_le (hε : 0 < ε) (hP : P.IsEquiparti
   have : (#A : 𝕜) + #P.parts ≤ 2 * #A := by
     rw [two_mul]; gcongr; exact P.card_parts_le_card
   refine (mul_le_mul_of_nonneg_left this <| by positivity).trans ?_
-  suffices 1 ≤ ε/4 * #P.parts by
+  suffices 1 ≤ ε / 4 * #P.parts by
     rw [mul_left_comm, ← sq]
     convert mul_le_mul_of_nonneg_left this (mul_nonneg zero_le_two <| sq_nonneg (#A : 𝕜))
       using 1 <;> ring
@@ -417,9 +417,9 @@ lemma regularityReduced_anti {δ₁ δ₂ : 𝕜} (hδ : δ₁ ≤ δ₂) :
 
 omit [IsStrictOrderedRing 𝕜] in
 lemma unreduced_edges_subset :
-    (A ×ˢ A).filter (fun (x, y) ↦ G.Adj x y ∧ ¬ (G.regularityReduced P (ε/8) (ε/4)).Adj x y) ⊆
-      (P.nonUniforms G (ε/8)).biUnion (fun (U, V) ↦ U ×ˢ V) ∪ P.parts.biUnion offDiag ∪
-        (P.sparsePairs G (ε/4)).biUnion fun (U, V) ↦ G.interedges U V := by
+    (A ×ˢ A).filter (fun (x, y) ↦ G.Adj x y ∧ ¬ (G.regularityReduced P (ε / 8) (ε / 4)).Adj x y) ⊆
+      (P.nonUniforms G (ε / 8)).biUnion (fun (U, V) ↦ U ×ˢ V) ∪ P.parts.biUnion offDiag ∪
+        (P.sparsePairs G (ε / 4)).biUnion fun (U, V) ↦ G.interedges U V := by
   rintro ⟨x, y⟩
   simp only [mem_filter, regularityReduced_adj, not_and, not_exists,
     not_le, mem_biUnion, mem_union, mem_product, Prod.exists, mem_offDiag, and_imp,
@@ -430,7 +430,7 @@ lemma unreduced_edges_subset :
   obtain ⟨V, hV, hy⟩ := P.exists_mem hy
   obtain rfl | hUV := eq_or_ne U V
   · exact Or.inr (Or.inl ⟨U, hU, hx, hy, G.ne_of_adj h⟩)
-  by_cases h₂ : G.IsUniform (ε/8) U V
+  by_cases h₂ : G.IsUniform (ε / 8) U V
   · exact Or.inr <| Or.inr ⟨U, V, hU, hV, hUV, h' _ hU _ hV hx hy hUV h₂, hx, hy, h⟩
   · exact Or.inl ⟨U, V, hU, hV, hUV, h₂, hx, hy⟩
 

Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean

@@ -87,7 +87,7 @@ private lemma triangle_removal_aux (hε : 0 < ε) (hε₁ : ε ≤ 1) (hP₁ : P
   have dXY := P.disjoint hX hY nXY
   have dXZ := P.disjoint hX hZ nXZ
   have dYZ := P.disjoint hY hZ nYZ
-  have that : 2 * (ε/8) = ε/4 := by ring
+  have that : 2 * (ε / 8) = ε / 4 := by ring
   have : 0 ≤ 1 - 2 * (ε / 8) := by
     have : ε / 4 ≤ 1 := ‹ε / 4 ≤ _›.trans (by exact mod_cast G.edgeDensity_le_one _ _); linarith
   calc
@@ -103,11 +103,11 @@ private lemma triangle_removal_aux (hε : 0 < ε) (hε₁ : ε ≤ 1) (hP₁ : P
 
 lemma regularityReduced_edges_card_aux [Nonempty α] (hε : 0 < ε) (hP : P.IsEquipartition)
     (hPε : P.IsUniform G (ε / 8)) (hP' : 4 / ε ≤ #P.parts) :
-    2 * (#G.edgeFinset - #(G.regularityReduced P (ε/8) (ε/4)).edgeFinset : ℝ)
+    2 * (#G.edgeFinset - #(G.regularityReduced P (ε / 8) (ε / 4)).edgeFinset : ℝ)
       < 2 * ε * (card α ^ 2 : ℕ) := by
-  let A := (P.nonUniforms G (ε/8)).biUnion fun (U, V) ↦ U ×ˢ V
+  let A := (P.nonUniforms G (ε / 8)).biUnion fun (U, V) ↦ U ×ˢ V
   let B := P.parts.biUnion offDiag
-  let C := (P.sparsePairs G (ε/4)).biUnion fun (U, V) ↦ G.interedges U V
+  let C := (P.sparsePairs G (ε / 4)).biUnion fun (U, V) ↦ G.interedges U V
   calc
     _ = (#((univ ×ˢ univ).filter fun (x, y) ↦
           G.Adj x y ∧ ¬(G.regularityReduced P (ε / 8) (ε /4)).Adj x y) : ℝ) := by
@@ -137,15 +137,15 @@ lemma FarFromTriangleFree.le_card_cliqueFinset (hG : G.FarFromTriangleFree ε) :
   obtain hε | hε := le_or_gt ε 0
   · apply (mul_nonpos_of_nonpos_of_nonneg (triangleRemovalBound_nonpos hε) _).trans <;> positivity
   let l : ℕ := ⌈4 / ε⌉₊
-  have hl : 4/ε ≤ l := le_ceil (4/ε)
+  have hl : 4 / ε ≤ l := le_ceil (4 / ε)
   rcases le_total (card α) l with hl' | hl'
   · calc
       _ ≤ triangleRemovalBound ε * ↑l ^ 3 := by
         gcongr; exact (triangleRemovalBound_pos hε).le
       _ ≤ (1 : ℝ) := (triangleRemovalBound_mul_cube_lt hε).le
       _ ≤ _ := by simpa [one_le_iff_ne_zero] using (hG.cliqueFinset_nonempty hε).card_pos.ne'
   obtain ⟨P, hP₁, hP₂, hP₃, hP₄⟩ := szemeredi_regularity G (by positivity : 0 < ε / 8) hl'
-  have : 4/ε ≤ #P.parts := hl.trans (cast_le.2 hP₂)
+  have : 4 / ε ≤ #P.parts := hl.trans (cast_le.2 hP₂)
   have k := regularityReduced_edges_card_aux hε hP₁ hP₄ this
   rw [mul_assoc] at k
   replace k := lt_of_mul_lt_mul_left k zero_le_two
@@ -156,7 +156,7 @@ lemma FarFromTriangleFree.le_card_cliqueFinset (hG : G.FarFromTriangleFree ε) :
 then they can all be removed by removing a few edges (on the order of `(card α)^2`). -/
 lemma triangle_removal (hG : #(G.cliqueFinset 3) < triangleRemovalBound ε * card α ^ 3) :
     ∃ G' ≤ G, ∃ _ : DecidableRel G'.Adj,
-      (#G.edgeFinset - #G'.edgeFinset : ℝ) < ε * (card α^2 : ℕ) ∧ G'.CliqueFree 3 := by
+      (#G.edgeFinset - #G'.edgeFinset : ℝ) < ε * (card α ^ 2 : ℕ) ∧ G'.CliqueFree 3 := by
   by_contra! h
   refine hG.not_ge (farFromTriangleFree_iff.2 ?_).le_card_cliqueFinset
   intro G' _ hG hG'

Mathlib/Computability/TuringMachine.lean

@@ -217,7 +217,7 @@ theorem stmts₁_trans {q₁ q₂ : Stmt Γ Λ σ} : q₁ ∈ stmts₁ q₂ →
     · exact Finset.mem_insert_of_mem (Finset.mem_union_right _ (IH₂ h₁₂))
   | goto l => subst h₁₂; exact h₀₁
   | halt => subst h₁₂; exact h₀₁
-  | load  _ q IH | _ _ _ q IH =>
+  | load _ q IH | _ _ _ q IH =>
     rcases h₁₂ with (rfl | h₁₂)
     · unfold stmts₁ at h₀₁
       exact h₀₁

Mathlib/Control/ULiftable.lean

@@ -165,7 +165,8 @@ instance WriterT.instULiftableULiftULift {m m'} [ULiftable m m'] :
     ULiftable (WriterT (ULift.{max v₀ u₀} s) m) (WriterT (ULift.{max v₁ u₀} s) m') :=
   WriterT.uliftable' <| Equiv.ulift.trans Equiv.ulift.symm
 
-instance Except.instULiftable {ε : Type u₀} : ULiftable (Except.{u₀,v₁} ε) (Except.{u₀,v₂} ε) where
+instance Except.instULiftable {ε : Type u₀} :
+    ULiftable (Except.{u₀, v₁} ε) (Except.{u₀, v₂} ε) where
   congr e :=
     { toFun := Except.map e
       invFun := Except.map e.symm

Mathlib/Geometry/Manifold/PoincareConjecture.lean

@@ -22,7 +22,7 @@ space viewed as a model space.
 open scoped Manifold ContDiff
 open Metric (sphere)
 
-local macro:max "ℝ"n:superscript(term) : term => `(EuclideanSpace ℝ (Fin $(⟨n.raw[0]⟩)))
+local macro:max "ℝ" noWs n:superscript(term) : term => `(EuclideanSpace ℝ (Fin $(⟨n.raw[0]⟩)))
 local macro:max "𝕊"n:superscript(term) : term =>
   `(sphere (0 : EuclideanSpace ℝ (Fin ($(⟨n.raw[0]⟩) + 1))) 1)
 

Mathlib/Geometry/Manifold/VectorBundle/SmoothSection.lean

@@ -80,7 +80,7 @@ lemma ContMDiff.add_section
 
 lemma ContMDiffWithinAt.neg_section
     (hs : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) u x₀) :
-    ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (- s x)) u x₀ := by
+    ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (-s x)) u x₀ := by
   rw [contMDiffWithinAt_section] at hs ⊢
   set e := trivializationAt F V x₀
   refine hs.neg.congr_of_eventuallyEq ?_ ?_
@@ -93,7 +93,7 @@ lemma ContMDiffWithinAt.neg_section
 
 lemma ContMDiffAt.neg_section
     (hs : ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) x₀) :
-    ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (- s x)) x₀ := by
+    ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (-s x)) x₀ := by
   rw [← contMDiffWithinAt_univ] at hs ⊢
   exact hs.neg_section
 

Mathlib/GroupTheory/ArchimedeanDensely.lean

@@ -55,7 +55,7 @@ lemma Subgroup.mem_closure_singleton_iff_existsUnique_zpow {G : Type*}
   · exact fun h ↦ h.exists
 
 lemma Int.addEquiv_eq_refl_or_neg (e : ℤ ≃+ ℤ) : e = .refl _ ∨ e = .neg _ := by
-  suffices e 1 = 1 ∨ - e 1 = 1 by simpa [AddEquiv.ext_int_iff, neg_eq_iff_eq_neg]
+  suffices e 1 = 1 ∨ -e 1 = 1 by simpa [AddEquiv.ext_int_iff, neg_eq_iff_eq_neg]
   have he : ¬IsOfFinAddOrder (e 1) :=
     not_isOfFinAddOrder_of_isAddTorsionFree ((AddEquiv.map_ne_zero_iff e).mpr Int.one_ne_zero)
   rw [← AddSubgroup.zmultiples_eq_zmultiples_iff he]

Mathlib/GroupTheory/CoprodI.lean

@@ -501,7 +501,7 @@ theorem smul_eq_of_smul {i} (m : M i) (w : Word M) :
 theorem mem_smul_iff {i j : ι} {m₁ : M i} {m₂ : M j} {w : Word M} :
     ⟨_, m₁⟩ ∈ (of m₂ • w).toList ↔
       (¬i = j ∧ ⟨i, m₁⟩ ∈ w.toList)
-      ∨ (m₁ ≠ 1 ∧ ∃ (hij : i = j),(⟨i, m₁⟩ ∈ w.toList.tail) ∨
+      ∨ (m₁ ≠ 1 ∧ ∃ (hij : i = j), (⟨i, m₁⟩ ∈ w.toList.tail) ∨
         (∃ m', ⟨j, m'⟩ ∈ w.toList.head? ∧ m₁ = hij ▸ (m₂ * m')) ∨
         (w.fstIdx ≠ some j ∧ m₁ = hij ▸ m₂)) := by
   rw [of_smul_def, mem_rcons_iff, mem_equivPair_tail_iff, equivPair_head, or_assoc]

Mathlib/GroupTheory/Coxeter/Basic.lean

@@ -312,7 +312,7 @@ private theorem toMonoidHom_apply_symm_apply (a : PresentedGroup (M.relationsSet
     (MulEquiv.toMonoidHom cs.mulEquiv : W →* PresentedGroup (M.relationsSet))
     ((MulEquiv.symm cs.mulEquiv) a) = a := calc
   _ = cs.mulEquiv ((MulEquiv.symm cs.mulEquiv) a) := by rfl
-  _ = _                                           := by rw [MulEquiv.apply_symm_apply]
+  _ = _ := by rw [MulEquiv.apply_symm_apply]
 
 /-- The universal mapping property of Coxeter systems. For any monoid `G`,
 functions `f : B → G` whose values satisfy the Coxeter relations are equivalent to
@@ -357,7 +357,7 @@ theorem simple_determines_coxeterSystem :
 /-- The product of the simple reflections of `W` corresponding to the indices in `ω`. -/
 def wordProd (ω : List B) : W := prod (map cs.simple ω)
 
-local prefix:100 "π" => cs.wordProd
+local prefix:100 "π " => cs.wordProd
 
 @[simp] theorem wordProd_nil : π [] = 1 := by simp [wordProd]
 
@@ -386,8 +386,8 @@ theorem wordProd_surjective : Surjective cs.wordProd := by
 /-- The word of length `m` that alternates between `i` and `i'`, ending with `i'`. -/
 def alternatingWord (i i' : B) (m : ℕ) : List B :=
   match m with
-  | 0    => []
-  | m+1  => (alternatingWord i' i m).concat i'
+  | 0 => []
+  | m + 1 => (alternatingWord i' i m).concat i'
 
 /-- The word of length `M i i'` that alternates between `i` and `i'`, ending with `i'`. -/
 abbrev braidWord (M : CoxeterMatrix B) (i i' : B) : List B := alternatingWord i i' (M i i')
@@ -420,9 +420,10 @@ lemma getElem_alternatingWord (i j : B) (p k : ℕ) (hk : k < p) :
   | succ n h => grind [CoxeterSystem.alternatingWord_succ']
 
 lemma getElem_alternatingWord_swapIndices (i j : B) (p k : ℕ) (h : k + 1 < p) :
-     (alternatingWord i j p)[k+1]'(by simp [h]) =
+     (alternatingWord i j p)[k + 1]'(by simp [h]) =
      (alternatingWord j i p)[k]'(by simp; cutsat) := by
-  rw [getElem_alternatingWord i j p (k+1) (by cutsat), getElem_alternatingWord j i p k (by cutsat)]
+  rw [getElem_alternatingWord i j p (k + 1) (by cutsat),
+    getElem_alternatingWord j i p k (by cutsat)]
   by_cases h_even : Even (p + k)
   · rw [if_pos h_even, ← add_assoc]
     simp only [ite_eq_right_iff, isEmpty_Prop, Nat.not_even_iff_odd, Even.add_one h_even,
@@ -456,7 +457,7 @@ lemma listTake_alternatingWord (i j : B) (p k : ℕ) (h : k < 2 * p) :
 lemma listTake_succ_alternatingWord (i j : B) (p : ℕ) (k : ℕ) (h : k + 1 < 2 * p) :
     List.take (k + 1) (alternatingWord i j (2 * p)) =
     i :: (List.take k (alternatingWord j i (2 * p))) := by
-  rw [listTake_alternatingWord j i p k (by cutsat), listTake_alternatingWord i j p (k+1) h]
+  rw [listTake_alternatingWord j i p k (by cutsat), listTake_alternatingWord i j p (k + 1) h]
   by_cases h_even : Even k
   · simp [Nat.not_even_iff_odd.mpr (Even.add_one h_even), alternatingWord_succ', h_even]
   · simp [(by rw [Nat.not_even_iff_odd] at h_even; exact Odd.add_one h_even : Even (k + 1)),

Mathlib/GroupTheory/Coxeter/Inversion.lean

@@ -53,9 +53,9 @@ variable {B : Type*}
 variable {W : Type*} [Group W]
 variable {M : CoxeterMatrix B} (cs : CoxeterSystem M W)
 
-local prefix:100 "s" => cs.simple
-local prefix:100 "π" => cs.wordProd
-local prefix:100 "ℓ" => cs.length
+local prefix:100 "s " => cs.simple
+local prefix:100 "π " => cs.wordProd
+local prefix:100 "ℓ " => cs.length
 
 /-- `t : W` is a *reflection* of the Coxeter system `cs` if it is of the form
 $w s_i w^{-1}$, where $w \in W$ and $s_i$ is a simple reflection. -/
@@ -184,8 +184,8 @@ $$s_{i_\ell}\cdots s_{i_1}\cdots s_{i_\ell}, \ldots,
 -/
 def rightInvSeq (ω : List B) : List W :=
   match ω with
-  | []          => []
-  | i :: ω      => (π ω)⁻¹ * (s i) * (π ω) :: rightInvSeq ω
+  | [] => []
+  | i :: ω => (π ω)⁻¹ * (s i) * (π ω) :: rightInvSeq ω
 
 /-- The left inversion sequence of `ω`. The left inversion sequence of a word
 $s_{i_1} \cdots s_{i_\ell}$ is the sequence
@@ -194,11 +194,11 @@ $$s_{i_1}, s_{i_1}s_{i_2}s_{i_1}, s_{i_1}s_{i_2}s_{i_3}s_{i_2}s_{i_1}, \ldots,
 -/
 def leftInvSeq (ω : List B) : List W :=
   match ω with
-  | []          => []
-  | i :: ω      => s i :: List.map (MulAut.conj (s i)) (leftInvSeq ω)
+  | [] => []
+  | i :: ω => s i :: List.map (MulAut.conj (s i)) (leftInvSeq ω)
 
-local prefix:100 "ris" => cs.rightInvSeq
-local prefix:100 "lis" => cs.leftInvSeq
+local prefix:100 "ris " => cs.rightInvSeq
+local prefix:100 "lis " => cs.leftInvSeq
 
 @[simp] theorem rightInvSeq_nil : ris [] = [] := rfl
 
@@ -262,7 +262,7 @@ theorem getD_rightInvSeq (ω : List B) (j : ℕ) :
       simp [ih j']
 
 lemma getElem_rightInvSeq (ω : List B) (j : ℕ) (h : j < ω.length) :
-    (ris ω)[j]'(by simp [h]) =
+    (ris ω)[j]'(by simp  [h]) =
     (π (ω.drop (j + 1)))⁻¹
       * (Option.map (cs.simple) ω[j]?).getD 1
       * π (ω.drop (j + 1)) := by
@@ -373,9 +373,9 @@ theorem isRightInversion_of_mem_rightInvSeq {ω : List B} (hω : cs.IsReduced ω
     rw [cs.length_rightInvSeq] at hj
     calc
       ℓ (π (ω.eraseIdx j))
-      _ ≤ (ω.eraseIdx j).length   := cs.length_wordProd_le _
-      _ < ω.length                := by rw [← List.length_eraseIdx_add_one hj]; exact lt_add_one _
-      _ = ℓ (π ω)                 := hω.symm
+      _ ≤ (ω.eraseIdx j).length := (cs.length_wordProd_le _)
+      _ < ω.length := by rw [← List.length_eraseIdx_add_one hj]; exact lt_add_one _
+      _ = ℓ (π ω) := hω.symm
 
 theorem isLeftInversion_of_mem_leftInvSeq {ω : List B} (hω : cs.IsReduced ω) {t : W}
     (ht : t ∈ lis ω) : cs.IsLeftInversion (π ω) t := by
@@ -386,9 +386,9 @@ theorem isLeftInversion_of_mem_leftInvSeq {ω : List B} (hω : cs.IsReduced ω)
     rw [cs.length_leftInvSeq] at hj
     calc
       ℓ (π (ω.eraseIdx j))
-      _ ≤ (ω.eraseIdx j).length   := cs.length_wordProd_le _
-      _ < ω.length                := by rw [← List.length_eraseIdx_add_one hj]; exact lt_add_one _
-      _ = ℓ (π ω)                 := hω.symm
+      _ ≤ (ω.eraseIdx j).length := (cs.length_wordProd_le _)
+      _ < ω.length := by rw [← List.length_eraseIdx_add_one hj]; exact lt_add_one _
+      _ = ℓ (π ω) := hω.symm
 
 theorem prod_rightInvSeq (ω : List B) : prod (ris ω) = (π ω)⁻¹ := by
   induction ω with
@@ -399,11 +399,11 @@ theorem prod_leftInvSeq (ω : List B) : prod (lis ω) = (π ω)⁻¹ := by
   simp only [leftInvSeq_eq_reverse_rightInvSeq_reverse, prod_reverse_noncomm, inv_inj]
   have : List.map (fun x ↦ x⁻¹) (ris ω.reverse) = ris ω.reverse := calc
     List.map (fun x ↦ x⁻¹) (ris ω.reverse)
-    _ = List.map id (ris ω.reverse)             := by
+    _ = List.map id (ris ω.reverse) := by
         apply List.map_congr_left
         intro t ht
         exact (cs.isReflection_of_mem_rightInvSeq _ ht).inv
-    _ = ris ω.reverse                           := map_id _
+    _ = ris ω.reverse := map_id _
   rw [this]
   nth_rw 2 [← reverse_reverse ω]
   rw [wordProd_reverse]
@@ -419,7 +419,7 @@ theorem IsReduced.nodup_rightInvSeq {ω : List B} (rω : cs.IsReduced ω) : List
   rw [← getD_eq_getElem _ 1, ← getD_eq_getElem _ 1] at dup
   set! t := (ris ω).getD j 1 with h₁
   set! t' := (ris (ω.eraseIdx j)).getD (j' - 1) 1 with h₂
-  have h₃ : t' = (ris ω).getD j' 1                    := by
+  have h₃ : t' = (ris ω).getD j' 1 := by
     rw [h₂, cs.getD_rightInvSeq, cs.getD_rightInvSeq,
       (Nat.sub_add_cancel (by cutsat) : j' - 1 + 1 = j'), eraseIdx_eq_take_drop_succ,
       drop_append, drop_of_length_le (by simp [j_lt_j'.le]), length_take, drop_drop,
@@ -429,19 +429,19 @@ theorem IsReduced.nodup_rightInvSeq {ω : List B} (rω : cs.IsReduced ω) : List
     show (List.take j ω ++ List.drop (j + 1) ω)[j' - 1]? = ω[j']?
     rw [getElem?_append_right (by simp [Nat.le_sub_one_of_lt j_lt_j']), getElem?_drop]
     grind
-  have h₄ : t * t' = 1                                := by
+  have h₄ : t * t' = 1 := by
     rw [h₁, h₃, dup]
     exact cs.getD_rightInvSeq_mul_self _ _
   have h₅ := calc
-    π ω   = π ω * t * t'                              := by rw [mul_assoc, h₄]; group
-    _     = (π (ω.eraseIdx j)) * t'                   :=
-        congrArg (· * t') (cs.wordProd_mul_getD_rightInvSeq _ _)
-    _     = π ((ω.eraseIdx j).eraseIdx (j' - 1))      :=
-        cs.wordProd_mul_getD_rightInvSeq _ _
+    π ω = π ω * t * t' := by rw [mul_assoc, h₄]; group
+    _ = (π (ω.eraseIdx j)) * t' :=
+        (congrArg (· * t') (cs.wordProd_mul_getD_rightInvSeq _ _))
+    _ = π ((ω.eraseIdx j).eraseIdx (j' - 1)) :=
+        (cs.wordProd_mul_getD_rightInvSeq _ _)
   have h₆ := calc
-    ω.length = ℓ (π ω)                                    := rω.symm
-    _        = ℓ (π ((ω.eraseIdx j).eraseIdx (j' - 1)))   := congrArg cs.length h₅
-    _        ≤ ((ω.eraseIdx j).eraseIdx (j' - 1)).length  := cs.length_wordProd_le _
+    ω.length = ℓ (π ω) := (rω.symm)
+    _ = ℓ (π ((ω.eraseIdx j).eraseIdx (j' - 1))) := (congrArg cs.length h₅)
+    _ ≤ ((ω.eraseIdx j).eraseIdx (j' - 1)).length := (cs.length_wordProd_le _)
   grind
 
 theorem IsReduced.nodup_leftInvSeq {ω : List B} (rω : cs.IsReduced ω) : List.Nodup (lis ω) := by