rintro (⟨u, hu⟩ | ⟨u, hu⟩) <;> obtain ⟨v, hv1, hv2⟩ := Zsqrt3.coe_of_isUnit' u.isUnit
case mp
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
⊢ Associated' x A → x = A ∨ x = star A
case mp.inl.intro.intro.intro
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : abs v = 1
⊢ x = A ∨ x = star A

case mp.inr.intro.intro.intro
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
hu : x * ↑u = star A
v : ℤ
hv1 : ↑u = ↑v
hv2 : abs v = 1
⊢ x = A ∨ x = star A