apply hcoprime.isUnit_of_dvd' <;>
  simp only [zero_add, mul_comm m, Zsqrtd.smul_re, Zsqrtd.smul_im, dvd_mul_right]
case intro.intro.intro.refine'_1
x : ℤ
hodd : Odd x
h : 1 < abs x
m : ℤ√(-3)
h2 : Zsqrtd.norm 0 < x ^ 2
hcoprime : IsCoprime (0 + m * ↑x).re (0 + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (0 + m * ↑x)
⊢ IsUnit x
no goals