Slight cleanupHEADmaster

1 files changed, 1 insertions, 1 deletions

diff --git a/sum.lean b/sum.lean
index d972d60..9ceeb0a 100644
--- a/sum.lean
+++ b/sum.lean
@@ -232,7 +232,7 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
               rw [←h₁₁]
               norm_cast
               omega
-            field_simp [h₈, h₉]
+            field_simp
             ring
           rw [h₇]
           have h₈ : ((n : ℝ) - 2) * (n * (n - 1)) < (2 * n - 3) * 2 ^ (n - 1) := by