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