Use rify more effectively

Changes

1 changed files (+4/-7)

• Sum.lean
  • @@ -47,7 +47,7 @@ lemma exp_larger (n : ℕ) (h : 2 ≤ n) : 2 * (n - 2) ≤ 2 ^ (n - 1) := by
    · grind -- Another similar lemma - lemma exp_larger' (n : ℕ) (h : 2 ≤ n) : n * (n - 1) * (n - 2) < (2 * n - 3) * 2 ^ (n - 1) := by + lemma exp_larger' (n : ℕ) (h : 2 ≤ n) : (n - 2) * (n * (n - 1)) < (2 * n - 3) * 2 ^ (n - 1) := by by_cases h : 4 < n · have : n * (n - 1) * (n - 2) < 2 ^ (n + 1) := by induction h
  • @@ -118,14 +118,11 @@ theorem double_sum : Tendsto (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2
    rw [h₃] have h₄ : ((n : ℝ) - 2) * (n * (n - 1)) < (2 * n - 3) * 2 ^ (n - 1) := by have h₅ := exp_larger' n h₁ - nth_rw 1 [mul_comm] at h₅ - rify at h₅ - have h₆ : ↑(n - 1) = (n : ℝ) - 1 := by grind [Nat.cast_sub] - have h₇ : ↑(2 * n - 3) = 2 * (n : ℝ) - 3 := by + have h₆ : ↑(2 * n - 3) = 2 * (n : ℝ) - 3 := by rw [Nat.cast_sub (by linarith)] simp - have h₈ : ↑(n - 2) = (n : ℝ) - 2 := by norm_cast - rwa [h₆, h₇, h₈] at h₅ + rify [h₁, h₆] at h₅ + grind [Nat.cast_sub] have h₅ : 0 < (2 : ℝ) ^ (n - 1) := by norm_num exact (div_lt_div_iff₀ h₅ (by nlinarith)).mpr h₄ ring_nf at h₃