by_cases him : p.im = 0
case intro
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
h1 : p ∈ s
h2 : star p ∈ s
⊢ IsUnit p
case pos
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
h1 : p ∈ s
h2 : star p ∈ s
him : p.im = 0
⊢ IsUnit p

case neg
s : Multiset (ℤ√(-3))
p : ℤ√(-3)
hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im
h1 : p ∈ s
h2 : star p ∈ s
him : ¬p.im = 0
⊢ IsUnit p