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

State before:
z : ℤ√(-3)
h : IsUnit z
⊢ ∃ u, z = ↑u ∧ abs u = 1
Tactic:
obtain ⟨u, hu⟩ := Zsqrt3.coe_of_isUnit h
State after:
case intro
z : ℤ√(-3)
h : IsUnit z
u : ℤˣ
hu : z = ↑↑u
⊢ ∃ u, z = ↑u ∧ abs u = 1

State before:
case intro
z : ℤ√(-3)
h : IsUnit z
u : ℤˣ
hu : z = ↑↑u
⊢ ∃ u, z = ↑u ∧ abs u = 1
Tactic:
refine' ⟨u, _, _⟩
State after:
case intro.refine'_1
z : ℤ√(-3)
h : IsUnit z
u : ℤˣ
hu : z = ↑↑u
⊢ z = ↑↑u

case intro.refine'_2
z : ℤ√(-3)
h : IsUnit z
u : ℤˣ
hu : z = ↑↑u
⊢ abs ↑u = 1

State before:
case intro.refine'_1
z : ℤ√(-3)
h : IsUnit z
u : ℤˣ
hu : z = ↑↑u
⊢ z = ↑↑u
Tactic:
rw [hu]
State after:
no goals

State before:
case intro.refine'_2
z : ℤ√(-3)
h : IsUnit z
u : ℤˣ
hu : z = ↑↑u
⊢ abs ↑u = 1
Tactic:
exact Int.isUnit_iff_abs_eq.mp u.isUnit
State after:
no goals