-- Mathlib/NumberTheory/FLT/Three.lean
/-- Given `S' : Solution'`, we have that `λ ^ 2` divides `S'.c`. -/
lemma lambda_sq_dvd_c : λ ^ 2 ∣ S'.c

Proof state:
case h.e'_3.h.e'_5.h.e'_6
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hm : FiniteMultiplicity λ S'.c
this : 2 ≤ multiplicity λ S'.c
x : 𝓞 K
hx : S'.c = λ ^ multiplicity λ S'.c * x
⊢ 2 + (multiplicity λ S'.c - 2) = multiplicity λ S'.c

Tactic:
simp [this]

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
hm : FiniteMultiplicity λ S'.c
this : 2 ≤ multiplicity λ S'.c
⊢ λ ^ 2 ∣ S'.c

Tactic:
obtain ⟨x, hx⟩ := pow_multiplicity_dvd (hζ.toInteger - 1) S'.c

Result:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hm : FiniteMultiplicity λ S'.c
this : 2 ≤ multiplicity λ S'.c
x : 𝓞 K
hx : S'.c = λ ^ multiplicity λ S'.c * x
⊢ λ ^ 2 ∣ S'.c

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hm : FiniteMultiplicity λ S'.c
⊢ 2 ≤ multiplicity λ S'.c

Tactic:
have := lambda_pow_four_dvd_c_cube S'

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hm : FiniteMultiplicity λ S'.c
this : λ ^ 4 ∣ S'.c ^ 3
⊢ 2 ≤ multiplicity λ S'.c

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ λ ^ 2 ∣ S'.c

Tactic:
have hm := S'.multiplicity_lambda_c_finite

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hm : FiniteMultiplicity λ S'.c
⊢ λ ^ 2 ∣ S'.c

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hm : FiniteMultiplicity λ S'.c
this : ↑4 ≤ ↑3 * ↑(multiplicity λ S'.c)
⊢ 2 ≤ multiplicity λ S'.c

Tactic:
norm_cast at this

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hm : FiniteMultiplicity λ S'.c
this : 4 ≤ 3 * multiplicity λ S'.c
⊢ 2 ≤ multiplicity λ S'.c

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

Tactic:
rw [pow_dvd_iff_le_emultiplicity, emultiplicity_pow hζ.zeta_sub_one_prime',
  hm.emultiplicity_eq_multiplicity] at this

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hm : FiniteMultiplicity λ S'.c
this : ↑4 ≤ ↑3 * ↑(multiplicity λ S'.c)
⊢ 2 ≤ multiplicity λ S'.c

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hm : FiniteMultiplicity λ S'.c
this : 4 ≤ 3 * multiplicity λ S'.c
⊢ 2 ≤ multiplicity λ S'.c

Tactic:
omega

Result:
no goals

Proof state:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hm : FiniteMultiplicity λ S'.c
this : 2 ≤ multiplicity λ S'.c
x : 𝓞 K
hx : S'.c = λ ^ multiplicity λ S'.c * x
⊢ S'.c = λ ^ (2 + (multiplicity λ S'.c - 2)) * x

Tactic:
convert hx using 3

Result:
case h.e'_3.h.e'_5.h.e'_6
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hm : FiniteMultiplicity λ S'.c
this : 2 ≤ multiplicity λ S'.c
x : 𝓞 K
hx : S'.c = λ ^ multiplicity λ S'.c * x
⊢ 2 + (multiplicity λ S'.c - 2) = multiplicity λ S'.c

Proof state:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hm : FiniteMultiplicity λ S'.c
this : 2 ≤ multiplicity λ S'.c
x : 𝓞 K
hx : S'.c = λ ^ multiplicity λ S'.c * x
⊢ S'.c = λ ^ 2 * (λ ^ (multiplicity λ S'.c - 2) * x)

Tactic:
rw [← mul_assoc, ← pow_add]

Result:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hm : FiniteMultiplicity λ S'.c
this : 2 ≤ multiplicity λ S'.c
x : 𝓞 K
hx : S'.c = λ ^ multiplicity λ S'.c * x
⊢ S'.c = λ ^ (2 + (multiplicity λ S'.c - 2)) * x

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hm : FiniteMultiplicity λ S'.c
⊢ λ ^ 2 ∣ S'.c

Tactic:
suffices 2 ≤ multiplicity (hζ.toInteger - 1) S'.c by
  obtain ⟨x, hx⟩ := pow_multiplicity_dvd (hζ.toInteger - 1) S'.c
  refine ⟨λ ^ (multiplicity (hζ.toInteger - 1) S'.c - 2) * x, ?_⟩
  rw [← mul_assoc, ← pow_add]
  convert hx using 3
  simp [this]

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hm : FiniteMultiplicity λ S'.c
⊢ 2 ≤ multiplicity λ S'.c

Proof state:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hm : FiniteMultiplicity λ S'.c
this : 2 ≤ multiplicity λ S'.c
x : 𝓞 K
hx : S'.c = λ ^ multiplicity λ S'.c * x
⊢ λ ^ 2 ∣ S'.c

Tactic:
refine ⟨λ ^ (multiplicity (hζ.toInteger - 1) S'.c - 2) * x, ?_⟩

Result:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hm : FiniteMultiplicity λ S'.c
this : 2 ≤ multiplicity λ S'.c
x : 𝓞 K
hx : S'.c = λ ^ multiplicity λ S'.c * x
⊢ S'.c = λ ^ 2 * (λ ^ (multiplicity λ S'.c - 2) * x)