-- Mathlib/NumberTheory/FLT/Three.lean
private lemma u₄_eq_one_or_neg_one : S.u₄ = 1 ∨ S.u₄ = -1

Proof state:
case hcong.intro.inl.inl.intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX :
  ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
      (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 =
    λ ^ 2 * X
Y : 𝓞 K
hY : FermatLastTheoremForThreeGen.Solution.Y S ^ 3 - 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : FermatLastTheoremForThreeGen.Solution.Z S ^ 3 - 1 = λ ^ 2 * Z
⊢ ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) - ↑(-1) =
    FermatLastTheoremForThreeGen.Solution.Y S ^ 3 +
          ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3 -
        (FermatLastTheoremForThreeGen.Solution.Y S ^ 3 - 1) -
      ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * (FermatLastTheoremForThreeGen.Solution.Z S ^ 3 - 1)

Tactic:
ring

Result:
no goals

Proof state:
case hcong
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
h :
  λ ^ 2 ∣
    ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
      (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3
⊢ ∃ n, λ ^ 2 ∣ ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) - ↑n

Tactic:
rcases h with ⟨X, hX⟩

Result:
case hcong.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX :
  ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
      (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 =
    λ ^ 2 * X
⊢ ∃ n, λ ^ 2 ∣ ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) - ↑n

Proof state:
case hcong.intro.inr.inl.intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX :
  ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
      (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 =
    λ ^ 2 * X
Y : 𝓞 K
hY : FermatLastTheoremForThreeGen.Solution.Y S ^ 3 + 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : FermatLastTheoremForThreeGen.Solution.Z S ^ 3 - 1 = λ ^ 2 * Z
⊢ ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) - ↑1 =
    FermatLastTheoremForThreeGen.Solution.Y S ^ 3 +
          ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3 -
        (FermatLastTheoremForThreeGen.Solution.Y S ^ 3 + 1) -
      ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * (FermatLastTheoremForThreeGen.Solution.Z S ^ 3 - 1)

Tactic:
ring

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX :
  ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
      (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 =
    λ ^ 2 * X
Y : 𝓞 K
hY : FermatLastTheoremForThreeGen.Solution.Y S ^ 3 - 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : FermatLastTheoremForThreeGen.Solution.Z S ^ 3 - 1 = λ ^ 2 * Z
⊢ λ ^ 2 * (X - Y - ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * Z) =
    λ ^ 2 * X - λ ^ 2 * Y - ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * (λ ^ 2 * Z)

Tactic:
ring

Result:
no goals

Proof state:
case hcong.intro.inl.inr.intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX :
  ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
      (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 =
    λ ^ 2 * X
Y : 𝓞 K
hY : FermatLastTheoremForThreeGen.Solution.Y S ^ 3 - 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : FermatLastTheoremForThreeGen.Solution.Z S ^ 3 + 1 = λ ^ 2 * Z
⊢ ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) - ↑1 =
    -(FermatLastTheoremForThreeGen.Solution.Y S ^ 3 +
            ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3 -
          (FermatLastTheoremForThreeGen.Solution.Y S ^ 3 - 1) -
        ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * (FermatLastTheoremForThreeGen.Solution.Z S ^ 3 + 1))

Tactic:
ring

Result:
no goals

Proof state:
case hcong.intro.inr.inr.intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX :
  ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
      (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 =
    λ ^ 2 * X
Y : 𝓞 K
hY : FermatLastTheoremForThreeGen.Solution.Y S ^ 3 + 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : FermatLastTheoremForThreeGen.Solution.Z S ^ 3 + 1 = λ ^ 2 * Z
⊢ ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) - ↑(-1) =
    -(FermatLastTheoremForThreeGen.Solution.Y S ^ 3 +
            ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3 -
          (FermatLastTheoremForThreeGen.Solution.Y S ^ 3 + 1) -
        ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * (FermatLastTheoremForThreeGen.Solution.Z S ^ 3 + 1))

Tactic:
ring

Result:
no goals

Proof state:
case hcong.intro.inr.inr.intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX :
  ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
      (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 =
    λ ^ 2 * X
Y : 𝓞 K
hY : FermatLastTheoremForThreeGen.Solution.Y S ^ 3 + 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : FermatLastTheoremForThreeGen.Solution.Z S ^ 3 + 1 = λ ^ 2 * Z
⊢ ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) - ↑(-1) =
    λ ^ 2 * (-X + Y + ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * Z)

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

Result:
case hcong.intro.inr.inr.intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX :
  ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
      (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 =
    λ ^ 2 * X
Y : 𝓞 K
hY : FermatLastTheoremForThreeGen.Solution.Y S ^ 3 + 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : FermatLastTheoremForThreeGen.Solution.Z S ^ 3 + 1 = λ ^ 2 * Z
⊢ ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) - ↑(-1) =
    -(FermatLastTheoremForThreeGen.Solution.Y S ^ 3 +
            ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3 -
          (FermatLastTheoremForThreeGen.Solution.Y S ^ 3 + 1) -
        ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * (FermatLastTheoremForThreeGen.Solution.Z S ^ 3 + 1))

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ λ ^ 4 = λ ^ 2 * λ ^ 2

Tactic:
ring

Result:
no goals