cases' hre with h1 h1 <;> cases' him with h2 h2 <;>
  [
    (left; use 1);
    (right; use 1);
    (right; use -1);
    (left; use -1)
  ] <;>
  simp [Zsqrtd.ext_iff, h1, h2]
x y : ℤ√(-3)
hre : x.re = y.re ∨ x.re = -y.re
him : x.im = y.im ∨ x.im = -y.im
⊢ Associated' x y
no goals