rw [← Int.isUnit_iff_abs_eq]
case intro.intro.intro.refine'_1
x : ℤ
hodd : Odd x
h : 1 < |x|
m : ℤ√(-3)
h2 : Zsqrtd.norm 0 < x ^ 2
hcoprime : IsCoprime (0 + m * ↑x).re (0 + m * ↑x).im
hfactor : x ∣ (0 + m * ↑x).norm
⊢ |x| = 1
case intro.intro.intro.refine'_1
x : ℤ
hodd : Odd x
h : 1 < |x|
m : ℤ√(-3)
h2 : Zsqrtd.norm 0 < x ^ 2
hcoprime : IsCoprime (0 + m * ↑x).re (0 + m * ↑x).im
hfactor : x ∣ (0 + m * ↑x).norm
⊢ IsUnit x