-- Mathlib/NumberTheory/FLT/Three.lean
private lemma lambda_not_dvd_x : ¬ λ ∣ S.x := fun h ↦ by
  replace h := mul_dvd_mul_left (λ ^ (3 * S.multiplicity - 2)) h
  rw [mul_comm, ← x_spec] at h
  replace h :=
    mul_dvd_mul (mul_dvd_mul h S.lambda_dvd_a_add_eta_mul_b) S.lambda_dvd_a_add_eta_sq_mul_b
  simp only [← a_cube_add_b_cube_eq_mul, S.H, w_spec, Units.isUnit, IsUnit.dvd_mul_left] at h
  rw [← pow_succ', mul_comm, ← mul_assoc, ← pow_succ'] at h
  have := S.two_le_multiplicity
  rw [show 3 * multiplicity S - 2 + 1 + 1 = 3 * multiplicity S by omega, mul_pow, ← pow_mul,
    mul_comm _ 3, mul_dvd_mul_iff_left _] at h
  · exact lambda_not_dvd_w _ <| hζ.zeta_sub_one_prime'.dvd_of_dvd_pow h
  · simp [hζ.zeta_sub_one_prime'.ne_zero]

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 + 1 + 1) * λ ∣ (λ ^ S.multiplicity * FermatLastTheoremForThreeGen.Solution.w S) ^ 3
⊢ False

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 - 2 + 1 + 1) * λ ∣ (λ ^ S.multiplicity * FermatLastTheoremForThreeGen.Solution.w S) ^ 3
this : 2 ≤ S.multiplicity
⊢ False

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) * λ ∣ λ ^ (3 * S.multiplicity - 2) * FermatLastTheoremForThreeGen.Solution.x S
⊢ False

Tactic:
rw [mul_comm, ← x_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 - 2) ∣ S.a + S.b
⊢ False

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) * λ ∣ λ ^ (3 * S.multiplicity) * FermatLastTheoremForThreeGen.Solution.w S ^ 3
this : 2 ≤ S.multiplicity
⊢ λ ^ (3 * S.multiplicity) ≠ 0

Tactic:
simp [hζ.zeta_sub_one_prime'.ne_zero]

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

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 : λ ∣ FermatLastTheoremForThreeGen.Solution.x S
⊢ False

Tactic:
replace h := mul_dvd_mul_left (λ ^ (3 * S.multiplicity - 2)) 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) * λ ∣ λ ^ (3 * S.multiplicity - 2) * FermatLastTheoremForThreeGen.Solution.x S
⊢ False

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ FermatLastTheoremForThreeGen.Solution.w S ^ 3
this : 2 ≤ S.multiplicity
⊢ False

Tactic:
exact lambda_not_dvd_w _ <| hζ.zeta_sub_one_prime'.dvd_of_dvd_pow 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 - 2) ∣ S.a + S.b
⊢ False

Tactic:
replace h :=
  mul_dvd_mul (mul_dvd_mul h S.lambda_dvd_a_add_eta_mul_b) S.lambda_dvd_a_add_eta_sq_mul_b

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

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.multiplicity * FermatLastTheoremForThreeGen.Solution.w S) ^ 3
⊢ False

Tactic:
rw [← pow_succ', mul_comm, ← mul_assoc, ← pow_succ'] 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 + 1 + 1) * λ ∣ (λ ^ S.multiplicity * FermatLastTheoremForThreeGen.Solution.w S) ^ 3
⊢ False

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 + 1 + 1) * λ ∣ (λ ^ S.multiplicity * FermatLastTheoremForThreeGen.Solution.w S) ^ 3
this : 2 ≤ S.multiplicity
⊢ False

Tactic:
rw [show 3 * multiplicity S - 2 + 1 + 1 = 3 * multiplicity S by omega, mul_pow, ← pow_mul,
  mul_comm _ 3, mul_dvd_mul_iff_left _] 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 : λ ∣ FermatLastTheoremForThreeGen.Solution.w S ^ 3
this : 2 ≤ S.multiplicity
⊢ False

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) * λ ∣ λ ^ (3 * S.multiplicity) * FermatLastTheoremForThreeGen.Solution.w S ^ 3
this : 2 ≤ S.multiplicity
⊢ λ ^ (3 * S.multiplicity) ≠ 0

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

Tactic:
simp only [← a_cube_add_b_cube_eq_mul, S.H, w_spec, Units.isUnit, IsUnit.dvd_mul_left] 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.multiplicity * FermatLastTheoremForThreeGen.Solution.w S) ^ 3
⊢ False