Use repeat rw instead of simp only in Sum.lean

Changes

1 changed files (+1/-1)

• Sum.lean
  • @@ -76,7 +76,7 @@ theorem double_sum : Tendsto (fun n : ℕ => ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    exact (List.left_le_of_mem_range' bico) have h₄ : 1 / ((b : ℝ) - 1) ≤ 1 := div_le_one₀ (by linarith) |>.mpr (by linarith) have h₅ : 1 / (b : ℝ) ^ (n - 1) ≤ 1 / 2 ^ (n - 1) := by - simp only [one_div] + repeat rw [one_div] exact inv_anti₀ (by norm_num) <| pow_le_pow_left₀ (by norm_num) h₃ (n - 1) grw [h₄, h₅] simp