awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
obtain :
  ∀ (z : 𝓞 K) (hz : S'.c = λ * z),
    HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 - 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 + 1 ∨
      HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 + 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 - 1
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 - 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 + 1 ∨
    HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 + 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 - 1

Tactic:
obtain ⟨z, hz⟩ := S'.hcdvd

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.hcdvd
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
inl :
  ∀ (x : 𝓞 K) (hx : HPow.hPow (β := ℕ) S'.a 3 - 1 = HPow.hPow (β := ℕ) λ 4 * x),
    HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 - 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 + 1 ∨
      HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 + 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 - 1
inr :
  ∀ (x : 𝓞 K) (hx : HPow.hPow (β := ℕ) S'.a 3 + 1 = HPow.hPow (β := ℕ) λ 4 * x),
    HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 - 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 + 1 ∨
      HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 + 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 - 1
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 - 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 + 1 ∨
    HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 + 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 - 1

Tactic:
rcases lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd hζ S'.ha with
    ⟨x, hx⟩ | ⟨x, hx⟩

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.ha, IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 - 1 = HPow.hPow (β := ℕ) λ 4 * x
inl :
  ∀ (y : 𝓞 K) (hy : HPow.hPow (β := ℕ) S'.b 3 - 1 = HPow.hPow (β := ℕ) λ 4 * y),
    HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 - 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 + 1 ∨
      HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 + 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 - 1
inl₁ :
  ∀ (y : 𝓞 K) (hy : HPow.hPow (β := ℕ) S'.b 3 + 1 = HPow.hPow (β := ℕ) λ 4 * y),
    HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 - 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 + 1 ∨
      HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 + 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 - 1
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 - 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 + 1 ∨
    HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 + 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 - 1

Tactic:
rcases lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd hζ S'.hb with
    ⟨y, hy⟩ | ⟨y, hy⟩

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.hb, IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 + 1 = HPow.hPow (β := ℕ) λ 4 * x
inr :
  ∀ (y : 𝓞 K) (hy : HPow.hPow (β := ℕ) S'.b 3 - 1 = HPow.hPow (β := ℕ) λ 4 * y),
    HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 - 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 + 1 ∨
      HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 + 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 - 1
inr₁ :
  ∀ (y : 𝓞 K) (hy : HPow.hPow (β := ℕ) S'.b 3 + 1 = HPow.hPow (β := ℕ) λ 4 * y),
    HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 - 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 + 1 ∨
      HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 + 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 - 1
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 - 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 + 1 ∨
    HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 + 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 - 1

Tactic:
rcases lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd hζ S'.hb with
    ⟨y, hy⟩ | ⟨y, hy⟩

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.hb, IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 - 1 = HPow.hPow (β := ℕ) λ 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 - 1 = HPow.hPow (β := ℕ) λ 4 * y
inl : False
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 - 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 + 1 ∨
    HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 + 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 - 1

Tactic:
exfalso
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 - 1 = HPow.hPow (β := ℕ) λ 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 - 1 = HPow.hPow (β := ℕ) λ 4 * y
rwa rwa₁ rwa₂ rwa₃ : IsPrimitiveRoot ζ 3
⊢ IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) (β := ℕ) 3 1)

Tactic:
rwa [pow_one]

Premises used: pow_one
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 - 1 = HPow.hPow (β := ℕ) λ 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 - 1 = HPow.hPow (β := ℕ) λ 4 * y
⊢ IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) (β := ℕ) 3 1)

Tactic:
replace hζ : IsPrimitiveRoot ζ (3 ^ 1) := by rwa [pow_one]
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ_1 : IsPrimitiveRoot ζ 3
S' : Solution' hζ_1
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ_1.toInteger - 1) * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 - 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 - 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * y
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) (β := ℕ) 3 1)
⊢ Ne (α := ℕ) 3 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ_1 : IsPrimitiveRoot ζ 3
S' : Solution' hζ_1
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ_1.toInteger - 1) * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 - 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 - 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * y
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) (β := ℕ) 3 1)
inl :
  2 =
    (hζ.toInteger - 1) *
      ((↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 2 * HPow.hPow (β := ℕ) z 3 -
        HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 3 * (x + y))
⊢ False

Tactic:
refine hζ.toInteger_sub_one_not_dvd_two (by decide) ⟨S'.u * λ ^ 2 * z ^ 3 - λ ^ 3 * (x + y), ?_⟩
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ_1 : IsPrimitiveRoot ζ 3
S' : Solution' hζ_1
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ_1.toInteger - 1) * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 - 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 - 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * y
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) (β := ℕ) 3 1)
inl :
  (hζ.toInteger - 1) *
      ((↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 2 * HPow.hPow (β := ℕ) z 3 -
        HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 3 * (x + y)) =
    2
⊢ 2 =
    (hζ.toInteger - 1) *
      ((↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 2 * HPow.hPow (β := ℕ) z 3 -
        HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 3 * (x + y))

Tactic:
symm
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ_1 : IsPrimitiveRoot ζ 3
S' : Solution' hζ_1
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ_1.toInteger - 1) * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 - 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 - 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * y
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) (β := ℕ) 3 1)
⊢ (hζ.toInteger - 1) *
      ((↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 2 * HPow.hPow (β := ℕ) z 3 -
        HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 3 * (x + y)) =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) ((hζ_1.toInteger - 1) * z) 3 - HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * x -
      HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * y

Tactic:
ring
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ_1 : IsPrimitiveRoot ζ 3
S' : Solution' hζ_1
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ_1.toInteger - 1) * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 - 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 - 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * y
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) (β := ℕ) 3 1)
rw :
  (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) ((hζ_1.toInteger - 1) * z) 3 - (HPow.hPow (β := ℕ) S'.a 3 - 1) -
      HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * y =
    HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3 - (HPow.hPow (β := ℕ) S'.a 3 - 1) -
      (HPow.hPow (β := ℕ) S'.b 3 - 1)
rw₁ :
  (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) ((hζ_1.toInteger - 1) * z) 3 - (HPow.hPow (β := ℕ) S'.a 3 - 1) -
      (HPow.hPow (β := ℕ) S'.b 3 - 1) =
    HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3 - (HPow.hPow (β := ℕ) S'.a 3 - 1) -
      (HPow.hPow (β := ℕ) S'.b 3 - 1)
rw₂ :
  (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3 - (HPow.hPow (β := ℕ) S'.a 3 - 1) - (HPow.hPow (β := ℕ) S'.b 3 - 1) =
    HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3 - (HPow.hPow (β := ℕ) S'.a 3 - 1) -
      (HPow.hPow (β := ℕ) S'.b 3 - 1)
rw₃ rw₄ :
  HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3 - (HPow.hPow (β := ℕ) S'.a 3 - 1) -
      (HPow.hPow (β := ℕ) S'.b 3 - 1) =
    HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3 - (HPow.hPow (β := ℕ) S'.a 3 - 1) -
      (HPow.hPow (β := ℕ) S'.b 3 - 1)
⊢ (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) ((hζ_1.toInteger - 1) * z) 3 - HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * x -
      HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * y =
    HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3 - (HPow.hPow (β := ℕ) S'.a 3 - 1) -
      (HPow.hPow (β := ℕ) S'.b 3 - 1)

Tactic:
rw [← hx, ← hy, ← hz, ← S'.H]

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.H
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ_1 : IsPrimitiveRoot ζ 3
S' : Solution' hζ_1
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ_1.toInteger - 1) * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 - 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 - 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * y
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) (β := ℕ) 3 1)
⊢ HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3 - (HPow.hPow (β := ℕ) S'.a 3 - 1) -
      (HPow.hPow (β := ℕ) S'.b 3 - 1) =
    2

Tactic:
ring
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ_1 : IsPrimitiveRoot ζ 3
S' : Solution' hζ_1
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ_1.toInteger - 1) * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 - 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 - 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * y
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) (β := ℕ) 3 1)
calc :
  (hζ.toInteger - 1) *
      ((↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 2 * HPow.hPow (β := ℕ) z 3 -
        HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 3 * (x + y)) =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) ((hζ_1.toInteger - 1) * z) 3 - HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * x -
      HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * y
calc₁ :
  (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) ((hζ_1.toInteger - 1) * z) 3 - HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * x -
      HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * y =
    HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3 - (HPow.hPow (β := ℕ) S'.a 3 - 1) -
      (HPow.hPow (β := ℕ) S'.b 3 - 1)
calc₂ :
  HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3 - (HPow.hPow (β := ℕ) S'.a 3 - 1) -
      (HPow.hPow (β := ℕ) S'.b 3 - 1) =
    2
⊢ (hζ.toInteger - 1) *
      ((↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 2 * HPow.hPow (β := ℕ) z 3 -
        HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 3 * (x + y)) =
    2

Tactic:
calc _ = S'.u * (λ * z) ^ 3 - λ ^ 4 * x - λ ^ 4 * y := by ring
    _ = (S'.a ^ 3 + S'.b ^ 3) - (S'.a ^ 3 - 1) - (S'.b ^ 3 - 1) := by rw [← hx, ← hy, ← hz, ← S'.H]
    _ = 2 := by ring

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.a, _private.0.FermatLastTheoremForThreeGen.Solution'.u, HSub.hSub, HPow.hPow, HAdd.hAdd, _private.0.FermatLastTheoremForThreeGen.Solution'.b, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 - 1 = HPow.hPow (β := ℕ) λ 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 + 1 = HPow.hPow (β := ℕ) λ 4 * y
inl : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 - 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 + 1
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 - 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 + 1 ∨
    HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 + 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 - 1

Tactic:
left
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 - 1 = HPow.hPow (β := ℕ) λ 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 + 1 = HPow.hPow (β := ℕ) λ 4 * y
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 - 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 + 1

Tactic:
⟨⟨x, hx⟩, ⟨y, hy⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 - 1 = HPow.hPow (β := ℕ) λ 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 + 1 = HPow.hPow (β := ℕ) λ 4 * y
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 - 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 + 1

Tactic:
exact ⟨⟨x, hx⟩, ⟨y, hy⟩⟩
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 + 1 = HPow.hPow (β := ℕ) λ 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 - 1 = HPow.hPow (β := ℕ) λ 4 * y
inr : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 + 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 - 1
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 - 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 + 1 ∨
    HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 + 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 - 1

Tactic:
right
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 + 1 = HPow.hPow (β := ℕ) λ 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 - 1 = HPow.hPow (β := ℕ) λ 4 * y
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 + 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 - 1

Tactic:
⟨⟨x, hx⟩, ⟨y, hy⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 + 1 = HPow.hPow (β := ℕ) λ 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 - 1 = HPow.hPow (β := ℕ) λ 4 * y
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 + 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 - 1

Tactic:
exact ⟨⟨x, hx⟩, ⟨y, hy⟩⟩
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 + 1 = HPow.hPow (β := ℕ) λ 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 + 1 = HPow.hPow (β := ℕ) λ 4 * y
inr : False
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 - 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 + 1 ∨
    HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.a 3 + 1 ∧ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.b 3 - 1

Tactic:
exfalso
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 + 1 = HPow.hPow (β := ℕ) λ 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 + 1 = HPow.hPow (β := ℕ) λ 4 * y
rwa rwa₁ rwa₂ rwa₃ : IsPrimitiveRoot ζ 3
⊢ IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) (β := ℕ) 3 1)

Tactic:
rwa [pow_one]

Premises used: pow_one
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 + 1 = HPow.hPow (β := ℕ) λ 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 + 1 = HPow.hPow (β := ℕ) λ 4 * y
⊢ IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) (β := ℕ) 3 1)

Tactic:
replace hζ : IsPrimitiveRoot ζ (3 ^ 1) := by rwa [pow_one]
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ_1 : IsPrimitiveRoot ζ 3
S' : Solution' hζ_1
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ_1.toInteger - 1) * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 + 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 + 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * y
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) (β := ℕ) 3 1)
⊢ Ne (α := ℕ) 3 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ_1 : IsPrimitiveRoot ζ 3
S' : Solution' hζ_1
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ_1.toInteger - 1) * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 + 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 + 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * y
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) (β := ℕ) 3 1)
inr :
  2 =
    (hζ.toInteger - 1) *
      (HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 3 * (x + y) -
        (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 2 * HPow.hPow (β := ℕ) z 3)
⊢ False

Tactic:
refine hζ.toInteger_sub_one_not_dvd_two (by decide) ⟨λ ^ 3 * (x + y) - S'.u * λ ^ 2 * z ^ 3, ?_⟩
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ_1 : IsPrimitiveRoot ζ 3
S' : Solution' hζ_1
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ_1.toInteger - 1) * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 + 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 + 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * y
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) (β := ℕ) 3 1)
inr :
  (hζ.toInteger - 1) *
      (HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 3 * (x + y) -
        (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 2 * HPow.hPow (β := ℕ) z 3) =
    2
⊢ 2 =
    (hζ.toInteger - 1) *
      (HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 3 * (x + y) -
        (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 2 * HPow.hPow (β := ℕ) z 3)

Tactic:
symm
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ_1 : IsPrimitiveRoot ζ 3
S' : Solution' hζ_1
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ_1.toInteger - 1) * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 + 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 + 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * y
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) (β := ℕ) 3 1)
⊢ (hζ.toInteger - 1) *
      (HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 3 * (x + y) -
        (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 2 * HPow.hPow (β := ℕ) z 3) =
    HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * x + HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * y -
      (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) ((hζ_1.toInteger - 1) * z) 3

Tactic:
ring
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ_1 : IsPrimitiveRoot ζ 3
S' : Solution' hζ_1
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ_1.toInteger - 1) * z
x : 𝓞 K
hx : HPow.hPow (β := ℕ) S'.a 3 + 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * x
y : 𝓞 K
hy : HPow.hPow (β := ℕ) S'.b 3 + 1 = HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * y
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) (β := ℕ) 3 1)
rw :
  HPow.hPow (β := ℕ) S'.a 3 + 1 + HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * y -
      (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) ((hζ_1.toInteger - 1) * z) 3 =
    HPow.hPow (β := ℕ) S'.a 3 + 1 + (HPow.hPow (β := ℕ) S'.b 3 + 1) -
      (HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3)
rw₁ :
  HPow.hPow (β := ℕ) S'.a 3 + 1 + (HPow.hPow (β := ℕ) S'.b 3 + 1) -
      (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) ((hζ_1.toInteger - 1) * z) 3 =
    HPow.hPow (β := ℕ) S'.a 3 + 1 + (HPow.hPow (β := ℕ) S'.b 3 + 1) -
      (HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3)
rw₂ :
  HPow.hPow (β := ℕ) S'.a 3 + 1 + (HPow.hPow (β := ℕ) S'.b 3 + 1) - (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3 =
    HPow.hPow (β := ℕ) S'.a 3 + 1 + (HPow.hPow (β := ℕ) S'.b 3 + 1) -
      (HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3)
rw₃ rw₄ :
  HPow.hPow (β := ℕ) S'.a 3 + 1 + (HPow.hPow (β := ℕ) S'.b 3 + 1) -
      (HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3) =
    HPow.hPow (β := ℕ) S'.a 3 + 1 + (HPow.hPow (β := ℕ) S'.b 3 + 1) -
      (HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3)
⊢ HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * x + HPow.hPow (β := ℕ) (hζ_1.toInteger - 1) 4 * y -
      (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) ((hζ_1.toInteger - 1) * z) 3 =
    HPow.hPow (β := ℕ) S'.a 3 + 1 + (HPow.hPow (β := ℕ) S'.b 3 + 1) -
      (HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3)

Tactic:
rw [← hx, ← hy, ← hz, ← S'.H]

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.H