-- Mathlib/NumberTheory/FLT/Three.lean
/-- Given `S' : Solution'`, we have that `λ ^ 2` divides one amongst `S'.a + S'.b`,
`S'.a + η * S'.b` and `S'.a + η ^ 2 * S'.b`. -/
lemma lambda_sq_dvd_or_dvd_or_dvd :
    λ ^ 2 ∣ S'.a + S'.b ∨ λ ^ 2 ∣ S'.a + η * S'.b ∨ λ ^ 2 ∣ 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
inst✝ : DecidableRel fun a b => a ∣ b
h1 : emultiplicity λ (S'.a + S'.b) < ↑2
h2 : emultiplicity λ (S'.a + ↑η * S'.b) < ↑2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
⊢ FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)

Tactic:
refine finiteMultiplicity_iff_emultiplicity_ne_top.2 (fun ht ↦ ?_)

Result:
K : Type u_1
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {3} ℚ K
inst✝ : DecidableRel fun a b => a ∣ b
h1 : emultiplicity λ (S'.a + S'.b) < ↑2
h2 : emultiplicity λ (S'.a + ↑η * S'.b) < ↑2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
ht : emultiplicity λ (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
inst✝ : DecidableRel fun a b => a ∣ b
h1 : emultiplicity λ (S'.a + S'.b) < ↑2
h2 : emultiplicity λ (S'.a + ↑η * S'.b) < ↑2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
ht : emultiplicity λ (S'.a + hζ.toInteger * S'.b) = ⊤
⊢ False

Tactic:
simp [ht] at h2

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
inst✝ : DecidableRel fun a b => a ∣ b
h1 : emultiplicity λ (S'.a + S'.b) < ↑2
h2 : emultiplicity λ (S'.a + ↑η * S'.b) < ↑2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
ht : emultiplicity λ (S'.a + S'.b) = ⊤
⊢ False

Tactic:
simp [ht] at h1

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
inst✝ : DecidableRel fun a b => a ∣ b
h1 : emultiplicity λ (S'.a + S'.b) < ↑2
h2 : emultiplicity λ (S'.a + ↑η * S'.b) < ↑2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
ht : emultiplicity λ (S'.a + hζ.toInteger ^ 2 * S'.b) = ⊤
⊢ False

Tactic:
simp [ht] at h3

Result:
no goals

Proof state:
case intro.intro
K : Type u_1
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {3} ℚ K
inst✝ : DecidableRel fun a b => a ∣ b
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + ↑η * S'.b) < 2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
⊢ False

Tactic:
rw [h3'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h3

Result:
case intro.intro
K : Type u_1
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {3} ℚ K
inst✝ : DecidableRel fun a b => a ∣ b
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + ↑η * S'.b) < 2
h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < 2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (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
inst✝ : DecidableRel fun a b => a ∣ b
h1 : emultiplicity λ (S'.a + S'.b) < ↑2
h2 : emultiplicity λ (S'.a + ↑η * S'.b) < ↑2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
ht : emultiplicity λ (S'.a + ↑η * S'.b) = ⊤
⊢ False

Tactic:
rw [coe_eta] at ht

Result:
K : Type u_1
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {3} ℚ K
inst✝ : DecidableRel fun a b => a ∣ b
h1 : emultiplicity λ (S'.a + S'.b) < ↑2
h2 : emultiplicity λ (S'.a + ↑η * S'.b) < ↑2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
ht : emultiplicity λ (S'.a + hζ.toInteger * 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
inst✝ : DecidableRel fun a b => a ∣ b
h1 : emultiplicity λ (S'.a + S'.b) < ↑2
h2 : emultiplicity λ (S'.a + ↑η * S'.b) < ↑2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
ht : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) = ⊤
⊢ False

Tactic:
rw [coe_eta] at ht

Result:
K : Type u_1
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {3} ℚ K
inst✝ : DecidableRel fun a b => a ∣ b
h1 : emultiplicity λ (S'.a + S'.b) < ↑2
h2 : emultiplicity λ (S'.a + ↑η * S'.b) < ↑2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
ht : emultiplicity λ (S'.a + hζ.toInteger ^ 2 * S'.b) = ⊤
⊢ False

Proof state:
case intro.intro
K : Type u_1
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {3} ℚ K
inst✝ : DecidableRel fun a b => a ∣ b
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + ↑η * S'.b) < 2
h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < 2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
this : (λ ^ 2) ^ 3 ∣ ↑S'.u * S'.c ^ 3
⊢ False

Tactic:
rw [← pow_mul, ← S'.H, a_cube_add_b_cube_eq_mul, pow_dvd_iff_le_emultiplicity,
  emultiplicity_mul hζ.zeta_sub_one_prime', emultiplicity_mul hζ.zeta_sub_one_prime',
    h1'.emultiplicity_eq_multiplicity, h2'.emultiplicity_eq_multiplicity,
    h3'.emultiplicity_eq_multiplicity, ← Nat.cast_add, ← Nat.cast_add, Nat.cast_le] at this

Result:
case intro.intro
K : Type u_1
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {3} ℚ K
inst✝ : DecidableRel fun a b => a ∣ b
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + ↑η * S'.b) < 2
h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < 2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
this : 2 * 3 ≤ multiplicity λ (S'.a + S'.b) + multiplicity λ (S'.a + ↑η * S'.b) + multiplicity λ (S'.a + ↑η ^ 2 * S'.b)
⊢ False

Proof state:
case intro.intro
K : Type u_1
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {3} ℚ K
inst✝ : DecidableRel fun a b => a ∣ b
h1 : ¬λ ^ 2 ∣ S'.a + S'.b
h2 : ¬λ ^ 2 ∣ S'.a + ↑η * S'.b
h3 : ¬λ ^ 2 ∣ S'.a + ↑η ^ 2 * S'.b
⊢ False

Tactic:
rw [← emultiplicity_lt_iff_not_dvd] at h1 h2 h3

Result:
case intro.intro
K : Type u_1
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {3} ℚ K
inst✝ : DecidableRel fun a b => a ∣ b
h1 : emultiplicity λ (S'.a + S'.b) < ↑2
h2 : emultiplicity λ (S'.a + ↑η * S'.b) < ↑2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
⊢ False