awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 + 1 + (HPow.hPow (β := ℕ) S'.b 3 + 1) -
      (HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3) =
    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) *
      (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
calc₁ :
  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)
calc₂ :
  HPow.hPow (β := ℕ) S'.a 3 + 1 + (HPow.hPow (β := ℕ) S'.b 3 + 1) -
      (HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3) =
    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) =
    2

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

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.a, _private.0.FermatLastTheoremForThreeGen.Solution'.u, 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
inl :
  ∀ (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'.c 3
inr :
  ∀ (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'.c 3
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.c 3

Tactic:
rcases a_cube_b_cube_congr_one_or_neg_one S' with
    ⟨⟨x, hx⟩, ⟨y, hy⟩⟩ | ⟨⟨x, hx⟩, ⟨y, hy⟩⟩

Premises used: _private.0.FermatLastTheoremForThreeGen.a_cube_b_cube_congr_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
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'.c 3

Tactic:
⟨S'.u⁻¹ * (x + y), ?_⟩

Premises used: Units.val, _private.0.FermatLastTheoremForThreeGen.Solution'.u, HMul.hMul, Inv.inv, HAdd.hAdd, 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
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 (β := ℕ) S'.c 3 = HPow.hPow (β := ℕ) λ 4 * ((↑S'.u⁻¹ : 𝓞 K) * (x + y))
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.c 3

Tactic:
refine ⟨S'.u⁻¹ * (x + y), ?_⟩
-- 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
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 * ((↑S'.u⁻¹ : 𝓞 K) * (x + y)) = HPow.hPow (β := ℕ) S'.c 3
⊢ HPow.hPow (β := ℕ) S'.c 3 = HPow.hPow (β := ℕ) λ 4 * ((↑S'.u⁻¹ : 𝓞 K) * (x + y))

Tactic:
symm
-- 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
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 * ((↑S'.u⁻¹ : 𝓞 K) * (x + y)) =
    (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) λ 4 * x + HPow.hPow (β := ℕ) λ 4 * y)

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
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
rw :
  (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) S'.a 3 - 1 + (HPow.hPow (β := ℕ) S'.b 3 + 1)) =
    (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3)
⊢ (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) λ 4 * x + HPow.hPow (β := ℕ) λ 4 * y) =
    (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3)

Tactic:
rw [← hx, ← 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
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
⊢ (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) S'.a 3 - 1 + (HPow.hPow (β := ℕ) S'.b 3 + 1)) =
    (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 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
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
rw rw₁ :
  (↑S'.u⁻¹ : 𝓞 K) * ((↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3) =
    (↑S'.u⁻¹ : 𝓞 K) * ((↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3)
⊢ (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3) =
    (↑S'.u⁻¹ : 𝓞 K) * ((↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3)

Tactic:
rw [S'.H]

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.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
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
⊢ (↑S'.u⁻¹ : 𝓞 K) * ((↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3) = HPow.hPow (β := ℕ) S'.c 3

Tactic:
simp
-- 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
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
calc :
  HPow.hPow (β := ℕ) λ 4 * ((↑S'.u⁻¹ : 𝓞 K) * (x + y)) =
    (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) λ 4 * x + HPow.hPow (β := ℕ) λ 4 * y)
calc₁ :
  (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) λ 4 * x + HPow.hPow (β := ℕ) λ 4 * y) =
    (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3)
calc₂ :
  (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3) =
    (↑S'.u⁻¹ : 𝓞 K) * ((↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3)
calc₃ : (↑S'.u⁻¹ : 𝓞 K) * ((↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3) = HPow.hPow (β := ℕ) S'.c 3
⊢ HPow.hPow (β := ℕ) λ 4 * ((↑S'.u⁻¹ : 𝓞 K) * (x + y)) = HPow.hPow (β := ℕ) S'.c 3

Tactic:
calc _ = S'.u⁻¹ * (λ ^ 4 * x + λ ^ 4 * y) := by ring
    _ = S'.u⁻¹ * (S'.a ^ 3 + S'.b ^ 3) := by rw [← hx, ← hy]; ring
    _ = S'.u⁻¹ * (S'.u * S'.c ^ 3) := by rw [S'.H]
    _ = S'.c ^ 3 := by simp

Premises used: Units.val, _private.0.FermatLastTheoremForThreeGen.Solution'.a, _private.0.FermatLastTheoremForThreeGen.Solution'.u, HMul.hMul, HPow.hPow, HAdd.hAdd, _private.0.FermatLastTheoremForThreeGen.Solution'.b, OfNat.ofNat, _private.0.FermatLastTheoremForThreeGen.Solution'.c
-- 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
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'.c 3

Tactic:
⟨S'.u⁻¹ * (x + y), ?_⟩

Premises used: Units.val, _private.0.FermatLastTheoremForThreeGen.Solution'.u, HMul.hMul, Inv.inv, HAdd.hAdd, 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
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 (β := ℕ) S'.c 3 = HPow.hPow (β := ℕ) λ 4 * ((↑S'.u⁻¹ : 𝓞 K) * (x + y))
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.c 3

Tactic:
refine ⟨S'.u⁻¹ * (x + y), ?_⟩
-- 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
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 * ((↑S'.u⁻¹ : 𝓞 K) * (x + y)) = HPow.hPow (β := ℕ) S'.c 3
⊢ HPow.hPow (β := ℕ) S'.c 3 = HPow.hPow (β := ℕ) λ 4 * ((↑S'.u⁻¹ : 𝓞 K) * (x + y))

Tactic:
symm
-- 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
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 * ((↑S'.u⁻¹ : 𝓞 K) * (x + y)) =
    (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) λ 4 * x + HPow.hPow (β := ℕ) λ 4 * y)

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
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
rw :
  (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) S'.a 3 + 1 + (HPow.hPow (β := ℕ) S'.b 3 - 1)) =
    (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3)
⊢ (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) λ 4 * x + HPow.hPow (β := ℕ) λ 4 * y) =
    (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3)

Tactic:
rw [← hx, ← 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
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
⊢ (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) S'.a 3 + 1 + (HPow.hPow (β := ℕ) S'.b 3 - 1)) =
    (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 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
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
rw rw₁ :
  (↑S'.u⁻¹ : 𝓞 K) * ((↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3) =
    (↑S'.u⁻¹ : 𝓞 K) * ((↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3)
⊢ (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3) =
    (↑S'.u⁻¹ : 𝓞 K) * ((↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3)

Tactic:
rw [S'.H]

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.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
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
⊢ (↑S'.u⁻¹ : 𝓞 K) * ((↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3) = HPow.hPow (β := ℕ) S'.c 3

Tactic:
simp
-- 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
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
calc :
  HPow.hPow (β := ℕ) λ 4 * ((↑S'.u⁻¹ : 𝓞 K) * (x + y)) =
    (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) λ 4 * x + HPow.hPow (β := ℕ) λ 4 * y)
calc₁ :
  (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) λ 4 * x + HPow.hPow (β := ℕ) λ 4 * y) =
    (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3)
calc₂ :
  (↑S'.u⁻¹ : 𝓞 K) * (HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3) =
    (↑S'.u⁻¹ : 𝓞 K) * ((↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3)
calc₃ : (↑S'.u⁻¹ : 𝓞 K) * ((↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3) = HPow.hPow (β := ℕ) S'.c 3
⊢ HPow.hPow (β := ℕ) λ 4 * ((↑S'.u⁻¹ : 𝓞 K) * (x + y)) = HPow.hPow (β := ℕ) S'.c 3

Tactic:
calc _ = S'.u⁻¹ * (λ ^ 4 * x + λ ^ 4 * y) := by ring
    _ = S'.u⁻¹ * (S'.a ^ 3 + S'.b ^ 3) := by rw [← hx, ← hy]; ring
    _ = S'.u⁻¹ * (S'.u * S'.c ^ 3) := by rw [S'.H]
    _ = S'.c ^ 3 := by simp

Premises used: Units.val, _private.0.FermatLastTheoremForThreeGen.Solution'.a, _private.0.FermatLastTheoremForThreeGen.Solution'.u, HMul.hMul, HPow.hPow, HAdd.hAdd, _private.0.FermatLastTheoremForThreeGen.Solution'.b, OfNat.ofNat, _private.0.FermatLastTheoremForThreeGen.Solution'.c
-- 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
⊢ FiniteMultiplicity λ S'.c

Tactic:
have hm := S'.multiplicity_lambda_c_finite
-- 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
hm : FiniteMultiplicity λ S'.c
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.c 3

Tactic:
have := lambda_pow_four_dvd_c_cube S'
-- 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
hm : FiniteMultiplicity λ S'.c
this : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S'.c 3
⊢ (↑4 : ℕ∞) ≤ HMul.hMul (α := ℕ∞) (↑3 : ℕ∞) (↑(multiplicity λ S'.c) : ℕ∞)

Tactic:
rw [pow_dvd_iff_le_emultiplicity, emultiplicity_pow hζ.zeta_sub_one_prime',
    hm.emultiplicity_eq_multiplicity] at this

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, pow_dvd_iff_le_emultiplicity, emultiplicity_pow, 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
hm : FiniteMultiplicity λ S'.c
this : (↑4 : ℕ∞) ≤ HMul.hMul (α := ℕ∞) (↑3 : ℕ∞) (↑(multiplicity λ S'.c) : ℕ∞)
⊢ 4 ≤ 3 * multiplicity λ S'.c

Tactic:
norm_cast at this
-- 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
hm : FiniteMultiplicity λ S'.c
this : 4 ≤ 3 * multiplicity λ S'.c
⊢ 2 ≤ multiplicity λ S'.c

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
hm : FiniteMultiplicity λ S'.c
this : 4 ≤ 3 * multiplicity λ S'.c
⊢ HPow.hPow (β := ℕ) λ 2 ∣ S'.c

Tactic:
exact (FiniteMultiplicity.pow_dvd_iff_le_multiplicity hm).mpr (by lia)

Premises used: Iff.mpr, FiniteMultiplicity.pow_dvd_iff_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
⊢ 2 ≤ S'.multiplicity

Tactic:
simpa [Solution'.multiplicity] using
    S'.multiplicity_lambda_c_finite.le_multiplicity_of_pow_dvd (lambda_sq_dvd_c S')

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.multiplicity, _private.0.FermatLastTheoremForThreeGen.lambda_sq_dvd_c, FiniteMultiplicity.le_multiplicity_of_pow_dvd, _private.0.FermatLastTheoremForThreeGen.Solution'.multiplicity_lambda_c_finite
-- 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
⊢ 2 ≤ S.multiplicity

Tactic:
S.toSolution'.two_le_multiplicity

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.multiplicity, _private.0.FermatLastTheoremForThreeGen.Solution'.two_le_multiplicity, _private.0.FermatLastTheoremForThreeGen.Solution.toSolution'
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
symm :
  (S'.a + S'.b) * (S'.a + (↑η : 𝓞 K) * S'.b) * (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) =
    HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3
⊢ HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3 =
    (S'.a + S'.b) * (S'.a + (↑η : 𝓞 K) * S'.b) * (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)

Tactic:
symm
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
⊢ (S'.a + S'.b) * (S'.a + (↑η : 𝓞 K) * S'.b) * (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) =
    HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.a 2 * S'.b * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + (↑η : 𝓞 K) + 1) +
        S'.a * HPow.hPow (β := ℕ) S'.b 2 *
          (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + (↑η : 𝓞 K) + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 3) +
      HPow.hPow (β := ℕ) (↑η : 𝓞 K) 3 * HPow.hPow (β := ℕ) S'.b 3

Tactic:
ring
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
⊢ HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.a 2 * S'.b * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + (↑η : 𝓞 K) + 1) +
        S'.a * HPow.hPow (β := ℕ) S'.b 2 *
          (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + (↑η : 𝓞 K) + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 3) +
      HPow.hPow (β := ℕ) (↑η : 𝓞 K) 3 * HPow.hPow (β := ℕ) S'.b 3 =
    HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.a 2 * S'.b * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + (↑η : 𝓞 K) + 1) +
        S'.a * HPow.hPow (β := ℕ) S'.b 2 * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + (↑η : 𝓞 K) + 1) +
      HPow.hPow (β := ℕ) S'.b 3

Tactic:
simp [hζ.toInteger_cube_eq_one]

Premises used: IsPrimitiveRoot.toInteger_cube_eq_one
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
rw :
  HPow.hPow (β := ℕ) S'.a 3 +
          HPow.hPow (β := ℕ) S'.a 2 * S'.b * (-(↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - 1 + (↑η : 𝓞 K) + 1) +
        S'.a * HPow.hPow (β := ℕ) S'.b 2 * (-(↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - 1 + (↑η : 𝓞 K) + 1) +
      HPow.hPow (β := ℕ) S'.b 3 =
    HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3
⊢ HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.a 2 * S'.b * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + (↑η : 𝓞 K) + 1) +
        S'.a * HPow.hPow (β := ℕ) S'.b 2 * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + (↑η : 𝓞 K) + 1) +
      HPow.hPow (β := ℕ) S'.b 3 =
    HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3

Tactic:
rw [eta_sq]

Premises used: IsCyclotomicExtension.Rat.Three.eta_sq
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
⊢ HPow.hPow (β := ℕ) S'.a 3 +
          HPow.hPow (β := ℕ) S'.a 2 * S'.b * (-(↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - 1 + (↑η : 𝓞 K) + 1) +
        S'.a * HPow.hPow (β := ℕ) S'.b 2 * (-(↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - 1 + (↑η : 𝓞 K) + 1) +
      HPow.hPow (β := ℕ) S'.b 3 =
    HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3

Tactic:
ring
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
calc :
  (S'.a + S'.b) * (S'.a + (↑η : 𝓞 K) * S'.b) * (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) =
    HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.a 2 * S'.b * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + (↑η : 𝓞 K) + 1) +
        S'.a * HPow.hPow (β := ℕ) S'.b 2 *
          (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + (↑η : 𝓞 K) + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 3) +
      HPow.hPow (β := ℕ) (↑η : 𝓞 K) 3 * HPow.hPow (β := ℕ) S'.b 3
calc₁ :
  HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.a 2 * S'.b * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + (↑η : 𝓞 K) + 1) +
        S'.a * HPow.hPow (β := ℕ) S'.b 2 *
          (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + (↑η : 𝓞 K) + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 3) +
      HPow.hPow (β := ℕ) (↑η : 𝓞 K) 3 * HPow.hPow (β := ℕ) S'.b 3 =
    HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.a 2 * S'.b * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + (↑η : 𝓞 K) + 1) +
        S'.a * HPow.hPow (β := ℕ) S'.b 2 * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + (↑η : 𝓞 K) + 1) +
      HPow.hPow (β := ℕ) S'.b 3
calc₂ :
  HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.a 2 * S'.b * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + (↑η : 𝓞 K) + 1) +
        S'.a * HPow.hPow (β := ℕ) S'.b 2 * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + (↑η : 𝓞 K) + 1) +
      HPow.hPow (β := ℕ) S'.b 3 =
    HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3
⊢ (S'.a + S'.b) * (S'.a + (↑η : 𝓞 K) * S'.b) * (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) =
    HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3

Tactic:
calc _ = S'.a^3+S'.a^2*S'.b*(η^2+η+1)+S'.a*S'.b^2*(η^2+η+η^3)+η^3*S'.b^3 := by ring
  _ = S'.a^3+S'.a^2*S'.b*(η^2+η+1)+S'.a*S'.b^2*(η^2+η+1)+S'.b^3 := by
    simp [hζ.toInteger_cube_eq_one]
  _ = S'.a ^ 3 + S'.b ^ 3 := by rw [eta_sq]; ring

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.a, _private.0.FermatLastTheoremForThreeGen.Solution'.b
-- 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
by_contra! :
  ∀ (h1 : ¬HPow.hPow (β := ℕ) λ 2 ∣ S'.a + S'.b) (h2 : ¬HPow.hPow (β := ℕ) λ 2 ∣ S'.a + (↑η : 𝓞 K) * S'.b)
    (h3 : ¬HPow.hPow (β := ℕ) λ 2 ∣ S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b), False
⊢ HPow.hPow (β := ℕ) λ 2 ∣ S'.a + S'.b ∨
    HPow.hPow (β := ℕ) λ 2 ∣ S'.a + (↑η : 𝓞 K) * S'.b ∨
      HPow.hPow (β := ℕ) λ 2 ∣ S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b

Tactic:
by_contra! ⟨h1, h2, h3⟩