v : PrimeMultiset
⊢ Multiset.map Subtype.val (Multiset.map Coe.coe v) = Multiset.map Subtype.val v
v : PrimeMultiset
⊢ Multiset.map PNat.val (toPNatMultiset v) = toNatMultiset v
change (v.map (Coe.coe : Nat.Primes → ℕ+)).map Subtype.val = v.map Subtype.val
v : PrimeMultiset
⊢ Multiset.map (Subtype.val ∘ Coe.coe) v = Multiset.map Subtype.val v
v : PrimeMultiset
⊢ Multiset.map Subtype.val (Multiset.map Coe.coe v) = Multiset.map Subtype.val v
rw [Multiset.map_map]
no goals
v : PrimeMultiset
⊢ Multiset.map (Subtype.val ∘ Coe.coe) v = Multiset.map Subtype.val v
congr