Minor simplification

Changes

1 changed files (+2/-5)

• Sum.lean
  • @@ -101,12 +101,9 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    linarith have h₆ : 1 / (b : ℝ) ^ (n - 1) ≤ 1 / 2 ^ (n - 1) := by rw [←one_div_pow, ←one_div_pow] - apply pow_le_pow_left₀ - norm_num + apply pow_le_pow_left₀ (by norm_num) simp - apply inv_anti₀ at h₄ - exact h₄ - norm_num + exact inv_anti₀ (by norm_num) h₄ rw [←one_div_mul_one_div, mul_comm] nth_rw 5 [←one_mul 1] rw [mul_div_assoc]