-- Mathlib/NumberTheory/FLT/Three.lean
private lemma lambda_sq_div_u₅_mul : λ ^ 2 ∣ S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3

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

Tactic:
calc _ = λ^(3*(S.multiplicity-1))*S.u₅*S.X^3 := by ring
_ = λ^2*λ^(3*S.multiplicity-5)*S.u₅*S.X^3 := by rw [this, pow_add]
_ = λ^2*(λ^(3*S.multiplicity-5)*S.u₅*S.X^3) := by 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 ≤ S.multiplicity
⊢ 3 * (S.multiplicity - 1) = 2 + (3 * S.multiplicity - 5)

Tactic:
omega

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

Tactic:
rw [this, pow_add]

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 : 3 * (S.multiplicity - 1) = 2 + (3 * S.multiplicity - 5)
⊢ ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
      (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 =
    λ ^ (3 * (S.multiplicity - 1)) * ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
      FermatLastTheoremForThreeGen.Solution.X S ^ 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
⊢ λ ^ 2 ∣
    ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
      (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3

Tactic:
use λ^(3*S.multiplicity-5)*S.u₅*(S.X^3)

Result:
case h
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) *
      (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 =
    λ ^ 2 *
      (λ ^ (3 * S.multiplicity - 5) * ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
        FermatLastTheoremForThreeGen.Solution.X S ^ 3)

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

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

Result:
case h
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : 3 * (S.multiplicity - 1) = 2 + (3 * S.multiplicity - 5)
⊢ ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
      (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 =
    λ ^ 2 *
      (λ ^ (3 * S.multiplicity - 5) * ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
        FermatLastTheoremForThreeGen.Solution.X 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
this : 3 * (S.multiplicity - 1) = 2 + (3 * S.multiplicity - 5)
⊢ λ ^ 2 * λ ^ (3 * S.multiplicity - 5) * ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
      FermatLastTheoremForThreeGen.Solution.X S ^ 3 =
    λ ^ 2 *
      (λ ^ (3 * S.multiplicity - 5) * ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
        FermatLastTheoremForThreeGen.Solution.X S ^ 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
⊢ 3 * (S.multiplicity - 1) = 2 + (3 * S.multiplicity - 5)

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