simp only [← hu, hv1, hx, add_zero, MulZeroClass.zero_mul, Zsqrtd.mul_re, MulZeroClass.mul_zero,
  Zsqrtd.intCast_im]
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : |v| = 1
⊢ A.re = 0
no goals