-- Mathlib/NumberTheory/FLT/Three.lean
/-- Given `S' : Solution'`, then `S'.a` and `S'.b` are both congruent to `1` modulo `λ ^ 4` or are
both congruent to `-1`. -/
lemma a_cube_b_cube_congr_one_or_neg_one :
    λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1

Proof state:
case intro.inr.intro.inr.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = λ ^ 4 * y
⊢ λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1

Tactic:
exfalso

Result:
case intro.inr.intro.inr.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = λ ^ 4 * y
⊢ False

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (↑3 ^ 1)
⊢ (hζ.toInteger - 1) * (↑S'.u * (hζ✝.toInteger - 1) ^ 2 * z ^ 3 - (hζ✝.toInteger - 1) ^ 3 * (x + y)) =
    ↑S'.u * ((hζ✝.toInteger - 1) * z) ^ 3 - (hζ✝.toInteger - 1) ^ 4 * x - (hζ✝.toInteger - 1) ^ 4 * y

Tactic:
ring

Result:
no goals

Proof state:
case intro.inl.intro.inl.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = λ ^ 4 * y
⊢ λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1

Tactic:
exfalso

Result:
case intro.inl.intro.inl.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = λ ^ 4 * y
⊢ False

Proof state:
case intro.inr.intro.inr.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (↑3 ^ 1)
⊢ 2 = (hζ.toInteger - 1) * ((hζ✝.toInteger - 1) ^ 3 * (x + y) - ↑S'.u * (hζ✝.toInteger - 1) ^ 2 * z ^ 3)

Tactic:
symm

Result:
case intro.inr.intro.inr.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (↑3 ^ 1)
⊢ (hζ.toInteger - 1) * ((hζ✝.toInteger - 1) ^ 3 * (x + y) - ↑S'.u * (hζ✝.toInteger - 1) ^ 2 * z ^ 3) = 2

Proof state:
case intro.inr.intro.inr.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (↑3 ^ 1)
⊢ (hζ.toInteger - 1) * ((hζ✝.toInteger - 1) ^ 3 * (x + y) - ↑S'.u * (hζ✝.toInteger - 1) ^ 2 * z ^ 3) = 2

Tactic:
calc _ =  λ ^ 4 * x + λ ^ 4 * y - S'.u * (λ * z) ^ 3 := by ring
_ = (S'.a ^ 3 + 1) + (S'.b ^ 3 + 1) - (S'.a ^ 3 + S'.b ^ 3) := by rw [← hx, ← hy, ← hz, ← S'.H]
_ = 2 := by 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
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (↑3 ^ 1)
⊢ 3 ≠ 2

Tactic:
decide

Result:
no goals

Proof state:
case intro.inl.intro.inr.intro.h
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = λ ^ 4 * y
⊢ λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1

Tactic:
exact ⟨⟨x, hx⟩, ⟨y, hy⟩⟩

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
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = λ ^ 4 * y
⊢ IsPrimitiveRoot ζ (↑3 ^ 1)

Tactic:
rwa [pow_one]

Result:
no goals

Proof state:
case intro.inl.intro.inl.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (↑3 ^ 1)
⊢ (hζ.toInteger - 1) * (↑S'.u * (hζ✝.toInteger - 1) ^ 2 * z ^ 3 - (hζ✝.toInteger - 1) ^ 3 * (x + y)) = 2

Tactic:
calc _ = S'.u * (λ * z) ^ 3 - λ ^ 4 * x - λ ^ 4 * y := by ring
_ = (S'.a ^ 3 + S'.b ^ 3) - (S'.a ^ 3 - 1) - (S'.b ^ 3 - 1) := by rw [← hx, ← hy, ← hz, ← S'.H]
_ = 2 := by ring

Result:
no goals

Proof state:
case intro.inl.intro.inl.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (↑3 ^ 1)
⊢ 2 = (hζ.toInteger - 1) * (↑S'.u * (hζ✝.toInteger - 1) ^ 2 * z ^ 3 - (hζ✝.toInteger - 1) ^ 3 * (x + y))

Tactic:
symm

Result:
case intro.inl.intro.inl.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (↑3 ^ 1)
⊢ (hζ.toInteger - 1) * (↑S'.u * (hζ✝.toInteger - 1) ^ 2 * z ^ 3 - (hζ✝.toInteger - 1) ^ 3 * (x + y)) = 2

Proof state:
case intro.inl.intro.inr.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = λ ^ 4 * y
⊢ λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1

Tactic:
left

Result:
case intro.inl.intro.inr.intro.h
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = λ ^ 4 * y
⊢ λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (↑3 ^ 1)
⊢ S'.a ^ 3 + 1 + (S'.b ^ 3 + 1) - (S'.a ^ 3 + S'.b ^ 3) = 2

Tactic:
ring

Result:
no goals