rw [← Int.isUnit_iff_abs_eq]
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)
⊢ abs x = 1
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