apply eq_or_eq_conj_of_associated_of_re_zero hxre ⟨u, hu⟩
case pos
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : |v| = 1
hxre : x.re = 0
⊢ x = A ∨ x = star A
no goals