no goals
α : Type u_1
β : Type ?u.231026
γ : Type ?u.231029
a b c d : ℝ≥0∞
r✝ p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : α → ℝ≥0
r : ℝ≥0
hr : HasSum f r
⊢ ↑(tsum f) = ∑' (a : α), ↑(f a)
rw [hr.tsum_eq, ENNReal.tsum_coe_eq hr]