simp only [hv1, hv2, mul_one, Int.cast_one, mul_neg, Int.cast_neg] at hu
case intro.intro.intro.inr.h
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hA : A.re = 0
hv2 : v = -1
⊢ x = star A
case intro.intro.intro.inr.h
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hA : A.re = 0
hv2 : v = -1
hu : -x = A
⊢ x = star A