case mp
α : Type u_1
f : α → ℝ≥0
⊢ (Summable fun a => ↑(f a)) → Summable f

case mpr
α : Type u_1
f : α → ℝ≥0
⊢ Summable f → Summable fun a => ↑(f a)
α : Type u_1
f : α → ℝ≥0
⊢ (Summable fun a => ↑(f a)) ↔ Summable f
constructor
case mpr
α : Type u_1
f : α → ℝ≥0
⊢ Summable f → Summable fun a => ↑(f a)
case mp
α : Type u_1
f : α → ℝ≥0
⊢ (Summable fun a => ↑(f a)) → Summable f

case mpr
α : Type u_1
f : α → ℝ≥0
⊢ Summable f → Summable fun a => ↑(f a)
exact fun ⟨a, ha⟩ => ⟨⟨a, ha.nonneg fun x => (f x).2⟩, hasSum_coe.1 ha⟩
no goals
case mpr
α : Type u_1
f : α → ℝ≥0
⊢ Summable f → Summable fun a => ↑(f a)
exact fun ⟨a, ha⟩ => ⟨a.1, hasSum_coe.2 ha⟩