rw [Zsqrtd.norm_def, mul_assoc, ← Int.natAbs_mul_self' a.re, ← Int.abs_eq_natAbs, H, one_mul,
  neg_mul, sub_neg_eq_add, add_right_eq_self, mul_eq_zero, mul_self_eq_zero] at h
a : ℤ√(-3)
h : a.norm = 1
H : |a.re| = 1
⊢ a.im = 0
a : ℤ√(-3)
h : 3 = 0 ∨ a.im = 0
H : |a.re| = 1
⊢ a.im = 0