-- Mathlib/NumberTheory/FLT/Three.lean
private lemma x_mul_y_mul_z_eq_u_mul_w_cube : S.x * S.y * S.z = S.u * S.w ^ 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
hh :
  FermatLastTheoremForThreeGen.Solution.x S *
      (FermatLastTheoremForThreeGen.Solution.y S * FermatLastTheoremForThreeGen.Solution.z S) =
    ↑S.u * FermatLastTheoremForThreeGen.Solution.w S ^ 3
⊢ FermatLastTheoremForThreeGen.Solution.x S * FermatLastTheoremForThreeGen.Solution.y S *
      FermatLastTheoremForThreeGen.Solution.z S =
    ↑S.u * FermatLastTheoremForThreeGen.Solution.w S ^ 3

Tactic:
convert hh using 1

Result:
case h.e'_2
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
hh :
  FermatLastTheoremForThreeGen.Solution.x S *
      (FermatLastTheoremForThreeGen.Solution.y S * FermatLastTheoremForThreeGen.Solution.z S) =
    ↑S.u * FermatLastTheoremForThreeGen.Solution.w S ^ 3
⊢ FermatLastTheoremForThreeGen.Solution.x S * FermatLastTheoremForThreeGen.Solution.y S *
      FermatLastTheoremForThreeGen.Solution.z S =
    FermatLastTheoremForThreeGen.Solution.x S *
      (FermatLastTheoremForThreeGen.Solution.y S * FermatLastTheoremForThreeGen.Solution.z S)

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ λ ^ (3 * S.multiplicity - 2) * FermatLastTheoremForThreeGen.Solution.x S * λ *
          FermatLastTheoremForThreeGen.Solution.y S *
        λ *
      FermatLastTheoremForThreeGen.Solution.z S =
    ↑S.u * λ ^ (3 * S.multiplicity) * FermatLastTheoremForThreeGen.Solution.w S ^ 3

Tactic:
simp only [← x_spec, mul_assoc, ← y_spec, ← z_spec]

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ (S.a + S.b) * ((S.a + ↑η * S.b) * (S.a + ↑η ^ 2 * S.b)) =
    ↑S.u * (λ ^ (3 * S.multiplicity) * FermatLastTheoremForThreeGen.Solution.w S ^ 3)

Proof state:
case h.e'_2
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
hh :
  FermatLastTheoremForThreeGen.Solution.x S *
      (FermatLastTheoremForThreeGen.Solution.y S * FermatLastTheoremForThreeGen.Solution.z S) =
    ↑S.u * FermatLastTheoremForThreeGen.Solution.w S ^ 3
⊢ FermatLastTheoremForThreeGen.Solution.x S * FermatLastTheoremForThreeGen.Solution.y S *
      FermatLastTheoremForThreeGen.Solution.z S =
    FermatLastTheoremForThreeGen.Solution.x S *
      (FermatLastTheoremForThreeGen.Solution.y S * FermatLastTheoremForThreeGen.Solution.z S)

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
hh :
  λ ^ (3 * S.multiplicity - 2) * FermatLastTheoremForThreeGen.Solution.x S * λ *
          FermatLastTheoremForThreeGen.Solution.y S *
        λ *
      FermatLastTheoremForThreeGen.Solution.z S =
    ↑S.u * λ ^ (3 * S.multiplicity) * FermatLastTheoremForThreeGen.Solution.w S ^ 3
⊢ FermatLastTheoremForThreeGen.Solution.x S * FermatLastTheoremForThreeGen.Solution.y S *
      FermatLastTheoremForThreeGen.Solution.z S =
    ↑S.u * FermatLastTheoremForThreeGen.Solution.w S ^ 3

Tactic:
rw [show λ ^ (3 * multiplicity S - 2) * x S * λ * y S * λ * z S =
  λ ^ (3 * multiplicity S - 2) * λ * λ * x S * y S * z S by ring] at hh

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hh :
  λ ^ (3 * S.multiplicity - 2) * λ * λ * FermatLastTheoremForThreeGen.Solution.x S *
        FermatLastTheoremForThreeGen.Solution.y S *
      FermatLastTheoremForThreeGen.Solution.z S =
    ↑S.u * λ ^ (3 * S.multiplicity) * FermatLastTheoremForThreeGen.Solution.w S ^ 3
⊢ FermatLastTheoremForThreeGen.Solution.x S * FermatLastTheoremForThreeGen.Solution.y S *
      FermatLastTheoremForThreeGen.Solution.z S =
    ↑S.u * FermatLastTheoremForThreeGen.Solution.w S ^ 3

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hh :
  λ ^ (3 * S.multiplicity - 2) * FermatLastTheoremForThreeGen.Solution.x S * λ *
          FermatLastTheoremForThreeGen.Solution.y S *
        λ *
      FermatLastTheoremForThreeGen.Solution.z S =
    ↑S.u * λ ^ (3 * S.multiplicity) * FermatLastTheoremForThreeGen.Solution.w S ^ 3
⊢ λ ^ (3 * S.multiplicity - 2) * FermatLastTheoremForThreeGen.Solution.x S * λ *
          FermatLastTheoremForThreeGen.Solution.y S *
        λ *
      FermatLastTheoremForThreeGen.Solution.z S =
    λ ^ (3 * S.multiplicity - 2) * λ * λ * FermatLastTheoremForThreeGen.Solution.x S *
        FermatLastTheoremForThreeGen.Solution.y S *
      FermatLastTheoremForThreeGen.Solution.z S

Tactic:
ring

Result:
no goals