no goals
α : Type u_1
β : Type ?u.333384
γ : Type ?u.333387
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≠ ⊤
⊢ ENNReal.toReal (∑' (a : α), f a) = ∑' (a : α), ENNReal.toReal (f a)
simp only [ENNReal.toReal, tsum_toNNReal_eq hf, NNReal.coe_tsum]