Slightly clean up Sum.lean, try out simp_rw

Changes

1 changed files (+5/-5)

• Sum.lean
  • @@ -75,7 +75,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 - repeat rw [one_div] + simp_rw [one_div] exact inv_anti₀ (by norm_num) <| pow_le_pow_left₀ (by norm_num) h₃ (n - 1) grw [h₄, h₅] simp
  • @@ -102,10 +102,10 @@ theorem double_sum : Tendsto (fun n : ℕ => ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    have h₃ : 0 < (2 : ℝ) ^ (n - 1) := by norm_num exact div_lt_div_iff₀ h₃ (by nlinarith) |>.mpr h₂ · -- Less than 1 - have h₂ b (bico : b ∈ Ico 2 n) : 0 < (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by - rw [one_div_pos] + have h₂ b (bico : b ∈ Ico 2 n) : 0 ≤ (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by + rw [one_div_nonneg] have : 1 < (b : ℝ) := Nat.one_lt_cast.mpr (List.left_le_of_mem_range' bico) - exact mul_pos (pow_pos (by linarith) (n - 1)) (by linarith) - have := sum_nonneg <| fun b a => le_of_lt (h₂ b a) + exact mul_nonneg (pow_nonneg (by linarith) (n - 1)) (by linarith) + have := sum_nonneg h₂ have : 0 < (1 : ℝ) / (n - 1) := by simp [Nat.one_lt_cast.mpr h₁] grind