α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ ∑ i in s, f i = ∑ a in s, ↑(Real.toNNReal (f a))
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ Real.toNNReal (∑ a in s, f a) = ∑ a in s, Real.toNNReal (f a)
rw [← NNReal.coe_eq, NNReal.coe_sum, Real.coe_toNNReal _ (Finset.sum_nonneg hf)]
no goals
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ ∑ i in s, f i = ∑ a in s, ↑(Real.toNNReal (f a))
exact Finset.sum_congr rfl fun x hxs => by rw [Real.coe_toNNReal _ (hf x hxs)]
no goals
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
x : α
hxs : x ∈ s
⊢ f x = ↑(Real.toNNReal (f x))
rw [Real.coe_toNNReal _ (hf x hxs)]