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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
HZ : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Z 3 + 1
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Y
hcong :
  ∀ (Z : 𝓞 K) (hZ : HPow.hPow (β := ℕ) S.Z 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Z),
    ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)
⊢ ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
rcases HZ with ⟨Z, hZ⟩

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.Z
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Y
Z : 𝓞 K
hZ : HPow.hPow (β := ℕ) S.Z 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Z
⊢ ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
⟨-1, X - Y - S.u₄ * Z, ?_⟩

Premises used: Units.val, HMul.hMul, HSub.hSub, Exists.intro, OfNat.ofNat, Neg.neg, _private.0.FermatLastTheoremForThreeGen.Solution.u₄
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Y
Z : 𝓞 K
hZ : HPow.hPow (β := ℕ) S.Z 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Z
hcong : (↑S.u₄ : 𝓞 K) - (↑(-1) : 𝓞 K) = HPow.hPow (β := ℕ) λ 2 * (X - Y - (↑S.u₄ : 𝓞 K) * Z)
⊢ ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
refine ⟨-1, X - Y - S.u₄ * Z, ?_⟩
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Y
Z : 𝓞 K
hZ : HPow.hPow (β := ℕ) S.Z 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Z
⊢ HPow.hPow (β := ℕ) λ 2 * (X - Y - (↑S.u₄ : 𝓞 K) * Z) =
    HPow.hPow (β := ℕ) λ 2 * X - HPow.hPow (β := ℕ) λ 2 * Y - (↑S.u₄ : 𝓞 K) * (HPow.hPow (β := ℕ) λ 2 * Z)

Tactic:
ring
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Y
Z : 𝓞 K
hZ : HPow.hPow (β := ℕ) S.Z 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Z
hcong :
  (↑S.u₄ : 𝓞 K) - (↑(-1) : 𝓞 K) =
    HPow.hPow (β := ℕ) S.Y 3 + (↑S.u₄ : 𝓞 K) * HPow.hPow (β := ℕ) S.Z 3 - (HPow.hPow (β := ℕ) S.Y 3 - 1) -
      (↑S.u₄ : 𝓞 K) * (HPow.hPow (β := ℕ) S.Z 3 - 1)
⊢ (↑S.u₄ : 𝓞 K) - (↑(-1) : 𝓞 K) = HPow.hPow (β := ℕ) λ 2 * (X - Y - (↑S.u₄ : 𝓞 K) * Z)

Tactic:
rw [show λ ^ 2 * (X - Y - S.u₄ * Z) = λ ^ 2 * X - λ ^ 2 * Y - S.u₄ * (λ ^ 2 * Z) by ring,
      ← hX, ← hY, ← hZ, ← formula2]

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.formula2
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Y
Z : 𝓞 K
hZ : HPow.hPow (β := ℕ) S.Z 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Z
⊢ (↑S.u₄ : 𝓞 K) - (↑(-1) : 𝓞 K) =
    HPow.hPow (β := ℕ) S.Y 3 + (↑S.u₄ : 𝓞 K) * HPow.hPow (β := ℕ) S.Z 3 - (HPow.hPow (β := ℕ) S.Y 3 - 1) -
      (↑S.u₄ : 𝓞 K) * (HPow.hPow (β := ℕ) S.Z 3 - 1)

Tactic:
ring
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Y
Z : 𝓞 K
hZ : HPow.hPow (β := ℕ) S.Z 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Z
⊢ ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
⟨1, -X + Y + S.u₄ * Z, ?_⟩

Premises used: Units.val, HMul.hMul, HAdd.hAdd, Exists.intro, OfNat.ofNat, Neg.neg, _private.0.FermatLastTheoremForThreeGen.Solution.u₄
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Y
Z : 𝓞 K
hZ : HPow.hPow (β := ℕ) S.Z 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Z
hcong : (↑S.u₄ : 𝓞 K) - (↑1 : 𝓞 K) = HPow.hPow (β := ℕ) λ 2 * (-X + Y + (↑S.u₄ : 𝓞 K) * Z)
⊢ ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
refine ⟨1, -X + Y + S.u₄ * Z, ?_⟩
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Y
Z : 𝓞 K
hZ : HPow.hPow (β := ℕ) S.Z 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Z
⊢ HPow.hPow (β := ℕ) λ 2 * (-X + Y + (↑S.u₄ : 𝓞 K) * Z) =
    -(HPow.hPow (β := ℕ) λ 2 * X - HPow.hPow (β := ℕ) λ 2 * Y - (↑S.u₄ : 𝓞 K) * (HPow.hPow (β := ℕ) λ 2 * Z))

Tactic:
ring
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Y
Z : 𝓞 K
hZ : HPow.hPow (β := ℕ) S.Z 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Z
hcong :
  (↑S.u₄ : 𝓞 K) - (↑1 : 𝓞 K) =
    -(HPow.hPow (β := ℕ) S.Y 3 + (↑S.u₄ : 𝓞 K) * HPow.hPow (β := ℕ) S.Z 3 - (HPow.hPow (β := ℕ) S.Y 3 - 1) -
        (↑S.u₄ : 𝓞 K) * (HPow.hPow (β := ℕ) S.Z 3 + 1))
⊢ (↑S.u₄ : 𝓞 K) - (↑1 : 𝓞 K) = HPow.hPow (β := ℕ) λ 2 * (-X + Y + (↑S.u₄ : 𝓞 K) * Z)

Tactic:
rw [show λ ^ 2 * (-X + Y + S.u₄ * Z) = -(λ ^ 2 * X - λ ^ 2 * Y - S.u₄ * (λ ^ 2 * Z)) by ring,
      ← hX, ← hY, ← hZ, ← formula2]

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.formula2
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Y
Z : 𝓞 K
hZ : HPow.hPow (β := ℕ) S.Z 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Z
⊢ (↑S.u₄ : 𝓞 K) - (↑1 : 𝓞 K) =
    -(HPow.hPow (β := ℕ) S.Y 3 + (↑S.u₄ : 𝓞 K) * HPow.hPow (β := ℕ) S.Z 3 - (HPow.hPow (β := ℕ) S.Y 3 - 1) -
        (↑S.u₄ : 𝓞 K) * (HPow.hPow (β := ℕ) S.Z 3 + 1))

Tactic:
ring
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Y
Z : 𝓞 K
hZ : HPow.hPow (β := ℕ) S.Z 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Z
⊢ ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
⟨1, X - Y - S.u₄ * Z, ?_⟩

Premises used: Units.val, HMul.hMul, HSub.hSub, Exists.intro, OfNat.ofNat, _private.0.FermatLastTheoremForThreeGen.Solution.u₄
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Y
Z : 𝓞 K
hZ : HPow.hPow (β := ℕ) S.Z 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Z
hcong : (↑S.u₄ : 𝓞 K) - (↑1 : 𝓞 K) = HPow.hPow (β := ℕ) λ 2 * (X - Y - (↑S.u₄ : 𝓞 K) * Z)
⊢ ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
refine ⟨1, X - Y - S.u₄ * Z, ?_⟩
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Y
Z : 𝓞 K
hZ : HPow.hPow (β := ℕ) S.Z 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Z
⊢ HPow.hPow (β := ℕ) λ 2 * (X - Y - (↑S.u₄ : 𝓞 K) * Z) =
    HPow.hPow (β := ℕ) λ 2 * X - HPow.hPow (β := ℕ) λ 2 * Y - (↑S.u₄ : 𝓞 K) * (HPow.hPow (β := ℕ) λ 2 * Z)

Tactic:
ring
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Y
Z : 𝓞 K
hZ : HPow.hPow (β := ℕ) S.Z 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Z
hcong :
  (↑S.u₄ : 𝓞 K) - (↑1 : 𝓞 K) =
    HPow.hPow (β := ℕ) S.Y 3 + (↑S.u₄ : 𝓞 K) * HPow.hPow (β := ℕ) S.Z 3 - (HPow.hPow (β := ℕ) S.Y 3 + 1) -
      (↑S.u₄ : 𝓞 K) * (HPow.hPow (β := ℕ) S.Z 3 - 1)
⊢ (↑S.u₄ : 𝓞 K) - (↑1 : 𝓞 K) = HPow.hPow (β := ℕ) λ 2 * (X - Y - (↑S.u₄ : 𝓞 K) * Z)

Tactic:
rw [show λ ^ 2 * (X - Y - S.u₄ * Z) = λ ^ 2 * X - λ ^ 2 * Y - S.u₄ * (λ ^ 2 * Z) by ring,
      ← hX, ← hY, ← hZ, ← formula2]

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.formula2
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Y
Z : 𝓞 K
hZ : HPow.hPow (β := ℕ) S.Z 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Z
⊢ (↑S.u₄ : 𝓞 K) - (↑1 : 𝓞 K) =
    HPow.hPow (β := ℕ) S.Y 3 + (↑S.u₄ : 𝓞 K) * HPow.hPow (β := ℕ) S.Z 3 - (HPow.hPow (β := ℕ) S.Y 3 + 1) -
      (↑S.u₄ : 𝓞 K) * (HPow.hPow (β := ℕ) S.Z 3 - 1)

Tactic:
ring
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Y
Z : 𝓞 K
hZ : HPow.hPow (β := ℕ) S.Z 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Z
⊢ ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
⟨-1, -X + Y + S.u₄ * Z, ?_⟩

Premises used: Units.val, HMul.hMul, HAdd.hAdd, Exists.intro, OfNat.ofNat, Neg.neg, _private.0.FermatLastTheoremForThreeGen.Solution.u₄
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Y
Z : 𝓞 K
hZ : HPow.hPow (β := ℕ) S.Z 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Z
hcong : (↑S.u₄ : 𝓞 K) - (↑(-1) : 𝓞 K) = HPow.hPow (β := ℕ) λ 2 * (-X + Y + (↑S.u₄ : 𝓞 K) * Z)
⊢ ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
refine ⟨-1, -X + Y + S.u₄ * Z, ?_⟩
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Y
Z : 𝓞 K
hZ : HPow.hPow (β := ℕ) S.Z 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Z
⊢ HPow.hPow (β := ℕ) λ 2 * (-X + Y + (↑S.u₄ : 𝓞 K) * Z) =
    -(HPow.hPow (β := ℕ) λ 2 * X - HPow.hPow (β := ℕ) λ 2 * Y - (↑S.u₄ : 𝓞 K) * (HPow.hPow (β := ℕ) λ 2 * Z))

Tactic:
ring
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Y
Z : 𝓞 K
hZ : HPow.hPow (β := ℕ) S.Z 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Z
hcong :
  (↑S.u₄ : 𝓞 K) - (↑(-1) : 𝓞 K) =
    -(HPow.hPow (β := ℕ) S.Y 3 + (↑S.u₄ : 𝓞 K) * HPow.hPow (β := ℕ) S.Z 3 - (HPow.hPow (β := ℕ) S.Y 3 + 1) -
        (↑S.u₄ : 𝓞 K) * (HPow.hPow (β := ℕ) S.Z 3 + 1))
⊢ (↑S.u₄ : 𝓞 K) - (↑(-1) : 𝓞 K) = HPow.hPow (β := ℕ) λ 2 * (-X + Y + (↑S.u₄ : 𝓞 K) * Z)

Tactic:
rw [show λ ^ 2 * (-X + Y + S.u₄ * Z) = -(λ ^ 2 * X - λ ^ 2 * Y - S.u₄ * (λ ^ 2 * Z)) by ring,
      ← hX, ← hY, ← hZ, ← formula2]

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.formula2
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Y
Z : 𝓞 K
hZ : HPow.hPow (β := ℕ) S.Z 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Z
⊢ (↑S.u₄ : 𝓞 K) - (↑(-1) : 𝓞 K) =
    -(HPow.hPow (β := ℕ) S.Y 3 + (↑S.u₄ : 𝓞 K) * HPow.hPow (β := ℕ) S.Z 3 - (HPow.hPow (β := ℕ) S.Y 3 + 1) -
        (↑S.u₄ : 𝓞 K) * (HPow.hPow (β := ℕ) S.Z 3 + 1))

Tactic:
ring
-- 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
inl : ∀ (h : S.u₄ = 1), HPow.hPow (β := ℕ) S.u₄ 2 = 1
inr : ∀ (h : S.u₄ = -1), HPow.hPow (β := ℕ) S.u₄ 2 = 1
⊢ HPow.hPow (β := ℕ) S.u₄ 2 = 1

Tactic:
rcases S.u₄_eq_one_or_neg_one with h | h

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.u₄_eq_one_or_neg_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
h : S.u₄ = 1
⊢ HPow.hPow (β := ℕ) S.u₄ 2 = 1

Tactic:
simp [h]
-- 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
h : S.u₄ = -1
⊢ HPow.hPow (β := ℕ) S.u₄ 2 = 1

Tactic:
simp [h]
-- 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
⊢ HPow.hPow (β := ℕ) S.Y 3 + HPow.hPow (β := ℕ) ((↑S.u₄ : 𝓞 K) * S.Z) 3 =
    HPow.hPow (β := ℕ) S.Y 3 + HPow.hPow (β := ℕ) (↑S.u₄ : 𝓞 K) 2 * (↑S.u₄ : 𝓞 K) * HPow.hPow (β := ℕ) S.Z 3

Tactic:
ring
-- 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
⊢ HPow.hPow (β := ℕ) S.Y 3 + HPow.hPow (β := ℕ) (↑S.u₄ : 𝓞 K) 2 * (↑S.u₄ : 𝓞 K) * HPow.hPow (β := ℕ) S.Z 3 =
    HPow.hPow (β := ℕ) S.Y 3 + (↑S.u₄ : 𝓞 K) * HPow.hPow (β := ℕ) S.Z 3

Tactic:
simp [← Units.val_pow_eq_pow_val, S.u₄_sq]

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.u₄_sq, Units.val_pow_eq_pow_val
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h : λ ^ (S.multiplicity - 1) * S.X = 0
⊢ S.X = 0

Tactic:
simpa [hζ.zeta_sub_one_prime'.ne_zero] using h

Premises used: Prime.ne_zero, IsPrimitiveRoot.zeta_sub_one_prime'
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
⊢ λ ∣ λ ^ (S.multiplicity - 1) * S.X

Tactic:
dvd_mul_of_dvd_left (dvd_pow_self _ (fun h ↦ ?_)) _

Premises used: dvd_mul_of_dvd_left, dvd_pow_self
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
refine : ∀ (h : S.multiplicity - 1 = 0), False
⊢ λ ∣ λ ^ (S.multiplicity - 1) * S.X

Tactic:
refine dvd_mul_of_dvd_left (dvd_pow_self _ (fun h ↦ ?_)) _

Premises used: dvd_mul_of_dvd_left, dvd_pow_self
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h : S.multiplicity - 1 = 0
⊢ LE.le (α := ℕ) 1 2

Tactic:
simp
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h : S.multiplicity - 1 = 0
⊢ S.multiplicity = 1

Tactic:
rw [Nat.sub_eq_iff_eq_add (le_trans (by simp) S.two_le_multiplicity), zero_add] at h

Premises used: Nat.sub_eq_iff_eq_add, _private.0.FermatLastTheoremForThreeGen.Solution.two_le_multiplicity, zero_add, le_trans
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h : S.multiplicity = 1
⊢ False

Tactic:
simpa [h] using S.two_le_multiplicity

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.two_le_multiplicity
-- 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
⊢ λ ^ (S.multiplicity - 1) ∣ S.Solution'_descent.c

Tactic:
simp [Solution'_descent]

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.Solution'_descent
-- 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
refine : ∀ (h : λ ^ (S.multiplicity - 1 + 1) ∣ S.Solution'_descent.c), λ ∣ S.X
⊢ S.Solution'_descent.multiplicity = S.multiplicity - 1

Tactic:
refine multiplicity_eq_of_dvd_of_not_dvd
    (by simp [Solution'_descent]) (fun h ↦ S.lambda_not_dvd_X ?_)

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.lambda_not_dvd_X, multiplicity_eq_of_dvd_of_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
h : λ ^ (S.multiplicity - 1 + 1) ∣ S.Solution'_descent.c
obtain : ∀ (k : 𝓞 K) (hk : λ ^ (S.multiplicity - 1) * S.X = λ ^ (S.multiplicity - 1 + 1) * k), λ ∣ S.X
⊢ λ ∣ S.X

Tactic:
obtain ⟨k, hk : λ ^ (S.multiplicity - 1) * S.X = λ ^ (S.multiplicity - 1 + 1) * k⟩ := h

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.multiplicity, _private.0.FermatLastTheoremForThreeGen.Solution.X, HSub.hSub, HAdd.hAdd, 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
k : 𝓞 K
hk : λ ^ (S.multiplicity - 1) * S.X = λ ^ (S.multiplicity - 1 + 1) * k
⊢ λ ^ (S.multiplicity - 1) * S.X = λ ^ (S.multiplicity - 1) * (λ * k)

Tactic:
rw [pow_succ, mul_assoc] at hk

Premises used: pow_succ, mul_assoc
-- 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
k : 𝓞 K
hk : λ ^ (S.multiplicity - 1) * S.X = λ ^ (S.multiplicity - 1) * (λ * k)
⊢ S.X = λ * k

Tactic:
simp only [mul_eq_mul_left_iff, pow_eq_zero_iff', hζ.zeta_sub_one_prime'.ne_zero, ne_eq,
    false_and, or_false] at hk

Premises used: mul_eq_mul_left_iff, false_and, pow_eq_zero_iff', ne_eq, Prime.ne_zero, or_false, IsPrimitiveRoot.zeta_sub_one_prime'
-- 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
k : 𝓞 K
hk : S.X = λ * k
⊢ λ ∣ S.X

Tactic:
simp [hk]
-- 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
rw : S.multiplicity.pred < S.multiplicity
⊢ S.Solution'_descent.multiplicity < S.multiplicity

Tactic:
rw [Solution'_descent_multiplicity S, Nat.sub_one]

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.Solution'_descent_multiplicity, Nat.sub_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
this : 2 ≤ S.multiplicity
⊢ S.multiplicity ≠ 0

Tactic:
lia
-- 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
⊢ S.multiplicity.pred < S.multiplicity

Tactic:
exact Nat.pred_lt <| by have := S.two_le_multiplicity; lia

Premises used: Nat.pred_lt
-- 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 :
  ∀ (S' : Solution hζ) (hS' : S'.multiplicity = S.Solution'_descent.multiplicity),
    ∃ (S₁ : Solution hζ), S₁.multiplicity < S.multiplicity
⊢ ∃ (S₁ : Solution hζ), S₁.multiplicity < S.multiplicity

Tactic:
obtain ⟨S', hS'⟩ := exists_Solution_of_Solution' (Solution'_descent S)

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.Solution'_descent, _private.0.FermatLastTheoremForThreeGen.exists_Solution_of_Solution'