-- Mathlib/NumberTheory/FLT/Three.lean
private lemma formula2 :
    S.Y ^ 3 + S.u₄ * S.Z ^ 3 = S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3

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 ≤ S.multiplicity
⊢ (S.multiplicity - 1) * 3 + 1 = 3 * S.multiplicity - 2

Tactic:
omega

Result:
no goals

Proof state:
case refine_3
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3 *
      (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η) =
    FermatLastTheoremForThreeGen.Solution.Z S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₃ S) * λ * ↑η ^ 2

Tactic:
field_simp [u₄_def]

Result:
case refine_3
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ FermatLastTheoremForThreeGen.Solution.Z S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₃ S) * λ * hζ.toInteger ^ 2 *
      ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) =
    hζ.toInteger * ↑(FermatLastTheoremForThreeGen.Solution.u₃ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3 *
      (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * hζ.toInteger)

Proof state:
case refine_2
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ FermatLastTheoremForThreeGen.Solution.Y S ^ 3 * (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η) =
    FermatLastTheoremForThreeGen.Solution.Y S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * λ * ↑η

Tactic:
ring

Result:
no goals

Proof state:
case refine_1
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ ↑(η ^ 2 * FermatLastTheoremForThreeGen.Solution.u₁ S * (FermatLastTheoremForThreeGen.Solution.u₂ S)⁻¹) *
        (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 *
      (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η) =
    FermatLastTheoremForThreeGen.Solution.X S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₁ S) *
      λ ^ (3 * S.multiplicity - 2)

Tactic:
have : (S.multiplicity-1)*3+1 = 3*S.multiplicity-2 := by have := S.two_le_multiplicity; omega

Result:
case refine_1
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : (S.multiplicity - 1) * 3 + 1 = 3 * S.multiplicity - 2
⊢ ↑(η ^ 2 * FermatLastTheoremForThreeGen.Solution.u₁ S * (FermatLastTheoremForThreeGen.Solution.u₂ S)⁻¹) *
        (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 *
      (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η) =
    FermatLastTheoremForThreeGen.Solution.X S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₁ S) *
      λ ^ (3 * S.multiplicity - 2)

Proof state:
case refine_3
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ FermatLastTheoremForThreeGen.Solution.Z S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₃ S) * λ * hζ.toInteger ^ 2 *
      ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) =
    hζ.toInteger * ↑(FermatLastTheoremForThreeGen.Solution.u₃ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3 *
      (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * hζ.toInteger)

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 : (S.multiplicity - 1) * 3 + 1 = 3 * S.multiplicity - 2
⊢ ↑(η ^ 2 * FermatLastTheoremForThreeGen.Solution.u₁ S * (FermatLastTheoremForThreeGen.Solution.u₂ S)⁻¹) *
        (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 *
      (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η) =
    FermatLastTheoremForThreeGen.Solution.X S ^ 3 *
          (↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S)⁻¹) *
        (↑η ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₁ S)) *
      (λ ^ ((S.multiplicity - 1) * 3) * λ)

Tactic:
push_cast

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : (S.multiplicity - 1) * 3 + 1 = 3 * S.multiplicity - 2
⊢ ↑η ^ 2 * ↑(FermatLastTheoremForThreeGen.Solution.u₁ S) * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S)⁻¹ *
        (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 *
      (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η) =
    FermatLastTheoremForThreeGen.Solution.X S ^ 3 *
          (↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S)⁻¹) *
        (↑η ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₁ S)) *
      (λ ^ ((S.multiplicity - 1) * 3) * λ)

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : (S.multiplicity - 1) * 3 + 1 = 3 * S.multiplicity - 2
⊢ ↑η ^ 2 * ↑(FermatLastTheoremForThreeGen.Solution.u₁ S) * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S)⁻¹ *
        (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 *
      (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η) =
    FermatLastTheoremForThreeGen.Solution.X S ^ 3 *
          (↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S)⁻¹) *
        (↑η ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₁ S)) *
      (λ ^ ((S.multiplicity - 1) * 3) * λ)

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
⊢ (S.multiplicity - 1) * 3 + 1 = 3 * S.multiplicity - 2

Tactic:
have := S.two_le_multiplicity

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : 2 ≤ S.multiplicity
⊢ (S.multiplicity - 1) * 3 + 1 = 3 * S.multiplicity - 2

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ (↑(η ^ 2 * FermatLastTheoremForThreeGen.Solution.u₁ S * (FermatLastTheoremForThreeGen.Solution.u₂ S)⁻¹) *
            (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 +
          FermatLastTheoremForThreeGen.Solution.Y S ^ 3 +
        ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3) *
      (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η) =
    0 * (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η)

Tactic:
simp only [zero_mul, add_mul]

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ ↑(η ^ 2 * FermatLastTheoremForThreeGen.Solution.u₁ S * (FermatLastTheoremForThreeGen.Solution.u₂ S)⁻¹) *
            (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 *
          (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η) +
        FermatLastTheoremForThreeGen.Solution.Y S ^ 3 * (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η) +
      ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3 *
        (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η) =
    0