no goals
α : Type ?u.313966
β : Type ?u.313969
γ : Type ?u.313972
f : ℕ → ℝ≥0
⊢ Summable f ↔ ¬Tendsto (fun n => ∑ i in Finset.range n, f i) atTop atTop
rw [← not_iff_not, Classical.not_not, not_summable_iff_tendsto_nat_atTop]