chore(Computability): fix whitespace (#33172)

Found by extending the commandStart linter to proof bodies.

Author: harahu

Mathlib/Computability/AkraBazzi/AkraBazzi.lean

@@ -188,7 +188,7 @@ lemma growsPolynomially_deriv_rpow_p_mul_one_sub_smoothingFn (p : ℝ) :
       (GrowsPolynomially.pow 2 growsPolynomially_log ?_)
     filter_upwards [eventually_ge_atTop 1] with _ hx using log_nonneg hx
   | inr hp => -- p ≠ 0
-    refine GrowsPolynomially.of_isTheta (growsPolynomially_rpow (p-1))
+    refine GrowsPolynomially.of_isTheta (growsPolynomially_rpow (p - 1))
       (isTheta_deriv_rpow_p_mul_one_sub_smoothingFn hp) ?_
     filter_upwards [eventually_gt_atTop 0] with _ _
     positivity
@@ -208,7 +208,7 @@ lemma growsPolynomially_deriv_rpow_p_mul_one_add_smoothingFn (p : ℝ) :
       (GrowsPolynomially.pow 2 growsPolynomially_log ?_)
     filter_upwards [eventually_ge_atTop 1] with x hx using log_nonneg hx
   | inr hp => -- p ≠ 0
-    refine GrowsPolynomially.of_isTheta (growsPolynomially_rpow (p-1))
+    refine GrowsPolynomially.of_isTheta (growsPolynomially_rpow (p - 1))
       (isTheta_deriv_rpow_p_mul_one_add_smoothingFn hp) ?_
     filter_upwards [eventually_gt_atTop 0] with _ _
     positivity
@@ -583,9 +583,9 @@ lemma T_isBigO_smoothingFn_mul_asympBound :
         refine mul_nonpos_of_nonpos_of_nonneg ?_ g_pos
         rw [sub_nonpos]
         calc 1
-          _ ≤ 2 * (c₁⁻¹ * c₁) * (1/2) := by
+          _ ≤ 2 * (c₁⁻¹ * c₁) * (1 / 2) := by
             rw [inv_mul_cancel₀ (by positivity : c₁ ≠ 0)]; norm_num
-          _ = (2 * c₁⁻¹) * c₁ * (1/2) := by ring
+          _ = (2 * c₁⁻¹) * c₁ * (1 / 2) := by ring
           _ ≤ C * c₁ * (1 - ε n) := by
             gcongr
             · rw [hC]; exact le_max_left _ _

Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean

@@ -220,7 +220,7 @@ lemma eventually_atTop_nonneg_or_nonpos (hf : GrowsPolynomially f) :
                         _ ≤ ((1 : ℝ) / (2 : ℝ)) * (2 : ℝ) ^ n * max n₀ 2 := by gcongr; norm_num
                         _ ≤ _ := by rw [mul_assoc]; gcongr; exact_mod_cast hz.1
           case ub =>
-            have h₁ : (2 : ℝ)^n = ((1 : ℝ)/(2 : ℝ)) * (2 : ℝ)^(n + 1) := by
+            have h₁ : (2 : ℝ)^n = ((1 : ℝ) / (2 : ℝ)) * (2 : ℝ)^(n + 1) := by
               rw [one_div, pow_add, pow_one]
               ring
             rw [h₁, mul_assoc]
@@ -417,10 +417,10 @@ lemma GrowsPolynomially.add_isLittleO {f g : ℝ → ℝ} (hf : GrowsPolynomiall
     have hfg₂ : ‖g x‖ ≤ 1 / 2 * f x := by
       calc ‖g x‖ ≤ 1 / 2 * ‖f x‖ := hfg' x hbx
            _ = 1 / 2 * f x := by congr; exact norm_of_nonneg (hf₂ _ hbx)
-    have hx_ub : f x + g x ≤ 3/2 * f x := by
+    have hx_ub : f x + g x ≤ 3 / 2 * f x := by
       calc _ ≤ f x + ‖g x‖ := by gcongr; exact le_norm_self (g x)
            _ ≤ f x + 1 / 2 * f x := by gcongr
-           _ = 3/2 * f x := by ring
+           _ = 3 / 2 * f x := by ring
     have hx_lb : 1 / 2 * f x ≤ f x + g x := by
       calc f x + g x ≥ f x - ‖g x‖ := by
                 rw [sub_eq_add_neg, norm_eq_abs]; gcongr; exact neg_abs_le (g x)
@@ -438,15 +438,15 @@ lemma GrowsPolynomially.add_isLittleO {f g : ℝ → ℝ} (hf : GrowsPolynomiall
            _ ≥ f u - 1 / 2 * f u := by gcongr
            _ = 1 / 2 * f u := by ring
            _ ≥ 1 / 2 * (c₁ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).1
-           _ = c₁/3 * (3/2 * f x) := by ring
-           _ ≥ c₁/3 * (f x + g x) := by gcongr
+           _ = c₁ / 3 * (3 / 2 * f x) := by ring
+           _ ≥ c₁ / 3 * (f x + g x) := by gcongr
     case ub =>
       calc _ ≤ f u + ‖g u‖ := by gcongr; exact le_norm_self (g u)
            _ ≤ f u + 1 / 2 * f u := by gcongr
-           _ = 3/2 * f u := by ring
-           _ ≤ 3/2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2
-           _ = 3*c₂ * (1 / 2 * f x) := by ring
-           _ ≤ 3*c₂ * (f x + g x) := by gcongr
+           _ = 3 / 2 * f u := by ring
+           _ ≤ 3 / 2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2
+           _ = 3 * c₂ * (1 / 2 * f x) := by ring
+           _ ≤ 3 * c₂ * (f x + g x) := by gcongr
   | inr hf' => -- f is eventually nonpos
     have hf := hf b hb
     obtain ⟨c₁, hc₁_mem : 0 < c₁, c₂, hc₂_mem : 0 < c₂, hf⟩ := hf
@@ -465,15 +465,15 @@ lemma GrowsPolynomially.add_isLittleO {f g : ℝ → ℝ} (hf : GrowsPolynomiall
       calc _ ≤ f x + ‖g x‖ := by gcongr; exact le_norm_self (g x)
            _ ≤ f x + (-1 / 2 * f x) := by gcongr
            _ = 1 / 2 * f x := by ring
-    have hx_lb : 3/2 * f x ≤ f x + g x := by
+    have hx_lb : 3 / 2 * f x ≤ f x + g x := by
       calc f x + g x ≥ f x - ‖g x‖ := by
                 rw [sub_eq_add_neg, norm_eq_abs]; gcongr; exact neg_abs_le (g x)
            _ ≥ f x + 1 / 2 * f x := by
                   rw [sub_eq_add_neg]
                   gcongr
                   refine le_of_neg_le_neg ?bc.a
                   rwa [neg_neg, ← neg_mul, ← neg_div]
-           _ = 3/2 * f x := by ring
+           _ = 3 / 2 * f x := by ring
     intro u ⟨hu_lb, hu_ub⟩
     have hfu_nonpos : f u ≤ 0 := hf₂ _ hu_lb
     have hfg₃ : ‖g u‖ ≤ -1 / 2 * f u := by
@@ -489,10 +489,10 @@ lemma GrowsPolynomially.add_isLittleO {f g : ℝ → ℝ} (hf : GrowsPolynomiall
                   gcongr
                   refine le_of_neg_le_neg ?_
                   rwa [neg_neg, ← neg_mul, ← neg_div]
-           _ = 3/2 * f u := by ring
-           _ ≥ 3/2 * (c₁ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).1
-           _ = 3*c₁ * (1 / 2 * f x) := by ring
-           _ ≥ 3*c₁ * (f x + g x) := by gcongr
+           _ = 3 / 2 * f u := by ring
+           _ ≥ 3 / 2 * (c₁ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).1
+           _ = 3 * c₁ * (1 / 2 * f x) := by ring
+           _ ≥ 3 * c₁ * (f x + g x) := by gcongr
     case ub =>
       calc _ ≤ f u + ‖g u‖ := by gcongr; exact le_norm_self (g u)
            _ ≤ f u - 1 / 2 * f u := by
@@ -501,8 +501,8 @@ lemma GrowsPolynomially.add_isLittleO {f g : ℝ → ℝ} (hf : GrowsPolynomiall
                 rwa [← neg_mul, ← neg_div]
            _ = 1 / 2 * f u := by ring
            _ ≤ 1 / 2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2
-           _ = c₂/3 * (3/2 * f x) := by ring
-           _ ≤ c₂/3 * (f x + g x) := by gcongr
+           _ = c₂ / 3 * (3 / 2 * f x) := by ring
+           _ ≤ c₂ / 3 * (f x + g x) := by gcongr
 
 protected lemma GrowsPolynomially.inv {f : ℝ → ℝ} (hf : GrowsPolynomially f) :
     GrowsPolynomially fun x => (f x)⁻¹ := by

Mathlib/Computability/NFA.lean

@@ -138,7 +138,7 @@ theorem evalFrom_iUnion {ι : Sort*} (s : ι → Set σ) (x : List α) :
     M.evalFrom (⋃ i, s i) x = ⋃ i, M.evalFrom (s i) x := by
   induction x generalizing s with
   | nil => simp
-  | cons a x ih => simp [stepSet, Set.iUnion_comm (ι:=σ) (ι':=ι), ih]
+  | cons a x ih => simp [stepSet, Set.iUnion_comm (ι := σ) (ι' := ι), ih]
 
 variable (M) in
 theorem evalFrom_iUnion₂ {ι : Sort*} {κ : ι → Sort*} (f : ∀ i, κ i → Set σ) (x : List α) :

Mathlib/Computability/TMToPartrec.lean

@@ -972,7 +972,7 @@ theorem trStmts₁_trans {q q'} : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trSt
     · exact Or.inr (Or.inr <| Or.inr <| q₂_ih h h')
 
 theorem trStmts₁_self (q) : q ∈ trStmts₁ q := by
-  induction q <;> · first | apply Finset.mem_singleton_self|apply Finset.mem_insert_self
+  induction q <;> · first | apply Finset.mem_singleton_self | apply Finset.mem_insert_self
 
 /-- The (finite!) set of machine states visited during the course of evaluation of `c`,
 including the state `ret k` but not any states after that (that is, the states visited while