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

Tactic:
congrm ?_ + ?_ + ?_

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
⊢ ↑(η ^ 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)

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) * λ * ↑η

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

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.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

Tactic:
rw [← formula1 S]

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) * ↑η) =
    FermatLastTheoremForThreeGen.Solution.X S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₁ S) *
          λ ^ (3 * S.multiplicity - 2) +
        FermatLastTheoremForThreeGen.Solution.Y S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * λ * ↑η +
      FermatLastTheoremForThreeGen.Solution.Z S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₃ S) * λ * ↑η ^ 2

Proof state:
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.Z S ^ 3 =
    ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
      (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3

Tactic:
rw [u₅_def, neg_mul, neg_mul, Units.val_neg, neg_mul, eq_neg_iff_add_eq_zero, add_assoc,
  add_comm (S.u₄ * S.Z ^ 3), ← add_assoc, add_comm (S.Y ^ 3)]

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.Y S ^ 3 +
      ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3 =
    0

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 =
    0

Tactic:
apply mul_right_cancel₀ <| mul_ne_zero
  (mul_ne_zero hζ.zeta_sub_one_prime'.ne_zero S.u₂.isUnit.ne_zero) (Units.isUnit η).ne_zero

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.Y S ^ 3 +
        ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3) *
      (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η) =
    0 * (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η)

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

Tactic:
simp [hζ.toInteger_cube_eq_one, ← pow_succ, this]

Result:
no goals