simp only [Zsqrtd.coe_int_re, and_true_iff, eq_self_iff_true, Zsqrtd.coe_int_im]
case intro.intro
z : ℤ√(-3)
h : IsUnit z
u : abs z.re = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ ↑v = (↑↑v).re ∧ 0 = (↑↑v).im
no goals