v : PrimeMultiset
h : ↑(prod v) = Multiset.prod (Multiset.map Coe.coe (Multiset.map Coe.coe v)) :=
  MonoidHom.map_multiset_prod PNat.coeMonoidHom (toPNatMultiset v)
⊢ ↑(prod v) = Multiset.prod (toNatMultiset v)
v : PrimeMultiset
⊢ ↑(prod v) = Multiset.prod (toNatMultiset v)
let h : (v.prod : ℕ) = ((v.map Coe.coe).map Coe.coe).prod :=
  PNat.coeMonoidHom.map_multiset_prod v.toPNatMultiset
v : PrimeMultiset
h : ↑(prod v) = Multiset.prod (Multiset.map (Coe.coe ∘ Coe.coe) v)
⊢ ↑(prod v) = Multiset.prod (toNatMultiset v)
v : PrimeMultiset
h : ↑(prod v) = Multiset.prod (Multiset.map Coe.coe (Multiset.map Coe.coe v)) :=
  MonoidHom.map_multiset_prod PNat.coeMonoidHom (toPNatMultiset v)
⊢ ↑(prod v) = Multiset.prod (toNatMultiset v)
rw [Multiset.map_map] at h
v : PrimeMultiset
h : ↑(prod v) = Multiset.prod (Multiset.map (Coe.coe ∘ Coe.coe) v)
this : Coe.coe ∘ Coe.coe = Coe.coe
⊢ ↑(prod v) = Multiset.prod (toNatMultiset v)
v : PrimeMultiset
h : ↑(prod v) = Multiset.prod (Multiset.map (Coe.coe ∘ Coe.coe) v)
⊢ ↑(prod v) = Multiset.prod (toNatMultiset v)
have : (Coe.coe : ℕ+ → ℕ) ∘ (Coe.coe : Nat.Primes → ℕ+) = Coe.coe := funext fun p => rfl
v : PrimeMultiset
h : ↑(prod v) = Multiset.prod (Multiset.map Coe.coe v)
this : Coe.coe ∘ Coe.coe = Coe.coe
⊢ ↑(prod v) = Multiset.prod (toNatMultiset v)
v : PrimeMultiset
h : ↑(prod v) = Multiset.prod (Multiset.map (Coe.coe ∘ Coe.coe) v)
this : Coe.coe ∘ Coe.coe = Coe.coe
⊢ ↑(prod v) = Multiset.prod (toNatMultiset v)
rw [this] at h
no goals
v : PrimeMultiset
h : ↑(prod v) = Multiset.prod (Multiset.map Coe.coe v)
this : Coe.coe ∘ Coe.coe = Coe.coe
⊢ ↑(prod v) = Multiset.prod (toNatMultiset v)
exact h