v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => { val := ↑p, property := hp }) v h) = v
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
⊢ toPNatMultiset (ofPNatMultiset v h) = v
dsimp [ofPNatMultiset, toPNatMultiset]
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
this : (fun p h => Coe.coe { val := ↑p, property := h }) = fun p x => id p
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => { val := ↑p, property := hp }) v h) = v
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => { val := ↑p, property := hp }) v h) = v
have : (fun (p : ℕ+) (h : p.Prime) => (Coe.coe : Nat.Primes → ℕ+) ⟨p, h⟩) = fun p _ => id p := by
  funext p h
  apply Subtype.eq
  rfl
no goals
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
this : (fun p h => Coe.coe { val := ↑p, property := h }) = fun p x => id p
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => { val := ↑p, property := hp }) v h) = v
rw [Multiset.map_pmap, this, Multiset.pmap_eq_map, Multiset.map_id]
case h.h
v : Multiset ℕ+
h✝ : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
p : ℕ+
h : PNat.Prime p
⊢ Coe.coe { val := ↑p, property := h } = id p
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
⊢ (fun p h => Coe.coe { val := ↑p, property := h }) = fun p x => id p
funext p h
case h.h.a
v : Multiset ℕ+
h✝ : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
p : ℕ+
h : PNat.Prime p
⊢ ↑(Coe.coe { val := ↑p, property := h }) = ↑(id p)
case h.h
v : Multiset ℕ+
h✝ : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
p : ℕ+
h : PNat.Prime p
⊢ Coe.coe { val := ↑p, property := h } = id p
apply Subtype.eq
no goals
case h.h.a
v : Multiset ℕ+
h✝ : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
p : ℕ+
h : PNat.Prime p
⊢ ↑(Coe.coe { val := ↑p, property := h }) = ↑(id p)
rfl