rw [H, isCoprime_zero_right, Int.isUnit_iff_abs_eq] at hcoprime
case inl
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
H : p.im = 0
h : (p.re ^ 2).natAbs = 4
⊢ False
case inl
p : ℤ√(-3)
hcoprime : |p.re| = 1
H : p.im = 0
h : (p.re ^ 2).natAbs = 4
⊢ False