chore(Data): fix whitespace (#32931)

harahu · harahu · commit 72eadd6131ba · 2025-12-16T09:51:40.000Z
diff --git a/Mathlib/Data/Complex/Basic.lean b/Mathlib/Data/Complex/Basic.lean
@@ -218,8 +218,8 @@ theorem re_ofReal_mul (r : ℝ) (z : ℂ) : (r * z).re = r * z.re := by simp [of
 
 theorem im_ofReal_mul (r : ℝ) (z : ℂ) : (r * z).im = r * z.im := by simp [ofReal]
 
-lemma re_mul_ofReal (z : ℂ) (r : ℝ) : (z * r).re = z.re *  r := by simp [ofReal]
-lemma im_mul_ofReal (z : ℂ) (r : ℝ) : (z * r).im = z.im *  r := by simp [ofReal]
+lemma re_mul_ofReal (z : ℂ) (r : ℝ) : (z * r).re = z.re * r := by simp [ofReal]
+lemma im_mul_ofReal (z : ℂ) (r : ℝ) : (z * r).im = z.im * r := by simp [ofReal]
 
 theorem ofReal_mul' (r : ℝ) (z : ℂ) : ↑r * z = ⟨r * z.re, r * z.im⟩ :=
   ext (re_ofReal_mul _ _) (im_ofReal_mul _ _)
diff --git a/Mathlib/Data/ENNReal/Inv.lean b/Mathlib/Data/ENNReal/Inv.lean
@@ -832,7 +832,7 @@ lemma mul_iInf' (hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0) (h₀ :
   obtain rfl | ha := eq_or_ne a ∞
   · obtain ⟨i, hi⟩ | hf := em (∃ i, f i = 0)
     · rw [(iInf_eq_bot _).2, (iInf_eq_bot _).2, bot_eq_zero, mul_zero] <;>
-        exact fun _ _↦ ⟨i, by simpa [hi]⟩
+        exact fun _ _ ↦ ⟨i, by simpa [hi]⟩
     · rw [top_mul (mt (hinfty rfl) hf), eq_comm, iInf_eq_top]
       exact fun i ↦ top_mul fun hi ↦ hf ⟨i, hi⟩
   · exact (mulLeftOrderIso _ <| isUnit_iff.2 ⟨ha₀, ha⟩).map_iInf _
diff --git a/Mathlib/Data/EReal/Basic.lean b/Mathlib/Data/EReal/Basic.lean
@@ -190,7 +190,7 @@ theorem induction₂_symm {P : EReal → EReal → Prop} (symm : ∀ {x y}, P x
     (fun _ h => symm <| pos_bot _ h) (symm zero_bot) (fun _ h => symm <| neg_bot _ h) bot_bot
 
 protected theorem mul_comm (x y : EReal) : x * y = y * x := by
-  induction x <;> induction y  <;>
+  induction x <;> induction y <;>
     try { rfl }
   rw [← coe_mul, ← coe_mul, mul_comm]
 
diff --git a/Mathlib/Data/Fin/Fin2.lean b/Mathlib/Data/Fin/Fin2.lean
@@ -125,7 +125,7 @@ def castSucc {n} : Fin2 n → Fin2 (n + 1)
 
 /-- The greatest value of `Fin2 (n+1)`. -/
 def last : {n : Nat} → Fin2 (n + 1)
-  | 0   => fz
+  | 0 => fz
   | n + 1 => fs (@last n)
 
 /-- Maps `0` to `n-1`, `1` to `n-2`, ..., `n-1` to `0`. -/
@@ -150,7 +150,7 @@ instance : Inhabited (Fin2 1) :=
   ⟨fz⟩
 
 instance instFintype : ∀ n, Fintype (Fin2 n)
-  | 0   => ⟨∅, Fin2.elim0⟩
+  | 0 => ⟨∅, Fin2.elim0⟩
   | n + 1 =>
     let ⟨elems, compl⟩ := instFintype n
     { elems    := elems.map ⟨Fin2.fs, @fs.inj _⟩ |>.cons .fz (by simp)
diff --git a/Mathlib/Data/Finset/Defs.lean b/Mathlib/Data/Finset/Defs.lean
@@ -209,7 +209,7 @@ instance : IsRefl (Finset α) (· ⊆ ·) :=
   inferInstanceAs <| IsRefl (Finset α) (· ≤ ·)
 
 instance : IsTrans (Finset α) (· ⊆ ·) :=
-  inferInstanceAs <|  IsTrans (Finset α) (· ≤ ·)
+  inferInstanceAs <| IsTrans (Finset α) (· ≤ ·)
 
 instance : IsAntisymm (Finset α) (· ⊆ ·) :=
   inferInstanceAs <| IsAntisymm (Finset α) (· ≤ ·)
diff --git a/Mathlib/Data/Finset/Sort.lean b/Mathlib/Data/Finset/Sort.lean
@@ -41,7 +41,7 @@ variable (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α
 variable (r' : β → β → Prop) [DecidableRel r'] [IsTrans β r'] [IsAntisymm β r'] [IsTotal β r']
 
 @[simp]
-theorem sort_val : Multiset.sort s.val r  = sort s r :=
+theorem sort_val : Multiset.sort s.val r = sort s r :=
   rfl
 
 @[simp]
diff --git a/Mathlib/Data/Finsupp/Interval.lean b/Mathlib/Data/Finsupp/Interval.lean
@@ -92,7 +92,7 @@ instance instLocallyFiniteOrder : LocallyFiniteOrder (ι →₀ α) :=
 
 theorem Icc_eq : Icc f g = (f.support ∪ g.support).finsupp (f.rangeIcc g) := rfl
 
-theorem card_Icc : #(Icc f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)):= by
+theorem card_Icc : #(Icc f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) := by
   simp_rw [Icc_eq, card_finsupp, coe_rangeIcc]
 
 theorem card_Ico : #(Ico f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 1 := by
diff --git a/Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean b/Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean
@@ -238,7 +238,7 @@ example : single (1 : Fin 2) 1 ≺[degLex] single 0 1 := by
   exact Nat.one_pos
 
 /-- for the deg-lexicographic ordering, X 0 * X 1 < X 0  ^ 2 -/
-example : (single 0 1 + single 1 1) ≺[degLex] single (0 : Fin 2) 2  := by
+example : (single 0 1 + single 1 1) ≺[degLex] single (0 : Fin 2) 2 := by
   rw [degLex_lt_iff, lt_iff, ofDegLex_toDegLex]
   simp only [Fin.isValue, map_add, degree_single, Nat.reduceAdd, ofDegLex_toDegLex,
     lt_self_iff_false, toLex_add, true_and, false_or]
diff --git a/Mathlib/Data/Fintype/List.lean b/Mathlib/Data/Fintype/List.lean
@@ -75,7 +75,7 @@ instance fintypeNodupList [Fintype α] : Fintype { l : List α // l.Nodup } := b
       simp only [_root_.Disjoint]
       rw [← m.coe_toList, ← n.coe_toList, Multiset.lists_coe, Multiset.lists_coe]
       have := Multiset.coe_disjoint m.toList.permutations n.toList.permutations
-      rw  [_root_.Disjoint] at this
+      rw [_root_.Disjoint] at this
       rw [this]
       simp only [ne_eq]
       rw [List.disjoint_iff_ne]
diff --git a/Mathlib/Data/Fintype/Option.lean b/Mathlib/Data/Fintype/Option.lean
@@ -92,7 +92,7 @@ theorem induction_empty_option {P : ∀ (α : Type u) [Fintype α], Prop}
   obtain ⟨p⟩ :=
     let f_empty := fun i => by convert h_empty
     let h_option : ∀ {α : Type u} [Fintype α] [DecidableEq α],
-          (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α)  := by
+          (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α) := by
       rintro α hα - Pα hα'
       convert h_option α (Pα _)
     @truncRecEmptyOption (fun α => ∀ h, @P α h) (@fun α β e hα hβ => @of_equiv α β hβ e (hα _))
diff --git a/Mathlib/Data/Fintype/Quotient.lean b/Mathlib/Data/Fintype/Quotient.lean
@@ -42,15 +42,15 @@ variable {ι : Type*} [DecidableEq ι] {α : ι → Sort*} {S : ∀ i, Setoid (
   term in the quotient of the product of the setoids indexed by `l`. -/
 def listChoice {l : List ι} (q : ∀ i ∈ l, Quotient (S i)) : @Quotient (∀ i ∈ l, α i) piSetoid :=
   match l with
-  |     [] => ⟦nofun⟧
+  | [] => ⟦nofun⟧
   | i :: _ => Quotient.liftOn₂ (List.Pi.head (i := i) q)
     (listChoice (List.Pi.tail q))
     (⟦List.Pi.cons _ _ · ·⟧)
     (fun _ _ _ _ ha hl ↦ Quotient.sound (List.Pi.forall_rel_cons_ext ha hl))
 
 theorem listChoice_mk {l : List ι} (a : ∀ i ∈ l, α i) : listChoice (S := S) (⟦a · ·⟧) = ⟦a⟧ :=
   match l with
-  |     [] => Quotient.sound nofun
+  | [] => Quotient.sound nofun
   | i :: l => by
     unfold listChoice List.Pi.tail
     rw [listChoice_mk]
@@ -61,7 +61,7 @@ theorem listChoice_mk {l : List ι} (a : ∀ i ∈ l, α i) : listChoice (S := S
 lemma list_ind {l : List ι} {C : (∀ i ∈ l, Quotient (S i)) → Prop}
     (f : ∀ a : ∀ i ∈ l, α i, C (⟦a · ·⟧)) (q : ∀ i ∈ l, Quotient (S i)) : C q :=
   match l with
-  |     [] => cast (congr_arg _ (funext₂ nofun)) (f nofun)
+  | [] => cast (congr_arg _ (funext₂ nofun)) (f nofun)
   | i :: l => by
     rw [← List.Pi.cons_eta q]
     induction List.Pi.head q using Quotient.ind with | _ a
diff --git a/Mathlib/Data/List/Lemmas.lean b/Mathlib/Data/List/Lemmas.lean
@@ -87,8 +87,7 @@ section MapAccumr
 theorem mapAccumr_eq_foldr {σ : Type*} (f : α → σ → σ × β) : ∀ (as : List α) (s : σ),
     mapAccumr f as s = List.foldr (fun a s =>
                                     let r := f a s.1
-                                    (r.1, r.2 :: s.2)
-                                  ) (s, []) as
+                                    (r.1, r.2 :: s.2)) (s, []) as
   | [], _ => rfl
   | a :: as, s => by
     simp only [mapAccumr, foldr, mapAccumr_eq_foldr f as]
@@ -97,8 +96,7 @@ theorem mapAccumr₂_eq_foldr {σ φ : Type*} (f : α → β → σ → σ × φ
     ∀ (as : List α) (bs : List β) (s : σ),
     mapAccumr₂ f as bs s = foldr (fun ab s =>
                               let r := f ab.1 ab.2 s.1
-                              (r.1, r.2 :: s.2)
-                            ) (s, []) (as.zip bs)
+                              (r.1, r.2 :: s.2)) (s, []) (as.zip bs)
   | [], [], _ => rfl
   | _ :: _, [], _ => rfl
   | [], _ :: _, _ => rfl
diff --git a/Mathlib/Data/List/Pairwise.lean b/Mathlib/Data/List/Pairwise.lean
@@ -113,7 +113,7 @@ alias Sorted.head!_le := Pairwise.head!_le
 alias Sorted.le_head! := Pairwise.head!_le
 
 theorem pairwise_replicate_of_refl {n} [IsRefl α R] : (replicate n a).Pairwise R :=
-  pairwise_replicate.mpr  (Or.inr <| refl_of ..)
+  pairwise_replicate.mpr (Or.inr <| refl_of ..)
 
 @[deprecated (since := "2025-10-11")]
 alias sorted_replicate := pairwise_replicate_of_refl
diff --git a/Mathlib/Data/List/PeriodicityLemma.lean b/Mathlib/Data/List/PeriodicityLemma.lean
@@ -97,7 +97,7 @@ lemma hasPeriod_iff_forall_getElem?_mod {p : ℕ} {w : List α} :
     HasPeriod w p ↔ (∀ i < w.length, w[i]? = w[i % p]?) := by
   constructor
   · intro per i len
-    exact  Eq.symm (per.getElem?_mod p i w len)
+    exact Eq.symm (per.getElem?_mod p i w len)
   · intro mod
     rw [hasPeriod_iff_getElem?]
     intro i less
@@ -163,7 +163,7 @@ lemma HasPeriod.take_append (p n : ℕ) (w : List α) (dvd : p ∣ n)
       have j_mod : (j - n) % p = j % p := by
         calc
           (j - n) % p = (j - p * (n / p)) % p := by rw [Nat.mul_div_cancel' dvd]
-          _           = j % p := sub_mul_mod ((Nat.mul_div_cancel' dvd).symm ▸ n_le_j)
+          _ = j % p := sub_mul_mod ((Nat.mul_div_cancel' dvd).symm ▸ n_le_j)
       calc
         (take n w ++ w)[j]? = w[j - (take n w).length]? := getElem?_append_right (by simp_all)
         _ = w[j - n]? := by simp_all
@@ -182,9 +182,9 @@ lemma HasPeriod.drop_of_hasPeriod_add {q k : ℕ} {w : List α}
   intro i i_lt
   calc
      w[q + i]? = w[i + q]? := congrArg (getElem? w) (add_comm q i)
-     _         = w[i]? := (per_q i (by lia)).symm
-     _         = w[i + (k + q)]? := per_plus i (by lia)
-     _         = w[q + (i + k)]? := congr_arg (getElem? w) (by lia)
+     _ = w[i]? := (per_q i (by lia)).symm
+     _ = w[i + (k + q)]? := per_plus i (by lia)
+     _ = w[q + (i + k)]? := congr_arg (getElem? w) (by lia)
 
 /-- The **Periodicity Lemma**, also known as the **Fine and Wilf theorem**, shows that
 if word `w` of length at least `p + q - gcd p q` has two periods `p` and `q`,
diff --git a/Mathlib/Data/List/Pi.lean b/Mathlib/Data/List/Pi.lean
@@ -75,7 +75,7 @@ variable {ι : Type*} [DecidableEq ι] {α : ι → Type*}
 
 /-- `pi xs f` creates the list of functions `g` such that, for `x ∈ xs`, `g x ∈ f x` -/
 def pi : ∀ l : List ι, (∀ i, List (α i)) → List (∀ i, i ∈ l → α i)
-  |     [],  _ => [List.Pi.nil α]
+  | [], _ => [List.Pi.nil α]
   | i :: l, fs => (fs i).flatMap (fun b ↦ (pi l fs).map (List.Pi.cons _ _ b))
 
 @[simp] lemma pi_nil (t : ∀ i, List (α i)) :
diff --git a/Mathlib/Data/Matrix/Mul.lean b/Mathlib/Data/Matrix/Mul.lean
@@ -611,7 +611,7 @@ theorem add_vecMulVec [Mul α] [Add α] [RightDistribClass α] (w₁ w₂ : m 
   ext fun _ _ => add_mul _ _ _
 
 theorem vecMulVec_add [Mul α] [Add α] [LeftDistribClass α] (w : m → α) (v₁ v₂ : n → α) :
-    vecMulVec w (v₁ + v₂) = vecMulVec w v₁ + vecMulVec w v₂  :=
+    vecMulVec w (v₁ + v₂) = vecMulVec w v₁ + vecMulVec w v₂ :=
   ext fun _ _ => mul_add _ _ _
 
 @[simp]
diff --git a/Mathlib/Data/Nat/Choose/Factorization.lean b/Mathlib/Data/Nat/Choose/Factorization.lean
@@ -113,7 +113,7 @@ added in base `p`. The set is expressed by filtering `Ico 1 b` where `b` is any
 than `log p (n + k)`. -/
 theorem factorization_choose' {p n k b : ℕ} (hp : p.Prime) (hnb : log p (n + k) < b) :
     (choose (n + k) k).factorization p = #{i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i} := by
-  have h₁ : (choose (n + k) k).factorization p +  (k ! * n !).factorization p
+  have h₁ : (choose (n + k) k).factorization p + (k ! * n !).factorization p
     = #{i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i} + (k ! * n !).factorization p := by
     have h2 := (add_tsub_cancel_right n k) ▸ choose_mul_factorial_mul_factorial (le_add_left k n)
     rw [← Pi.add_apply, ← coe_add, ← factorization_mul (ne_of_gt <| choose_pos (le_add_left k n))
@@ -130,7 +130,7 @@ are added in base `p`. The set is expressed by filtering `Ico 1 b` where `b`
 is any bound greater than `log p n`. -/
 theorem factorization_choose {p n k b : ℕ} (hp : p.Prime) (hkn : k ≤ n) (hnb : log p n < b) :
     (choose n k).factorization p = #{i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i} := by
-  rw [←factorization_choose' hp ((Nat.sub_add_cancel hkn).symm ▸ hnb), Nat.sub_add_cancel hkn]
+  rw [← factorization_choose' hp ((Nat.sub_add_cancel hkn).symm ▸ hnb), Nat.sub_add_cancel hkn]
 
 /-- Modified version of `emultiplicity_le_emultiplicity_of_dvd_right`
 but for factorization. -/
diff --git a/Mathlib/Data/Nat/Digits/Defs.lean b/Mathlib/Data/Nat/Digits/Defs.lean
@@ -521,7 +521,7 @@ lemma toDigitsCore_lens_eq (b f : Nat) : ∀ (n : Nat) (c : Char) (tl : List Cha
   | succ f ih =>
     grind
 
-lemma nat_repr_len_aux (n b e : Nat) (h_b_pos : 0 < b) :  n < b ^ e.succ → n / b < b ^ e := by
+lemma nat_repr_len_aux (n b e : Nat) (h_b_pos : 0 < b) : n < b ^ e.succ → n / b < b ^ e := by
   simp only [Nat.pow_succ]
   exact (@Nat.div_lt_iff_lt_mul b n (b ^ e) h_b_pos).mpr
 
diff --git a/Mathlib/Data/Nat/Digits/Lemmas.lean b/Mathlib/Data/Nat/Digits/Lemmas.lean
@@ -30,7 +30,7 @@ theorem ofDigits_eq_sum_mapIdx_aux (b : ℕ) (l : List ℕ) :
       b * (l.zipWith (fun a i => a * b ^ i) (List.range l.length)).sum := by
   suffices
     l.zipWith (fun a i : ℕ => a * b ^ (i + 1)) (List.range l.length) =
-      l.zipWith (fun a i=> b * (a * b ^ i)) (List.range l.length)
+      l.zipWith (fun a i => b * (a * b ^ i)) (List.range l.length)
     by simp [this]
   congr; ext; ring
 
@@ -63,7 +63,7 @@ theorem digits_len (b n : ℕ) (hb : 1 < b) (hn : n ≠ 0) : (b.digits n).length
     exact div_eq_of_lt h
 
 theorem digits_length_le_iff {b k : ℕ} (hb : 1 < b) (n : ℕ) :
-    (b.digits n).length ≤ k ↔ n < b ^ k  := by
+    (b.digits n).length ≤ k ↔ n < b ^ k := by
   by_cases h : n = 0
   · have : 0 < b ^ k := by positivity
     simpa [h]
@@ -182,7 +182,7 @@ theorem sub_one_mul_sum_div_pow_eq_sub_sum_digits {p : ℕ}
         rw [← Ico_succ_singleton, List.drop_length, ofDigits] at this
         have h₁ : 1 ≤ tl.length := List.length_pos_iff.mpr h'
         rw [← sum_range_add_sum_Ico _ <| h₁, ← add_zero (∑ x ∈ Ico _ _, ofDigits p (tl.drop x)),
-            ← this, sum_Ico_consecutive _  h₁ <| (le_add_right tl.length 1),
+            ← this, sum_Ico_consecutive _ h₁ <| (le_add_right tl.length 1),
             ← sum_Ico_add _ 0 tl.length 1,
             Ico_zero_eq_range, mul_add, mul_add, ih, range_one, sum_singleton, List.drop, ofDigits,
             mul_zero, add_zero, ← Nat.add_sub_assoc <| sum_le_ofDigits _ <| Nat.le_of_lt h]
diff --git a/Mathlib/Data/Nat/MaxPowDiv.lean b/Mathlib/Data/Nat/MaxPowDiv.lean
@@ -105,7 +105,7 @@ theorem le_of_dvd {p n pow : ℕ} (hp : 1 < p) (hn : n ≠ 0) (h : p ^ pow ∣ n
   have : 0 < c := by
     apply Nat.pos_of_ne_zero
     intro h'
-    rw [h',mul_zero] at hc
+    rw [h', mul_zero] at hc
     lia
   simp [hc, base_pow_mul hp this]
 
diff --git a/Mathlib/Data/Nat/ModEq.lean b/Mathlib/Data/Nat/ModEq.lean
@@ -349,7 +349,7 @@ lemma eq_of_lt_of_lt (h : a ≡ b [MOD m]) (ha : a < m) (hb : b < m) : a = b :=
   h.eq_of_abs_lt <| Int.abs_sub_lt_of_lt_lt ha hb
 
 /-- To cancel a common factor `c` from a `ModEq` we must divide the modulus `m` by `gcd m c` -/
-lemma cancel_left_div_gcd (hm : 0 < m) (h : c * a ≡ c * b [MOD m]) :  a ≡ b [MOD m / gcd m c] := by
+lemma cancel_left_div_gcd (hm : 0 < m) (h : c * a ≡ c * b [MOD m]) : a ≡ b [MOD m / gcd m c] := by
   let d := gcd m c
   have hmd := gcd_dvd_left m c
   have hcd := gcd_dvd_right m c
diff --git a/Mathlib/Data/Nat/Prime/Defs.lean b/Mathlib/Data/Nat/Prime/Defs.lean
@@ -390,8 +390,7 @@ theorem factors_lemma {k} : (k + 2) / minFac (k + 2) < k + 2 :=
   div_lt_self (Nat.zero_lt_succ _) (minFac_prime (by
       apply Nat.ne_of_gt
       apply Nat.succ_lt_succ
-      apply Nat.zero_lt_succ
-      )).one_lt
+      apply Nat.zero_lt_succ)).one_lt
 
 end MinFac
 
diff --git a/Mathlib/Data/PFunctor/Multivariate/M.lean b/Mathlib/Data/PFunctor/Multivariate/M.lean
@@ -203,7 +203,7 @@ theorem M.dest_corec {α : TypeVec n} {β : Type u} (g : β → P (α.append1 β
 theorem M.bisim_lemma {α : TypeVec n} {a₁ : (mp P).A} {f₁ : (mp P).B a₁ ⟹ α} {a' : P.A}
     {f' : (P.B a').drop ⟹ α} {f₁' : (P.B a').last → M P α}
     (e₁ : M.dest P ⟨a₁, f₁⟩ = ⟨a', splitFun f' f₁'⟩) :
-    ∃ (g₁' : _)(e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
+    ∃ (g₁' : _) (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
       f' = M.pathDestLeft P e₁' f₁ ∧
         f₁' = fun x : (last P).B a' => ⟨g₁' x, M.pathDestRight P e₁' f₁ x⟩ := by
   generalize ef : @splitFun n _ (append1 α (M P α)) f' f₁' = ff at e₁
diff --git a/Mathlib/Data/PFunctor/Univariate/M.lean b/Mathlib/Data/PFunctor/Univariate/M.lean
@@ -395,8 +395,7 @@ def isubtree [DecidableEq F.A] [Inhabited (M F)] : Path F → M F → M F
       if h : a = a' then
         isubtree ps (f <| cast (by rw [h]) i)
       else
-        default (α := M F)
-    )
+        default (α := M F))
 
 /-- similar to `isubtree` but returns the data at the end of the path instead
 of the whole subtree -/
diff --git a/Mathlib/Data/Real/ConjExponents.lean b/Mathlib/Data/Real/ConjExponents.lean
@@ -342,7 +342,7 @@ theorem mul_eq_add : p * q = p + q := by
 
 theorem div_conj_eq_sub_one : p / q = p - 1 := by
   field_simp [h.symm.ne_zero]
-  linear_combination - h.sub_one_mul_conj
+  linear_combination -h.sub_one_mul_conj
 
 lemma inv_add_inv_ennreal : (p⁻¹ + q⁻¹ : ℝ≥0∞) = 1 := by norm_cast; exact h.inv_add_inv_eq_one
 
@@ -409,7 +409,7 @@ lemma holderTriple_coe_iff {p q r : ℝ≥0} (hr : r ≠ 0) :
     HolderTriple (p : ℝ≥0∞) (q : ℝ≥0∞) (r : ℝ≥0∞) ↔ NNReal.HolderTriple p q r := by
   refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
   · rw [NNReal.holderTriple_iff]
-    obtain ⟨hp, hq⟩ : p ≠ 0 ∧ q ≠ 0:= by
+    obtain ⟨hp, hq⟩ : p ≠ 0 ∧ q ≠ 0 := by
       constructor
       all_goals
         rintro rfl
diff --git a/Mathlib/Data/Real/Embedding.lean b/Mathlib/Data/Real/Embedding.lean
@@ -170,7 +170,7 @@ theorem embedRealFun_zero : embedRealFun (0 : M) = 0 := by
     rw [mem_upperBounds]
     suffices (∀ (y : ℚ), y.num • (1 : M) < 0 → y ≤ x) → 0 ≤ x by simpa using this
     intro h
-    have h' (y : ℚ) (hy: y < 0) : y ≤ x := by
+    have h' (y : ℚ) (hy : y < 0) : y ≤ x := by
       exact h _ <| (smul_neg_iff_of_neg_left (by simpa using hy)).mpr zero_lt_one
     contrapose! h'
     obtain ⟨y, hxy, hy⟩ := exists_rat_btwn h'
@@ -201,7 +201,7 @@ def embedReal : M →+o ℝ where
   map_add' := embedRealFun_add
   monotone' := (embedRealFun_strictMono M).monotone
 
-theorem embedReal_apply (a : M) :  embedReal M a = embedRealFun a := by rfl
+theorem embedReal_apply (a : M) : embedReal M a = embedRealFun a := by rfl
 
 variable (M) in
 theorem embedReal_injective : Function.Injective (embedReal M) :=
diff --git a/Mathlib/Data/Seq/Computation.lean b/Mathlib/Data/Seq/Computation.lean
@@ -220,8 +220,7 @@ theorem corec_eq (f : β → α ⊕ β) (b : β) : destruct (corec f b) = rmap (
     dsimp [Corec.f, Stream'.corec', Stream'.corec, Stream'.map, Stream'.get, Stream'.iterate]
     match (f b) with
     | Sum.inl x => rfl
-    | Sum.inr x => rfl
-    ]
+    | Sum.inr x => rfl]
   rcases h : f b with a | b'; · rfl
   dsimp [Corec.f, destruct]
   apply congr_arg; apply Subtype.ext
diff --git a/Mathlib/Data/TypeVec.lean b/Mathlib/Data/TypeVec.lean
@@ -423,7 +423,7 @@ def ofRepeat {α : Sort _} : ∀ {n i}, «repeat» n α i → α
 
 theorem const_iff_true {α : TypeVec n} {i x p} : ofRepeat (TypeVec.const p α i x) ↔ p := by
   induction i with
-  | fz      => rfl
+  | fz => rfl
   | fs _ ih =>
     rw [TypeVec.const]
     exact ih
diff --git a/Mathlib/Data/WSeq/Relation.lean b/Mathlib/Data/WSeq/Relation.lean
@@ -391,7 +391,7 @@ theorem liftRel_join.lem (R : α → β → Prop) {S T} {U : WSeq α → WSeq β
       simp only [destruct_join]
       exact ⟨none, mem_bind mT (ret_mem _), by rw [eq_of_pure_mem rs2.mem]; trivial⟩
     | some (s, S'), some (t, T'), ⟨st, ST'⟩, _, rs2, mT => by
-      simp? [destruct_append]  at rs2  says simp only [destruct_join.aux, destruct_append] at rs2
+      simp? [destruct_append] at rs2 says simp only [destruct_join.aux, destruct_append] at rs2
       exact
         let ⟨k1, rs3, ek⟩ := of_results_think rs2
         let ⟨o', m1, n1, rs4, rs5, ek1⟩ := of_results_bind rs3
diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean
@@ -1022,7 +1022,7 @@ theorem neg_val {n : ℕ} [NeZero n] (a : ZMod n) : (-a).val = if a = 0 then 0 e
   rwa [Nat.le_zero, val_eq_zero] at h
 
 theorem val_neg_of_ne_zero {n : ℕ} [nz : NeZero n] (a : ZMod n) [na : NeZero a] :
-    (- a).val = n - a.val := by simp_all [neg_val a, na.out]
+    (-a).val = n - a.val := by simp_all [neg_val a, na.out]
 
 theorem val_sub {n : ℕ} [NeZero n] {a b : ZMod n} (h : b.val ≤ a.val) :
     (a - b).val = a.val - b.val := by
diff --git a/Mathlib/Data/ZMod/Units.lean b/Mathlib/Data/ZMod/Units.lean
@@ -50,7 +50,7 @@ theorem unitsMap_surjective [hm : NeZero m] (h : n ∣ m) :
     have ⟨k, hk⟩ := this x.val.val (val_coe_unit_coprime x)
     refine ⟨unitOfCoprime _ hk, Units.ext ?_⟩
     have : NeZero n := ⟨fun hn ↦ hm.out (eq_zero_of_zero_dvd (hn ▸ h))⟩
-    simp [unitsMap_def, - castHom_apply]
+    simp [unitsMap_def, -castHom_apply]
   intro x hx
   let ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
   use ps.prod id
