-- Mathlib/NumberTheory/FLT/Three.lean
/-- We have that `λ ^ (3*S.multiplicity-2)` divides `S.a + S.b`. -/
private lemma lambda_pow_dvd_a_add_b : λ ^ (3 * S.multiplicity - 2) ∣ S.a + 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
h :
  λ ^ (3 * S.multiplicity) ∣
    (S.a + S.b) * (λ * FermatLastTheoremForThreeGen.Solution.y S) * (λ * FermatLastTheoremForThreeGen.Solution.z S)
⊢ λ ^ (3 * S.multiplicity - 2) ∣ FermatLastTheoremForThreeGen.Solution.z S * (S.a + S.b)

Tactic:
apply hζ.zeta_sub_one_prime'.pow_dvd_of_dvd_mul_left _ S.lambda_not_dvd_y

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h :
  λ ^ (3 * S.multiplicity) ∣
    (S.a + S.b) * (λ * FermatLastTheoremForThreeGen.Solution.y S) * (λ * FermatLastTheoremForThreeGen.Solution.z S)
⊢ λ ^ (3 * S.multiplicity - 2) ∣
    FermatLastTheoremForThreeGen.Solution.y S * (FermatLastTheoremForThreeGen.Solution.z S * (S.a + 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
h :
  λ ^ (3 * S.multiplicity) ∣
    (S.a + S.b) * (λ * FermatLastTheoremForThreeGen.Solution.y S) * (λ * FermatLastTheoremForThreeGen.Solution.z S)
this : 2 ≤ S.multiplicity
⊢ λ ^ (3 * S.multiplicity - 2) ∣
    FermatLastTheoremForThreeGen.Solution.y S * (FermatLastTheoremForThreeGen.Solution.z S * (S.a + S.b))

Tactic:
rw [show 3 * multiplicity S = 3 * multiplicity S - 2 + 1 + 1 by omega, pow_succ, pow_succ,
  show (S.a + S.b) * (λ * y S) * (λ * z S) = (S.a + S.b) * y S * z S * λ * λ by ring] at h

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h :
  λ ^ (3 * S.multiplicity - 2) * λ * λ ∣
    (S.a + S.b) * FermatLastTheoremForThreeGen.Solution.y S * FermatLastTheoremForThreeGen.Solution.z S * λ * λ
this : 2 ≤ S.multiplicity
⊢ λ ^ (3 * S.multiplicity - 2) ∣
    FermatLastTheoremForThreeGen.Solution.y S * (FermatLastTheoremForThreeGen.Solution.z S * (S.a + 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
⊢ λ ^ (3 * S.multiplicity - 2) ∣ S.a + S.b

Tactic:
have h : λ ^ S.multiplicity ∣ S.c := pow_multiplicity_dvd _ _

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ S.multiplicity ∣ S.c
⊢ λ ^ (3 * S.multiplicity - 2) ∣ S.a + 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
h : (λ ^ S.multiplicity) ^ 3 ∣ ↑S.u * S.c ^ 3
⊢ λ ^ (3 * S.multiplicity - 2) ∣ S.a + S.b

Tactic:
rw [← S.H, a_cube_add_b_cube_eq_mul, ← pow_mul, mul_comm, y_spec, z_spec] at h

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h :
  λ ^ (3 * S.multiplicity) ∣
    (S.a + S.b) * (λ * FermatLastTheoremForThreeGen.Solution.y S) * (λ * FermatLastTheoremForThreeGen.Solution.z S)
⊢ λ ^ (3 * S.multiplicity - 2) ∣ S.a + 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
h : λ ^ S.multiplicity ∣ S.c
⊢ λ ^ (3 * S.multiplicity - 2) ∣ S.a + S.b

Tactic:
replace h : (λ ^ multiplicity S) ^ 3 ∣ S.u * S.c ^ 3 := by simp [h]

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : (λ ^ S.multiplicity) ^ 3 ∣ ↑S.u * S.c ^ 3
⊢ λ ^ (3 * S.multiplicity - 2) ∣ S.a + 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
h :
  λ ^ (3 * S.multiplicity) ∣
    (S.a + S.b) * (λ * FermatLastTheoremForThreeGen.Solution.y S) * (λ * FermatLastTheoremForThreeGen.Solution.z S)
⊢ λ ^ (3 * S.multiplicity - 2) ∣
    FermatLastTheoremForThreeGen.Solution.y S * (FermatLastTheoremForThreeGen.Solution.z S * (S.a + S.b))

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
h :
  λ ^ (3 * S.multiplicity) ∣
    (S.a + S.b) * (λ * FermatLastTheoremForThreeGen.Solution.y S) * (λ * FermatLastTheoremForThreeGen.Solution.z S)
this : 2 ≤ S.multiplicity
⊢ λ ^ (3 * S.multiplicity - 2) ∣
    FermatLastTheoremForThreeGen.Solution.y S * (FermatLastTheoremForThreeGen.Solution.z S * (S.a + 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
this : 2 ≤ S.multiplicity
h :
  λ ^ (3 * S.multiplicity - 2) ∣
    (S.a + S.b) * FermatLastTheoremForThreeGen.Solution.y S * FermatLastTheoremForThreeGen.Solution.z S
⊢ (S.a + S.b) * FermatLastTheoremForThreeGen.Solution.y S * FermatLastTheoremForThreeGen.Solution.z S =
    FermatLastTheoremForThreeGen.Solution.y S * (FermatLastTheoremForThreeGen.Solution.z S * (S.a + 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
h :
  λ ^ (3 * S.multiplicity) ∣
    (S.a + S.b) * (λ * FermatLastTheoremForThreeGen.Solution.y S) * (λ * FermatLastTheoremForThreeGen.Solution.z S)
this : 2 ≤ S.multiplicity
⊢ 3 * S.multiplicity = 3 * S.multiplicity - 2 + 1 + 1

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
h :
  λ ^ (3 * S.multiplicity - 2) * λ * λ ∣
    (S.a + S.b) * (λ * FermatLastTheoremForThreeGen.Solution.y S) * (λ * FermatLastTheoremForThreeGen.Solution.z S)
this : 2 ≤ S.multiplicity
⊢ (S.a + S.b) * (λ * FermatLastTheoremForThreeGen.Solution.y S) * (λ * FermatLastTheoremForThreeGen.Solution.z S) =
    (S.a + S.b) * 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
this : 2 ≤ S.multiplicity
h :
  λ ^ (3 * S.multiplicity - 2) ∣
    (S.a + S.b) * FermatLastTheoremForThreeGen.Solution.y S * FermatLastTheoremForThreeGen.Solution.z S
⊢ λ ^ (3 * S.multiplicity - 2) ∣
    FermatLastTheoremForThreeGen.Solution.y S * (FermatLastTheoremForThreeGen.Solution.z S * (S.a + S.b))

Tactic:
rwa [show (S.a + S.b) * y S * z S = y S * (z S * (S.a + S.b)) by ring] at h

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
h :
  λ ^ (3 * S.multiplicity) ∣
    (S.a + S.b) * (λ * FermatLastTheoremForThreeGen.Solution.y S) * (λ * FermatLastTheoremForThreeGen.Solution.z S)
⊢ λ ^ (3 * S.multiplicity - 2) ∣ S.a + S.b

Tactic:
apply hζ.zeta_sub_one_prime'.pow_dvd_of_dvd_mul_left _ S.lambda_not_dvd_z

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