Use decide if possible instead of simp in Sum.lean

Changes

1 changed files (+1/-1)

• Sum.lean
  • @@ -54,7 +54,7 @@ lemma exp_larger' (n : ℕ) (h : 2 ≤ n) : (n - 2) * (n * (n - 1)) < (2 * n - 3
    have : 2 ^ (n + 1) = 4 * 2 ^ (n - 1) := by grind [mul_pow_sub_one] simp only [this, Nat.ofNat_pos, pow_pos, mul_le_mul_iff_left₀, ge_iff_le] grind - · interval_cases n <;> simp + · interval_cases n <;> decide theorem double_sum : Tendsto (fun n : ℕ => ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a)) atTop (𝓝 (1 : ℝ)) := by rw [atTop_basis.tendsto_iff (nhds_basis_Ioo_pos 1)]