no goals
α : Type u_1
β : Type ?u.229498
γ : Type ?u.229501
a b c d : ℝ≥0∞
r✝ p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : α → ℝ≥0
r : ℝ≥0
⊢ HasSum (fun a => ↑(f a)) ↑r ↔ HasSum f r
simp only [HasSum, ← coe_finset_sum, tendsto_coe]