case mp
α : Type ?u.312905
β : Type ?u.312908
γ : Type ?u.312911
f : ℕ → ℝ≥0
⊢ ¬Summable f → Tendsto (fun n => ∑ i in Finset.range n, f i) atTop atTop

case mpr
α : Type ?u.312905
β : Type ?u.312908
γ : Type ?u.312911
f : ℕ → ℝ≥0
⊢ Tendsto (fun n => ∑ i in Finset.range n, f i) atTop atTop → ¬Summable f
α : Type ?u.312905
β : Type ?u.312908
γ : Type ?u.312911
f : ℕ → ℝ≥0
⊢ ¬Summable f ↔ Tendsto (fun n => ∑ i in Finset.range n, f i) atTop atTop
constructor
case mp
α : Type ?u.312905
β : Type ?u.312908
γ : Type ?u.312911
f : ℕ → ℝ≥0
h : ¬Summable f
⊢ Tendsto (fun n => ∑ i in Finset.range n, f i) atTop atTop
case mp
α : Type ?u.312905
β : Type ?u.312908
γ : Type ?u.312911
f : ℕ → ℝ≥0
⊢ ¬Summable f → Tendsto (fun n => ∑ i in Finset.range n, f i) atTop atTop
intro h
case mp.refine'_1
α : Type ?u.312905
β : Type ?u.312908
γ : Type ?u.312911
f : ℕ → ℝ≥0
h : ¬Summable f
⊢ Monotone fun s => ∑ b in s, f b

case mp.refine'_2
α : Type ?u.312905
β : Type ?u.312908
γ : Type ?u.312911
f : ℕ → ℝ≥0
h : ¬Summable f
⊢ Tendsto (fun n => Finset.range n) atTop atTop
case mp
α : Type ?u.312905
β : Type ?u.312908
γ : Type ?u.312911
f : ℕ → ℝ≥0
h : ¬Summable f
⊢ Tendsto (fun n => ∑ i in Finset.range n, f i) atTop atTop
refine' ((tendsto_of_monotone _).resolve_right h).comp _
no goals
case mp.refine'_1
α : Type ?u.312905
β : Type ?u.312908
γ : Type ?u.312911
f : ℕ → ℝ≥0
h : ¬Summable f
⊢ Monotone fun s => ∑ b in s, f b

case mp.refine'_2
α : Type ?u.312905
β : Type ?u.312908
γ : Type ?u.312911
f : ℕ → ℝ≥0
h : ¬Summable f
⊢ Tendsto (fun n => Finset.range n) atTop atTop
exacts [Finset.sum_mono_set _, tendsto_finset_range]
case mpr.intro
α : Type ?u.312905
β : Type ?u.312908
γ : Type ?u.312911
f : ℕ → ℝ≥0
hnat : Tendsto (fun n => ∑ i in Finset.range n, f i) atTop atTop
r : ℝ≥0
hr : HasSum f r
⊢ False
case mpr
α : Type ?u.312905
β : Type ?u.312908
γ : Type ?u.312911
f : ℕ → ℝ≥0
⊢ Tendsto (fun n => ∑ i in Finset.range n, f i) atTop atTop → ¬Summable f
rintro hnat ⟨r, hr⟩
no goals
case mpr.intro
α : Type ?u.312905
β : Type ?u.312908
γ : Type ?u.312911
f : ℕ → ℝ≥0
hnat : Tendsto (fun n => ∑ i in Finset.range n, f i) atTop atTop
r : ℝ≥0
hr : HasSum f r
⊢ False
exact not_tendsto_nhds_of_tendsto_atTop hnat _ (hasSum_iff_tendsto_nat.1 hr)