l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
this : ↑(prod (ofNatMultiset (↑l) h)) = Multiset.prod ↑l
⊢ ↑(prod (ofNatList l h)) = List.prod l
l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
⊢ ↑(prod (ofNatList l h)) = List.prod l
have := prod_ofNatMultiset (l : Multiset ℕ) h
l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
this : ↑(prod (ofNatMultiset (↑l) h)) = List.prod l
⊢ ↑(prod (ofNatList l h)) = List.prod l
l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
this : ↑(prod (ofNatMultiset (↑l) h)) = Multiset.prod ↑l
⊢ ↑(prod (ofNatList l h)) = List.prod l
rw [Multiset.coe_prod] at this
no goals
l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
this : ↑(prod (ofNatMultiset (↑l) h)) = List.prod l
⊢ ↑(prod (ofNatList l h)) = List.prod l
exact this