Theorem: eq_or_eq_conj_of_associated_of_re_zero (FltRegular/FltThree/Edwards.lean)

State before:
x A : ℤ√(-3)
hx : x.re = 0
h : Associated x A
⊢ x = A ∨ x = star A
Tactic:
obtain ⟨u, hu⟩ := h
State after:
case intro
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
⊢ x = A ∨ x = star A

State before:
case intro
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
⊢ x = A ∨ x = star A
Tactic:
obtain ⟨v, hv1, hv2⟩ := Zsqrt3.coe_of_isUnit' u.isUnit
State after:
case intro.intro.intro
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : |v| = 1
⊢ x = A ∨ x = star A

State before:
case intro.intro.intro
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : |v| = 1
⊢ x = A ∨ x = star A
Tactic:
have hA : A.re = 0 := by
  simp only [← hu, hv1, hx, add_zero, MulZeroClass.zero_mul, Zsqrtd.mul_re, MulZeroClass.mul_zero,
    Zsqrtd.intCast_im]
State after:
case intro.intro.intro
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : |v| = 1
hA : A.re = 0
⊢ x = A ∨ x = star A

State before:
case intro.intro.intro
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : |v| = 1
hA : A.re = 0
⊢ x = A ∨ x = star A
Tactic:
rw [abs_eq <| zero_le_one' ℤ] at hv2
State after:
case intro.intro.intro
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : v = 1 ∨ v = -1
hA : A.re = 0
⊢ x = A ∨ x = star A

State before:
case intro.intro.intro
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : v = 1 ∨ v = -1
hA : A.re = 0
⊢ x = A ∨ x = star A
Tactic:
cases' hv2 with hv2 hv2
State after:
case intro.intro.intro.inl
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hA : A.re = 0
hv2 : v = 1
⊢ x = A ∨ x = star A

case intro.intro.intro.inr
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hA : A.re = 0
hv2 : v = -1
⊢ x = A ∨ x = star A

State before:
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : |v| = 1
⊢ A.re = 0
Tactic:
simp only [← hu, hv1, hx, add_zero, MulZeroClass.zero_mul, Zsqrtd.mul_re, MulZeroClass.mul_zero,
  Zsqrtd.intCast_im]
State after:
no goals

State before:
case intro.intro.intro.inl
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hA : A.re = 0
hv2 : v = 1
⊢ x = A ∨ x = star A
Tactic:
left
State after:
case intro.intro.intro.inl.h
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hA : A.re = 0
hv2 : v = 1
⊢ x = A

State before:
case intro.intro.intro.inl.h
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hA : A.re = 0
hv2 : v = 1
⊢ x = A
Tactic:
simpa only [hv1, hv2, mul_one, Int.cast_one] using hu
State after:
no goals

State before:
case intro.intro.intro.inr
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hA : A.re = 0
hv2 : v = -1
⊢ x = A ∨ x = star A
Tactic:
right
State after:
case intro.intro.intro.inr.h
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hA : A.re = 0
hv2 : v = -1
⊢ x = star A

State before:
case intro.intro.intro.inr.h
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hA : A.re = 0
hv2 : v = -1
⊢ x = star A
Tactic:
simp only [hv1, hv2, mul_one, Int.cast_one, mul_neg, Int.cast_neg] at hu
State after:
case intro.intro.intro.inr.h
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hA : A.re = 0
hv2 : v = -1
hu : -x = A
⊢ x = star A

State before:
case intro.intro.intro.inr.h
x A : ℤ√(-3)
hx : x.re = 0
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hA : A.re = 0
hv2 : v = -1
hu : -x = A
⊢ x = star A
Tactic:
simp [← hu, hx, Zsqrtd.ext_iff]
State after:
no goals