More minor tweaks to Sum.lean

Changes

1 changed files (+1/-3)

• Sum.lean
  • @@ -126,9 +126,7 @@ theorem double_sum : Tendsto (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2
    · interval_cases n <;> simp nth_rw 1 [mul_comm] at h₅ rify at h₅ - have h₆ : ↑(n - 1) = (n : ℝ) - 1 := by - rw [Nat.cast_sub (by linarith)] - simp + have h₆ : ↑(n - 1) = (n : ℝ) - 1 := by grind [Nat.cast_sub] have h₇ : ↑(2 * n - 3) = 2 * (n : ℝ) - 3 := by rw [Nat.cast_sub (by linarith)] simp