Theorem: eq_or_eq_conj_iff_associated'_of_nonneg (FltRegular/FltThree/Edwards.lean)

State before:
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
⊢ Associated' x A ↔ x = A ∨ x = star A
Tactic:
constructor
State after:
case mp
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
⊢ Associated' x A → x = A ∨ x = star A

case mpr
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
⊢ x = A ∨ x = star A → Associated' x A

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

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

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

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

State before:
case pos
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
hu : x * ↑u = A
v : ℤ
hv1 : ↑u = ↑v
hv2 : |v| = 1
hxre : x.re = 0
⊢ x = A ∨ x = star A
Tactic:
apply eq_or_eq_conj_of_associated_of_re_zero hxre ⟨u, hu⟩
State after:
no goals

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

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

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

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

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

State before:
case neg.inl.h
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hu : x * ↑v = A
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = 1
⊢ x = A
Tactic:
rw [← hu, habsv, Int.cast_one, mul_one]
State after:
no goals

State before:
case neg.inr
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hu : x * ↑v = A
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
⊢ x = A ∨ x = star A
Tactic:
exfalso
State after:
case neg.inr
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hu : x * ↑v = A
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
⊢ False

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

State before:
case neg.inr
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = A
⊢ False
Tactic:
apply lt_irrefl (0 : ℤ)
State after:
case neg.inr
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = A
⊢ 0 < 0

State before:
case neg.inr
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = A
⊢ 0 < 0
Tactic:
calc
  0 ≤ A.re := hA
  _ = -x.re := ?_
  _ < 0 := ?_
State after:
case neg.inr.calc_1
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = A
⊢ A.re = -x.re

case neg.inr.calc_2
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = A
⊢ -x.re < 0

State before:
case neg.inr.calc_1
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = A
⊢ A.re = -x.re
Tactic:
simp only [← hu, Zsqrtd.neg_re]
State after:
no goals

State before:
case neg.inr.calc_2
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = A
⊢ -x.re < 0
Tactic:
simp only [neg_neg_iff_pos]
State after:
case neg.inr.calc_2
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = A
⊢ 0 < x.re

State before:
case neg.inr.calc_2
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = A
⊢ 0 < x.re
Tactic:
exact lt_of_le_of_ne hx (Ne.symm hxre)
State after:
no goals

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

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

State before:
case pos
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
hu : x * ↑u = star A
v : ℤ
hv1 : ↑u = ↑v
hv2 : |v| = 1
hxre : x.re = 0
⊢ x = A ∨ x = star A
Tactic:
convert(eq_or_eq_conj_of_associated_of_re_zero hxre ⟨u, hu⟩).symm
State after:
case h.e'_1.h.e'_3
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
hu : x * ↑u = star A
v : ℤ
hv1 : ↑u = ↑v
hv2 : |v| = 1
hxre : x.re = 0
⊢ A = star (star A)

State before:
case h.e'_1.h.e'_3
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
hu : x * ↑u = star A
v : ℤ
hv1 : ↑u = ↑v
hv2 : |v| = 1
hxre : x.re = 0
⊢ A = star (star A)
Tactic:
rw [star_star]
State after:
no goals

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

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

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

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

State before:
case neg.inl
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hu : x * ↑v = star A
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = 1
⊢ x = A ∨ x = star A
Tactic:
right
State after:
case neg.inl.h
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hu : x * ↑v = star A
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = 1
⊢ x = star A

State before:
case neg.inl.h
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hu : x * ↑v = star A
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = 1
⊢ x = star A
Tactic:
rw [← hu, habsv, Int.cast_one, mul_one]
State after:
no goals

State before:
case neg.inr
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hu : x * ↑v = star A
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
⊢ x = A ∨ x = star A
Tactic:
exfalso
State after:
case neg.inr
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hu : x * ↑v = star A
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
⊢ False

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

State before:
case neg.inr
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = star A
⊢ False
Tactic:
apply lt_irrefl (0 : ℤ)
State after:
case neg.inr
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = star A
⊢ 0 < 0

State before:
case neg.inr
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = star A
⊢ 0 < 0
Tactic:
calc
  0 ≤ A.re := hA
  _ = -x.re := ?_
  _ < 0 := ?_
State after:
case neg.inr.calc_1
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = star A
⊢ A.re = -x.re

case neg.inr.calc_2
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = star A
⊢ -x.re < 0

State before:
case neg.inr.calc_1
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = star A
⊢ A.re = -x.re
Tactic:
rw [← star_star A, ← hu]
State after:
case neg.inr.calc_1
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = star A
⊢ (star (-x)).re = -x.re

State before:
case neg.inr.calc_1
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = star A
⊢ (star (-x)).re = -x.re
Tactic:
simp only [Zsqrtd.neg_re, Zsqrtd.star_re]
State after:
no goals

State before:
case neg.inr.calc_2
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = star A
⊢ -x.re < 0
Tactic:
simp only [neg_neg_iff_pos]
State after:
case neg.inr.calc_2
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = star A
⊢ 0 < x.re

State before:
case neg.inr.calc_2
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
u : (ℤ√(-3))ˣ
v : ℤ
hv1 : ↑u = ↑v
hxre : ¬x.re = 0
habsv : v = -1
hu : -x = star A
⊢ 0 < x.re
Tactic:
apply lt_of_le_of_ne hx (Ne.symm hxre)
State after:
no goals

State before:
case mpr
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
⊢ x = A ∨ x = star A → Associated' x A
Tactic:
rintro (rfl | rfl)
State after:
case mpr.inl
x : ℤ√(-3)
hx hA : 0 ≤ x.re
⊢ Associated' x x

case mpr.inr
A : ℤ√(-3)
hA : 0 ≤ A.re
hx : 0 ≤ (star A).re
⊢ Associated' (star A) A

State before:
case mpr.inl
x : ℤ√(-3)
hx hA : 0 ≤ x.re
⊢ Associated' x x
Tactic:
rfl
State after:
no goals

State before:
case mpr.inr
A : ℤ√(-3)
hA : 0 ≤ A.re
hx : 0 ≤ (star A).re
⊢ Associated' (star A) A
Tactic:
right
State after:
case mpr.inr.h
A : ℤ√(-3)
hA : 0 ≤ A.re
hx : 0 ≤ (star A).re
⊢ Associated (star A) (star A)

State before:
case mpr.inr.h
A : ℤ√(-3)
hA : 0 ≤ A.re
hx : 0 ≤ (star A).re
⊢ Associated (star A) (star A)
Tactic:
rfl
State after:
no goals