Theorem: Zsqrt3.isUnit_iff (Flt/Edwards.lean)

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

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

State before:
z : ℤ√(-3)
h : abs z.re = 1 ∧ z.im = 0
⊢ Zsqrtd.norm z = 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