internlm/Lean-Github huggingface dataset:
Theorem: eq_or_eq_conj_of_associated_of_re_zero
Proof 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
Proof 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
Theorem: eq_or_eq_conj_of_associated_of_re_zero
Proof 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
Proof state after:
no goals
Theorem: eq_or_eq_conj_of_associated_of_re_zero
Proof 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
Proof 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
Theorem: eq_or_eq_conj_of_associated_of_re_zero
Proof 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
Proof 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
Theorem: eq_or_eq_conj_of_associated_of_re_zero
Proof 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]
Proof state after:
no goals
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof state before:
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
⊢ Associated' x A ↔ x = A ∨ x = star A
Tactic:
constructor
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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⟩
Proof state after:
no goals
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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]
Proof state after:
no goals
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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 : ℤ)
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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 := ?_
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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]
Proof state after:
no goals
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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]
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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)
Proof state after:
no goals
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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
Proof 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)
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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]
Proof state after:
no goals
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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]
Proof state after:
no goals
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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 : ℤ)
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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 := ?_
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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]
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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]
Proof state after:
no goals
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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]
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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)
Proof state after:
no goals
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof 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)
Proof 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
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof state before:
case mpr.inl
x : ℤ√(-3)
hx hA : 0 ≤ x.re
⊢ Associated' x x
Tactic:
rfl
Proof state after:
no goals
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof state before:
case mpr.inr
A : ℤ√(-3)
hA : 0 ≤ A.re
hx : 0 ≤ (star A).re
⊢ Associated' (star A) A
Tactic:
right
Proof state after:
case mpr.inr.h
A : ℤ√(-3)
hA : 0 ≤ A.re
hx : 0 ≤ (star A).re
⊢ Associated (star A) (star A)
Theorem: eq_or_eq_conj_iff_associated'_of_nonneg
Proof state before:
case mpr.inr.h
A : ℤ√(-3)
hA : 0 ≤ A.re
hx : 0 ≤ (star A).re
⊢ Associated (star A) (star A)
Tactic:
rfl
Proof state after:
no goals
Theorem: step5'
Proof state before:
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
⊢ ∃ g, factorization' hcoprime = 3 • g
Tactic:
obtain ⟨h1, h2⟩ := factorization'_prop hcoprime
Proof state after:
case intro
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
h1 : a = (factorization' hcoprime).prod ∨ a = -(factorization' hcoprime).prod
h2 : ∀ pq ∈ factorization' hcoprime, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
⊢ ∃ g, factorization' hcoprime = 3 • g
Theorem: step5'
Proof state before:
case intro
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
h1 : a = (factorization' hcoprime).prod ∨ a = -(factorization' hcoprime).prod
h2 : ∀ pq ∈ factorization' hcoprime, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
⊢ ∃ g, factorization' hcoprime = 3 • g
Tactic:
set f := factorization' hcoprime with hf
Proof state after:
case intro
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
⊢ ∃ g, f = 3 • g
Theorem: step5'
Proof state before:
case intro
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
⊢ ∃ g, f = 3 • g
Tactic:
apply Multiset.exists_smul_of_dvd_count
Proof state after:
case intro.h
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
⊢ ∀ a ∈ f, 3 ∣ Multiset.count a f
Theorem: step5'
Proof state before:
case intro.h
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
⊢ ∀ a ∈ f, 3 ∣ Multiset.count a f
Tactic:
intro x hx
Proof state after:
case intro.h
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
⊢ 3 ∣ Multiset.count x f
Theorem: step5'
Proof state before:
case intro.h
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
⊢ 3 ∣ Multiset.count x f
Tactic:
convert dvd_mul_right 3 (Multiset.count x.norm.natAbs (factorsOddPrimeOrFour r))
Proof state after:
case h.e'_4
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
⊢ Multiset.count x f = 3 * Multiset.count x.norm.natAbs (factorsOddPrimeOrFour r)
Theorem: step5'
Proof state before:
case h.e'_4
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
⊢ Multiset.count x f = 3 * Multiset.count x.norm.natAbs (factorsOddPrimeOrFour r)
Tactic:
have : Even (evenFactorExp r) :=
  by
  suffices Even (3 * evenFactorExp r)
    by
    rw [Nat.even_mul] at this
    apply this.resolve_left
    norm_num; decide
  rw [← evenFactorExp.pow r 3, hcube]
  exact factors_2_even' hcoprime
Proof state after:
case h.e'_4
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.count x f = 3 * Multiset.count x.norm.natAbs (factorsOddPrimeOrFour r)
Theorem: step5'
Proof state before:
case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
⊢ x = A ↔ x.norm.natAbs = A.norm.natAbs

case h.e'_4.calc_2
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.countP (fun x_1 => x.norm.natAbs = x_1) (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f) =
    Multiset.countP (fun x_1 => x.norm.natAbs = x_1) (factorsOddPrimeOrFour a.norm.natAbs)
Tactic:
swap
Proof state after:
case h.e'_4.calc_2
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.countP (fun x_1 => x.norm.natAbs = x_1) (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f) =
    Multiset.countP (fun x_1 => x.norm.natAbs = x_1) (factorsOddPrimeOrFour a.norm.natAbs)

case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
⊢ x = A ↔ x.norm.natAbs = A.norm.natAbs