exact h2.resolve_left this
p : ℤ√(-3)
him : ¬p.im = 0
this : star p ≠ p
t1 : Multiset (ℤ√(-3))
hcoprime : IsCoprime (Multiset.prod (p ::ₘ t1)).re (Multiset.prod (p ::ₘ t1)).im
h1 : p ∈ p ::ₘ t1
h2 : star p = p ∨ star p ∈ t1
⊢ star p ∈ t1
no goals