-- Mathlib/NumberTheory/FLT/Three.lean
/-- Given `(S : Solution)`, we have that `λ ^ 2` does not divide `S.a + η ^ 2 * S.b`. -/
lemma lambda_sq_not_dvd_a_add_eta_sq_mul_b : ¬ λ ^ 2 ∣ (S.a + η ^ 2 * S.b)

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
k : 𝓞 K
hk : S.a + ↑η ^ 2 * S.b = λ ^ 2 * k
k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
⊢ False

Tactic:
refine S.hb ⟨(k - k') * (-η), ?_⟩

Result:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k : 𝓞 K
hk : S.a + ↑η ^ 2 * S.b = λ ^ 2 * k
k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
⊢ S.b = λ * ((k - k') * -↑η)

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
k k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
hk : S.b = λ * k * -↑η + ↑η * λ * k'
⊢ λ * k * -↑η + ↑η * λ * k' = λ * ((k - k') * -↑η)

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

Tactic:
intro ⟨k, hk⟩

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k : 𝓞 K
hk : S.a + ↑η ^ 2 * S.b = λ ^ 2 * k
⊢ False

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k : 𝓞 K
hk : S.a + ↑η ^ 2 * S.b = λ ^ 2 * k
⊢ False

Tactic:
rcases S.hab with ⟨k', hk'⟩

Result:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k : 𝓞 K
hk : S.a + ↑η ^ 2 * S.b = λ ^ 2 * k
k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
⊢ False

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
hk : (S.b * (↑η + 1) + λ * k') * -↑η = λ * k * -↑η
⊢ (S.b * (↑η + 1) + λ * k') * -↑η = -S.b * (↑η ^ 2 + ↑η + 1 - 1) - ↑η * λ * k'

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
k k' : 𝓞 K
hk : λ ^ 2 * k' - S.b + ↑η ^ 2 * S.b = λ ^ 2 * k
hk' : S.a + S.b = λ ^ 2 * k'
⊢ λ ^ 2 * k' - S.b + hζ.toInteger ^ 2 * S.b = λ * (S.b * (hζ.toInteger + 1) + λ * k')

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
k : 𝓞 K
hk : S.a + ↑η ^ 2 * S.b = λ ^ 2 * k
k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
⊢ S.a + ↑η ^ 2 * S.b = S.a + S.b - S.b + ↑η ^ 2 * S.b

Tactic:
ring

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
k k' : 𝓞 K
hk : λ * (S.b * (↑η + 1) + λ * k') = λ * (λ * k)
hk' : S.a + S.b = λ ^ 2 * k'
⊢ S.b = λ * ((k - k') * -↑η)

Tactic:
simp only [mul_eq_mul_left_iff, hζ.zeta_sub_one_prime'.ne_zero, or_false] at hk

Result:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
hk : S.b * (↑η + 1) + λ * k' = λ * k
⊢ S.b = λ * ((k - k') * -↑η)

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
k k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
hk : (S.b * (↑η + 1) + λ * k') * -↑η = λ * k * -↑η
⊢ S.b = λ * ((k - k') * -↑η)

Tactic:
rw [show (S.b * (η + 1) + λ * k') * -η = (- S.b) * (η ^ 2 + η + 1 - 1) - η * λ * k' by ring,
  eta_sq, show -S.b * (-↑η - 1 + ↑η + 1 - 1) = S.b by ring, sub_eq_iff_eq_add] at hk

Result:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
hk : S.b = λ * k * -↑η + ↑η * λ * k'
⊢ S.b = λ * ((k - k') * -↑η)

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
hk : -S.b * (-↑η - 1 + ↑η + 1 - 1) - ↑η * λ * k' = λ * k * -↑η
⊢ -S.b * (-↑η - 1 + ↑η + 1 - 1) = 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
k k' : 𝓞 K
hk : λ ^ 2 * k' - S.b + ↑η ^ 2 * S.b = λ ^ 2 * k
hk' : S.a + S.b = λ ^ 2 * k'
⊢ λ ^ 2 * k' - S.b + ↑η ^ 2 * S.b = λ * (S.b * (↑η + 1) + λ * k')

Tactic:
rw [coe_eta]

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k k' : 𝓞 K
hk : λ ^ 2 * k' - S.b + ↑η ^ 2 * S.b = λ ^ 2 * k
hk' : S.a + S.b = λ ^ 2 * k'
⊢ λ ^ 2 * k' - S.b + hζ.toInteger ^ 2 * S.b = λ * (S.b * (hζ.toInteger + 1) + λ * k')

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
k : 𝓞 K
hk : S.a + ↑η ^ 2 * S.b = λ ^ 2 * k
k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
⊢ S.b = λ * ((k - k') * -↑η)

Tactic:
rw [show S.a + η ^ 2 * S.b = S.a + S.b - S.b + η ^ 2 * S.b by ring, hk',
  show λ ^ 2 * k' - S.b + η ^ 2 * S.b = λ * (S.b * (η +1) + λ * k') by rw [coe_eta]; ring,
  pow_two, mul_assoc] at hk

Result:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k k' : 𝓞 K
hk : λ * (S.b * (↑η + 1) + λ * k') = λ * (λ * k)
hk' : S.a + S.b = λ ^ 2 * k'
⊢ S.b = λ * ((k - k') * -↑η)

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
k k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
hk : S.b = λ * k * -↑η + ↑η * λ * k'
⊢ S.b = λ * ((k - k') * -↑η)

Tactic:
rw [hk]

Result:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
hk : S.b = λ * k * -↑η + ↑η * λ * k'
⊢ λ * k * -↑η + ↑η * λ * k' = λ * ((k - k') * -↑η)