Casting lemmas for non-negative rational numbers involving sums and products

theorem NNRat.coe_list_sum (l : List ℚ≥0) : ↑l.sum = (List.map NNRat.cast l).sum

theorem NNRat.coe_list_prod (l : List ℚ≥0) : ↑l.prod = (List.map NNRat.cast l).prod

theorem NNRat.coe_multiset_sum (s : Multiset ℚ≥0) : ↑s.sum = (Multiset.map NNRat.cast s).sum

theorem NNRat.coe_multiset_prod (s : Multiset ℚ≥0) : ↑s.prod = (Multiset.map NNRat.cast s).prod

theorem NNRat.coe_sum {α : Type u_2} {s : Finset α} {f : α → ℚ≥0} : ↑(∑ a ∈ s, f a) = ∑ a ∈ s, ↑(f a)

theorem NNRat.toNNRat_sum_of_nonneg {α : Type u_2} {s : Finset α} {f : α → ℚ} (hf : ∀ a ∈ s, 0 ≤ f a) : (∑ a ∈ s, f a).toNNRat = ∑ a ∈ s, (f a).toNNRat

theorem NNRat.coe_prod {α : Type u_2} {s : Finset α} {f : α → ℚ≥0} : ↑(∏ a ∈ s, f a) = ∏ a ∈ s, ↑(f a)

theorem NNRat.toNNRat_prod_of_nonneg {α : Type u_2} {s : Finset α} {f : α → ℚ} (hf : ∀ a ∈ s, 0 ≤ f a) : (∏ a ∈ s, f a).toNNRat = ∏ a ∈ s, (f a).toNNRat