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

State before:
z : ℤ√(-3)
h : IsUnit z
⊢ ∃ u, z = ↑↑u
Tactic:
obtain ⟨u, hu⟩ := Zsqrt3.isUnit_iff.mp h
State after:
case intro
z : ℤ√(-3)
h : IsUnit z
u : abs z.re = 1
hu : z.im = 0
⊢ ∃ u, z = ↑↑u

State before:
case intro
z : ℤ√(-3)
h : IsUnit z
u : abs z.re = 1
hu : z.im = 0
⊢ ∃ u, z = ↑↑u
Tactic:
obtain ⟨v, hv⟩ : IsUnit z.re := by rwa [Int.isUnit_iff_abs_eq]
State after:
case intro.intro
z : ℤ√(-3)
h : IsUnit z
u : abs z.re = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ ∃ u, z = ↑↑u

State before:
case intro.intro
z : ℤ√(-3)
h : IsUnit z
u : abs z.re = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ ∃ u, z = ↑↑u
Tactic:
use v
State after:
case intro.intro
z : ℤ√(-3)
h : IsUnit z
u : abs z.re = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ z = ↑↑v

State before:
case intro.intro
z : ℤ√(-3)
h : IsUnit z
u : abs z.re = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ z = ↑↑v
Tactic:
rw [Zsqrtd.ext, hu, ← hv]
State after:
case intro.intro
z : ℤ√(-3)
h : IsUnit z
u : abs z.re = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ ↑v = (↑↑v).re ∧ 0 = (↑↑v).im

State before:
case intro.intro
z : ℤ√(-3)
h : IsUnit z
u : abs z.re = 1
hu : z.im = 0
v : ℤˣ
hv : ↑v = z.re
⊢ ↑v = (↑↑v).re ∧ 0 = (↑↑v).im
Tactic:
simp only [Zsqrtd.coe_int_re, and_true_iff, eq_self_iff_true, Zsqrtd.coe_int_im]
State after:
no goals

State before:
z : ℤ√(-3)
h : IsUnit z
u : abs z.re = 1
hu : z.im = 0
⊢ IsUnit z.re
Tactic:
rwa [Int.isUnit_iff_abs_eq]
State after:
no goals