rw [Zsqrtd.ext_iff, hu, ← hv]
case h
z : ℤ√(-3)
h : IsUnit z
u : |z.re| = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ z = ↑↑v
case h
z : ℤ√(-3)
h : IsUnit z
u : |z.re| = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ ↑v = (↑↑v).re ∧ 0 = (↑↑v).im