Use interval_cases instead of lots of if-elses

Changes

1 changed files (+7/-15)

• Sum.lean
  • @@ -117,15 +117,12 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    suffices 1 / (n - 1) + (n - 2) / 2 ^ (n - 1) < ε by linarith if hε : 3 / 2 < ε then have : 2 ≤ (n : ℝ) := Nat.ofNat_le_cast.mpr h₁ - have : 1 / ((n : ℝ) - 1) ≤ 1 := by - refine (div_le_one₀ ?_).mpr (by linarith) - linarith + have : 1 / ((n : ℝ) - 1) ≤ 1 := div_le_one₀ (by linarith) |>.mpr (by linarith) suffices ((n : ℝ) - 2) / 2 ^ (n - 1) ≤ 1 / 2 by linarith have h₄ : 2 * (n - 2) ≤ 2 ^ (n - 1) := by - if h₅ : n = 2 then - simp [h₅] - else - exact exp_larger n (by omega) + by_cases h₅ : n > 2 + · exact exp_larger n h₅ + · grind rw [mul_comm, ← one_mul (2 ^ (n - 1))] at h₄ exact (div_le_div_iff₀ (by norm_num) (by norm_num)).mpr (by norm_cast) else
  • @@ -137,14 +134,9 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    omega suffices 1 / ((n : ℝ) - 1) + ((n : ℝ) - 2) / 2 ^ (n - 1) < 3 / n by linarith have h₄ : n * (n - 1) * (n - 2) < (2 * n - 3) * 2 ^ (n - 1) := by - if h₅ : n = 2 then - simp [h₅] - else if h₆ : n = 3 then - simp [h₆] - else if h₇ : n = 4 then - simp [h₇] - else - exact exp_larger' n (by omega) + by_cases h₅ : n > 4 + · exact exp_larger' n h₅ + · interval_cases n <;> simp apply lt_sub_iff_add_lt'.mp have h₅ : 3 / (n : ℝ) - 1 / (n - 1) = (2 * n - 3) / (n * (n - 1)) := by have : (n : ℝ) ≠ 0 := by grind [Nat.cast_ne_zero]