Theorem: Spts.eq_one' (Flt/Spts.lean)

State before:
a : ℤ√(-3)
h : Zsqrtd.norm a = 1
⊢ a = 1 ∨ a = -1
Tactic:
simp only [Zsqrtd.ext, Zsqrtd.one_re, Zsqrtd.one_im, Zsqrtd.neg_im, Zsqrtd.neg_re, neg_zero, ←
  or_and_right, ← abs_eq (zero_le_one' ℤ), Spts.eq_one h, eq_self_iff_true, and_self_iff]
State after:
no goals