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