apply IsCoprime.isUnit_of_dvd' hcoprime <;>
  simp only [add_zero, Zsqrtd.intCast_re, MulZeroClass.zero_mul, dvd_mul_right, Zsqrtd.mul_re,
    MulZeroClass.mul_zero, Zsqrtd.mul_im, Zsqrtd.intCast_im]
case neg.intro.intro
p : ℤ√(-3)
him : ¬p.im = 0
this✝ : star p ≠ p
t2 : Multiset (ℤ√(-3))
hcoprime : IsCoprime (↑p.norm * t2.prod).re (↑p.norm * t2.prod).im
h1 : p ∈ p ::ₘ star p ::ₘ t2
h2 : star p ∈ p ::ₘ star p ::ₘ t2
this : star p ∈ star p ::ₘ t2
⊢ IsUnit p.norm
no goals