Theorem: Zsqrt3.isUnit_iff (FltRegular/FltThree/Edwards.lean)

State before:
z : ℤ√(-3)
⊢ IsUnit z ↔ |z.re| = 1 ∧ z.im = 0
Tactic:
rw [← Zsqrtd.norm_eq_one_iff, ← Int.natCast_inj, Int.ofNat_one,
  Int.natAbs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) z)]
State after:
z : ℤ√(-3)
⊢ z.norm = 1 ↔ |z.re| = 1 ∧ z.im = 0

State before:
z : ℤ√(-3)
⊢ z.norm = 1 ↔ |z.re| = 1 ∧ z.im = 0
Tactic:
refine' ⟨Spts.eq_one, fun h => _⟩
State after:
z : ℤ√(-3)
h : |z.re| = 1 ∧ z.im = 0
⊢ z.norm = 1

State before:
z : ℤ√(-3)
h : |z.re| = 1 ∧ z.im = 0
⊢ z.norm = 1
Tactic:
rw [Zsqrtd.norm_def, h.2, MulZeroClass.mul_zero, sub_zero, ← sq, ← sq_abs, h.1, one_pow]
State after:
no goals

State before:
z : ℤ√(-3)
⊢ -3 ≤ 0
Tactic:
norm_num
State after:
no goals