Theorem: Spts.eq_one' (FltRegular/FltThree/Spts.lean)

State before:
a : ℤ√(-3)
h : a.norm = 1
⊢ a = 1 ∨ a = -1
Tactic:
simp only [Zsqrtd.ext_iff, 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