rw [Multiset.prod_cons] at hcoprime
case pos.intro
p : ℤ√(-3)
him : p.im = 0
t : Multiset (ℤ√(-3))
hcoprime : IsCoprime (p ::ₘ t).prod.re (p ::ₘ t).prod.im
h1 : p ∈ p ::ₘ t
h2 : star p ∈ p ::ₘ t
⊢ IsUnit p
case pos.intro
p : ℤ√(-3)
him : p.im = 0
t : Multiset (ℤ√(-3))
hcoprime : IsCoprime (p * t.prod).re (p * t.prod).im
h1 : p ∈ p ::ₘ t
h2 : star p ∈ p ::ₘ t
⊢ IsUnit p