rw [← Zsqrtd.norm_eq_one_iff, ← Int.coe_nat_inj', Int.ofNat_one,
  Int.natAbs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) z)]
z : ℤ√(-3)
⊢ IsUnit z ↔ abs z.re = 1 ∧ z.im = 0
z : ℤ√(-3)
⊢ Zsqrtd.norm z = 1 ↔ abs z.re = 1 ∧ z.im = 0