v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => { val := p, property := hp }) v h) = v
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
⊢ toNatMultiset (ofNatMultiset v h) = v
dsimp [ofNatMultiset, toNatMultiset]
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.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 → Nat.Prime p
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => { val := p, property := hp }) v h) = v
have : (fun p h => (Coe.coe : Nat.Primes → ℕ) ⟨p, h⟩) = fun p _ => id p := by
  funext p h
  rfl
no goals
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.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 → Nat.Prime p
p : ℕ
h : Nat.Prime p
⊢ Coe.coe { val := p, property := h } = id p
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
⊢ (fun p h => Coe.coe { val := p, property := h }) = fun p x => id p
funext p h
no goals
case h.h
v : Multiset ℕ
h✝ : ∀ (p : ℕ), p ∈ v → Nat.Prime p
p : ℕ
h : Nat.Prime p
⊢ Coe.coe { val := p, property := h } = id p
rfl