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

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

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

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

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

theorem NNRat.coe_sum {α : Type u_2} {s : Finset α} {f : α → ℚ≥0} : ↑(Finset.sum s fun (a : α) => f a) = Finset.sum s fun (a : α) => ↑(f a)

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

theorem NNRat.coe_prod {α : Type u_2} {s : Finset α} {f : α → ℚ≥0} : ↑(Finset.prod s fun (a : α) => f a) = Finset.prod s fun (a : α) => ↑(f a)

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