α : Type ?u.348849
β : Type ?u.348852
γ : Type ?u.348855
f : ℕ → ℝ
c : ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
h : ∀ (n : ℕ), ∑ i in Finset.range n, f i ≤ c
H : Tendsto (fun n => ∑ i in Finset.range n, f i) atTop atTop
⊢ False
α : Type ?u.348849
β : Type ?u.348852
γ : Type ?u.348855
f : ℕ → ℝ
c : ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
h : ∀ (n : ℕ), ∑ i in Finset.range n, f i ≤ c
⊢ Summable f
refine (summable_iff_not_tendsto_nat_atTop_of_nonneg hf).2 fun H => ?_
case intro.intro
α : Type ?u.348849
β : Type ?u.348852
γ : Type ?u.348855
f : ℕ → ℝ
c : ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
h : ∀ (n : ℕ), ∑ i in Finset.range n, f i ≤ c
H : Tendsto (fun n => ∑ i in Finset.range n, f i) atTop atTop
n : ℕ
hn : c < ∑ i in Finset.range n, f i
⊢ False
α : Type ?u.348849
β : Type ?u.348852
γ : Type ?u.348855
f : ℕ → ℝ
c : ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
h : ∀ (n : ℕ), ∑ i in Finset.range n, f i ≤ c
H : Tendsto (fun n => ∑ i in Finset.range n, f i) atTop atTop
⊢ False
rcases exists_lt_of_tendsto_atTop H 0 c with ⟨n, -, hn⟩
no goals
case intro.intro
α : Type ?u.348849
β : Type ?u.348852
γ : Type ?u.348855
f : ℕ → ℝ
c : ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
h : ∀ (n : ℕ), ∑ i in Finset.range n, f i ≤ c
H : Tendsto (fun n => ∑ i in Finset.range n, f i) atTop atTop
n : ℕ
hn : c < ∑ i in Finset.range n, f i
⊢ False
exact lt_irrefl _ (hn.trans_le (h n))