case intro.mk.intro
v : PrimeMultiset
p : ℕ+
h : p ∈ toPNatMultiset v
val✝ : ℕ
hp' : Nat.Prime val✝
left✝ : { val := val✝, property := hp' } ∈ v
h_eq : Coe.coe { val := val✝, property := hp' } = p
⊢ PNat.Prime p
v : PrimeMultiset
p : ℕ+
h : p ∈ toPNatMultiset v
⊢ PNat.Prime p
rcases Multiset.mem_map.mp h with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩
no goals
case intro.mk.intro
v : PrimeMultiset
p : ℕ+
h : p ∈ toPNatMultiset v
val✝ : ℕ
hp' : Nat.Prime val✝
left✝ : { val := val✝, property := hp' } ∈ v
h_eq : Coe.coe { val := val✝, property := hp' } = p
⊢ PNat.Prime p
exact h_eq ▸ hp'