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