-- 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:
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
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
⊢ False

Tactic:
have h3' : FiniteMultiplicity (hζ.toInteger - 1) (S'.a + η ^ 2 * S'.b) := by
  refine finiteMultiplicity_iff_emultiplicity_ne_top.2 (fun ht ↦ ?_)
  rw [coe_eta] at ht
  simp [ht] 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 : 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)
h3' : FiniteMultiplicity λ (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 : 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)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
⊢ False

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

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

Tactic:
rcases h with ⟨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 : ¬λ ^ 2 ∣ S'.a + S'.b
h2 : ¬λ ^ 2 ∣ S'.a + ↑η * S'.b
h3 : ¬λ ^ 2 ∣ 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 : emultiplicity λ (S'.a + S'.b) < ↑2
h2 : emultiplicity λ (S'.a + ↑η * S'.b) < ↑2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
⊢ False

Tactic:
have h1' : FiniteMultiplicity (hζ.toInteger - 1) (S'.a + S'.b) :=
  finiteMultiplicity_iff_emultiplicity_ne_top.2 (fun ht ↦ by simp [ht] at h1)

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
h1' : FiniteMultiplicity λ (S'.a + 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 ≤ multiplicity λ (S'.a + S'.b) + multiplicity λ (S'.a + ↑η * S'.b) + multiplicity λ (S'.a + ↑η ^ 2 * S'.b)
⊢ False

Tactic:
omega

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 : 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)
⊢ False

Tactic:
have h2' : FiniteMultiplicity (hζ.toInteger - 1) (S'.a + η * S'.b) := by
  refine finiteMultiplicity_iff_emultiplicity_ne_top.2 (fun ht ↦ ?_)
  rw [coe_eta] at ht
  simp [ht] at h2

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

Tactic:
by_contra! h

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
h : ¬λ ^ 2 ∣ S'.a + S'.b ∧ ¬λ ^ 2 ∣ S'.a + ↑η * S'.b ∧ ¬λ ^ 2 ∣ S'.a + ↑η ^ 2 * S'.b
⊢ False