simp only [him, add_zero, MulZeroClass.zero_mul, Zsqrtd.mul_im, Zsqrtd.mul_re,
  MulZeroClass.mul_zero] at hcoprime
case pos.intro
p : ℤ√(-3)
him : p.im = 0
t : Multiset (ℤ√(-3))
hcoprime : IsCoprime (p * Multiset.prod t).re (p * Multiset.prod t).im
h1 : p ∈ p ::ₘ t
h2 : star p ∈ p ::ₘ t
⊢ IsUnit p
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 * (Multiset.prod t).re) (p.re * (Multiset.prod t).im)
⊢ IsUnit p