use v
case intro.intro
z : ℤ√(-3)
h : IsUnit z
u : abs z.re = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ ∃ u, z = ↑↑u
case intro.intro
z : ℤ√(-3)
h : IsUnit z
u : abs z.re = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ z = ↑↑v