α : Type u_1
p q : ℚ≥0
s : Finset α
f : α → ℚ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ ∑ i in s, f i = ∑ a in s, ↑(toNNRat (f a))
α : Type u_1
p q : ℚ≥0
s : Finset α
f : α → ℚ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ toNNRat (∑ a in s, f a) = ∑ a in s, toNNRat (f a)
rw [← coe_inj, coe_sum, Rat.coe_toNNRat _ (Finset.sum_nonneg hf)]
no goals
α : Type u_1
p q : ℚ≥0
s : Finset α
f : α → ℚ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ ∑ i in s, f i = ∑ a in s, ↑(toNNRat (f a))
exact Finset.sum_congr rfl fun x hxs ↦ by rw [Rat.coe_toNNRat _ (hf x hxs)]
no goals
α : Type u_1
p q : ℚ≥0
s : Finset α
f : α → ℚ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
x : α
hxs : x ∈ s
⊢ f x = ↑(toNNRat (f x))
rw [Rat.coe_toNNRat _ (hf x hxs)]