-- 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
⊢ FermatLastTheoremForThreeGen.Solution.x S * FermatLastTheoremForThreeGen.Solution.y S *
      FermatLastTheoremForThreeGen.Solution.z S =
    ↑S.u * FermatLastTheoremForThreeGen.Solution.w S ^ 3

Tactic:
suffices hh : λ ^ (3 * S.multiplicity - 2) * S.x * λ * S.y * λ * S.z =
    S.u * λ ^ (3 * S.multiplicity) * S.w ^ 3 by
  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
  have := S.two_le_multiplicity
  rw [mul_comm _ (λ ^ (3 * multiplicity S)), ← pow_succ, ← pow_succ,
    show 3 * multiplicity S - 2 + 1 + 1 = 3 * multiplicity S by omega, mul_assoc, mul_assoc,
    mul_assoc] at hh
  simp only [mul_eq_mul_left_iff, pow_eq_zero_iff', hζ.zeta_sub_one_prime'.ne_zero, ne_eq,
    mul_eq_zero, OfNat.ofNat_ne_zero, false_or, false_and, or_false] at hh
  convert hh using 1
  ring

Result:
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

Proof state:
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)

Tactic:
rw [mul_comm 3, pow_mul, ← mul_pow, ← w_spec, ← S.H, a_cube_add_b_cube_eq_mul]

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.a + S.b) * (S.a + ↑η * S.b) * (S.a + ↑η ^ 2 * S.b)

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

Tactic:
rw [mul_comm _ (λ ^ (3 * multiplicity S)), ← pow_succ, ← pow_succ,
  show 3 * multiplicity S - 2 + 1 + 1 = 3 * multiplicity S by omega, mul_assoc, mul_assoc,
  mul_assoc] 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) *
      (FermatLastTheoremForThreeGen.Solution.x S *
        (FermatLastTheoremForThreeGen.Solution.y S * FermatLastTheoremForThreeGen.Solution.z S)) =
    λ ^ (3 * S.multiplicity) * (↑S.u * FermatLastTheoremForThreeGen.Solution.w S ^ 3)
this : 2 ≤ S.multiplicity
⊢ 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
⊢ (S.a + S.b) * ((S.a + ↑η * S.b) * (S.a + ↑η ^ 2 * S.b)) = (S.a + S.b) * (S.a + ↑η * S.b) * (S.a + ↑η ^ 2 * S.b)

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

Tactic:
simp only [mul_eq_mul_left_iff, pow_eq_zero_iff', hζ.zeta_sub_one_prime'.ne_zero, ne_eq,
  mul_eq_zero, OfNat.ofNat_ne_zero, false_or, false_and, or_false] at hh

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

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

Tactic:
omega

Result:
no goals