α : Type u_1
β : Type ?u.203569
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ≥0∞
hf : ∀ (a : α), a ∈ s → f a ≠ ⊤
⊢ ∑ a in s, ↑(ENNReal.toNNReal (f a)) = ∑ a in s, ENNReal.toReal (f a)
α : Type u_1
β : Type ?u.203569
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ≥0∞
hf : ∀ (a : α), a ∈ s → f a ≠ ⊤
⊢ ENNReal.toReal (∑ a in s, f a) = ∑ a in s, ENNReal.toReal (f a)
rw [ENNReal.toReal, toNNReal_sum hf, NNReal.coe_sum]
no goals
α : Type u_1
β : Type ?u.203569
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ≥0∞
hf : ∀ (a : α), a ∈ s → f a ≠ ⊤
⊢ ∑ a in s, ↑(ENNReal.toNNReal (f a)) = ∑ a in s, ENNReal.toReal (f a)
rfl