rw [him, isCoprime_zero_right, Int.isUnit_iff_abs_eq] at hcoprime
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hfour : Zsqrtd.norm p = 4
him : p.im = 0
⊢ False
p : ℤ√(-3)
hcoprime : abs p.re = 1
hfour : Zsqrtd.norm p = 4
him : p.im = 0
⊢ False