Add space after ← in rw to follow mathlib style

Changes

1 changed files (+9/-9)

• Sum.lean
  • @@ -19,7 +19,7 @@ lemma geom_sum (b : ℝ) (N : ℕ) (h₁ : 2 ≤ N) (h₂ : 2 ≤ b) : ∑ a ∈
    _ = 1 / (b - 1) - 1 / b - 1 / (b ^ (N - 1) * (b - 1)) := by have h₃ : b ≠ 0 := by linarith have h₄ : b ^ N * (b - 1) = b * (b ^ (N - 1) * (b - 1)) := by - rw [←mul_assoc, ←pow_succ' b (N - 1), Nat.sub_one_add_one] + rw [← mul_assoc, ← pow_succ' b (N - 1), Nat.sub_one_add_one] linarith simp [h₄, div_mul_cancel_left₀ h₃]
  • @@ -52,7 +52,7 @@ lemma exp_larger (n : ℕ) (h : 3 ≤ n) : 2 * (n - 2) ≤ 2 ^ (n - 1) := by
    rename_i m simp simp at a - rw [←mul_pow_sub_one] + rw [← mul_pow_sub_one] grind omega
  • @@ -67,14 +67,14 @@ lemma exp_larger' (n : ℕ) (h : 5 ≤ n) : n * (n - 1) * (n - 2) < (2 * n - 3)
    simp simp at a suffices (m + 1) * m * (m - 1) ≤ 2 * (m * (m - 1) * (m - 2)) by grind - rw [←mul_assoc, mul_assoc] + rw [← mul_assoc, mul_assoc] nth_rw 3 [mul_comm] - nth_rw 2 [←mul_assoc] + nth_rw 2 [← mul_assoc] apply Nat.mul_le_mul_right (m * (m - 1)) omega suffices 2 ^ (n + 1) ≤ (2 * n - 3) * 2 ^ (n - 1) by linarith have h₂ : 2 ^ (n + 1) = 2 * (2 * 2 ^ (n - 1)) := by grind [mul_pow_sub_one] - rw [h₂, ←mul_assoc] + rw [h₂, ← mul_assoc] apply Nat.mul_le_mul_right (2 ^ (n - 1)) omega
  • @@ -100,12 +100,12 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    refine (div_le_one₀ ?_).mpr (by linarith) linarith have h₆ : 1 / (b : ℝ) ^ (n - 1) ≤ 1 / 2 ^ (n - 1) := by - rw [←one_div_pow, ←one_div_pow] + rw [← one_div_pow, ← one_div_pow] apply pow_le_pow_left₀ (by norm_num) simp exact inv_anti₀ (by norm_num) h₄ - rw [←one_div_mul_one_div, mul_comm] - nth_rw 5 [←one_mul 1] + rw [← one_div_mul_one_div, mul_comm] + nth_rw 5 [← one_mul 1] rw [mul_div_assoc] exact mul_le_mul h₅ h₆ (by norm_num) (by norm_num) have h₄ : ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ ∑ b ∈ Ico 2 n, 1 / 2 ^ (n - 1) := sum_le_sum h₃
  • @@ -126,7 +126,7 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    simp [h₅] else exact exp_larger n (by omega) - rw [mul_comm, ←one_mul (2 ^ (n - 1))] at h₄ + rw [mul_comm, ← one_mul (2 ^ (n - 1))] at h₄ exact (div_le_div_iff₀ (by norm_num) (by norm_num)).mpr (by norm_cast) else simp at hε