v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
⊢ Multiset.prod (toPNatMultiset (ofPNatMultiset v h)) = Multiset.prod v
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
⊢ prod (ofPNatMultiset v h) = Multiset.prod v
dsimp [prod]
no goals
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
⊢ Multiset.prod (toPNatMultiset (ofPNatMultiset v h)) = Multiset.prod v
rw [to_ofPNatMultiset]