-- Mathlib/NumberTheory/FLT/Three.lean
/-- Given `S' : Solution'`, we may assume that `λ ^ 2` divides `S'.a + S'.b ∨ λ ^ 2` (see also the
result below). -/
lemma ex_cube_add_cube_eq_and_isCoprime_and_not_dvd_and_dvd :
    ∃ (a' b' : 𝓞 K), a' ^ 3 + b' ^ 3 = S'.u * S'.c ^ 3 ∧ IsCoprime a' b' ∧ ¬ λ ∣ a' ∧
      ¬ λ ∣ b' ∧ λ ^ 2 ∣ a' + b'

Proof state:
case inr.inr
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 + ↑η ^ 2 * S'.b
⊢ ∃ a' b', a' ^ 3 + b' ^ 3 = ↑S'.u * S'.c ^ 3 ∧ IsCoprime a' b' ∧ ¬λ ∣ a' ∧ ¬λ ∣ b' ∧ λ ^ 2 ∣ a' + b'

Tactic:
refine ⟨S'.a, η ^ 2 * S'.b, ?_, ?_, S'.ha, fun ⟨x, hx⟩ ↦ S'.hb ⟨η * x, ?_⟩, h⟩

Result:
case inr.inr.refine_1
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 + ↑η ^ 2 * S'.b
⊢ S'.a ^ 3 + (↑η ^ 2 * S'.b) ^ 3 = ↑S'.u * S'.c ^ 3

case inr.inr.refine_2
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 + ↑η ^ 2 * S'.b
⊢ IsCoprime S'.a (↑η ^ 2 * S'.b)

case inr.inr.refine_3
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 + ↑η ^ 2 * S'.b
x✝ : λ ∣ ↑η ^ 2 * S'.b
x : 𝓞 K
hx : ↑η ^ 2 * S'.b = λ * x
⊢ S'.b = λ * (↑η * x)

Proof state:
case inr.inl.refine_1
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
⊢ S'.a ^ 3 + (↑η * S'.b) ^ 3 = ↑S'.u * S'.c ^ 3

Tactic:
simp [mul_pow, ← val_pow_eq_pow_val, hζ.toInteger_cube_eq_one, val_one, one_mul, S'.H]

Result:
no goals

Proof state:
case inr.inl
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
⊢ ∃ a' b', a' ^ 3 + b' ^ 3 = ↑S'.u * S'.c ^ 3 ∧ IsCoprime a' b' ∧ ¬λ ∣ a' ∧ ¬λ ∣ b' ∧ λ ^ 2 ∣ a' + b'

Tactic:
refine ⟨S'.a, η * S'.b, ?_, ?_, S'.ha, fun ⟨x, hx⟩ ↦ S'.hb ⟨η ^ 2 * x, ?_⟩, h⟩

Result:
case inr.inl.refine_1
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
⊢ S'.a ^ 3 + (↑η * S'.b) ^ 3 = ↑S'.u * S'.c ^ 3

case inr.inl.refine_2
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
⊢ IsCoprime S'.a (↑η * S'.b)

case inr.inl.refine_3
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
x✝ : λ ∣ ↑η * S'.b
x : 𝓞 K
hx : ↑η * S'.b = λ * x
⊢ S'.b = λ * (↑η ^ 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
inst✝ : DecidableRel fun a b => a ∣ b
⊢ ∃ a' b', a' ^ 3 + b' ^ 3 = ↑S'.u * S'.c ^ 3 ∧ IsCoprime a' b' ∧ ¬λ ∣ a' ∧ ¬λ ∣ b' ∧ λ ^ 2 ∣ a' + b'

Tactic:
rcases lambda_sq_dvd_or_dvd_or_dvd S' with h | h | h

Result:
case inl
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
⊢ ∃ a' b', a' ^ 3 + b' ^ 3 = ↑S'.u * S'.c ^ 3 ∧ IsCoprime a' b' ∧ ¬λ ∣ a' ∧ ¬λ ∣ b' ∧ λ ^ 2 ∣ a' + b'

case inr.inl
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
⊢ ∃ a' b', a' ^ 3 + b' ^ 3 = ↑S'.u * S'.c ^ 3 ∧ IsCoprime a' b' ∧ ¬λ ∣ a' ∧ ¬λ ∣ b' ∧ λ ^ 2 ∣ a' + b'

case inr.inr
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 + ↑η ^ 2 * S'.b
⊢ ∃ a' b', a' ^ 3 + b' ^ 3 = ↑S'.u * S'.c ^ 3 ∧ IsCoprime a' b' ∧ ¬λ ∣ a' ∧ ¬λ ∣ b' ∧ λ ^ 2 ∣ a' + b'

Proof state:
case inr.inr.refine_3
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 + ↑η ^ 2 * S'.b
x✝ : λ ∣ ↑η ^ 2 * S'.b
x : 𝓞 K
hx : ↑η ^ 2 * S'.b = λ * x
⊢ S'.b = λ * (↑η * x)

Tactic:
rw [mul_comm _ x, ← mul_assoc, ← hx, mul_comm _ S'.b, mul_assoc, ← pow_succ, coe_eta,
  hζ.toInteger_cube_eq_one, mul_one]

Result:
no goals

Proof state:
case inr.inl.refine_3
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
x✝ : λ ∣ ↑η * S'.b
x : 𝓞 K
hx : ↑η * S'.b = λ * x
⊢ S'.b = λ * (↑η ^ 2 * x)

Tactic:
rw [mul_comm _ x, ← mul_assoc, ← hx, mul_comm _ S'.b, mul_assoc, ← pow_succ', coe_eta,
  hζ.toInteger_cube_eq_one, mul_one]

Result:
no goals

Proof state:
case inl
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
⊢ ∃ a' b', a' ^ 3 + b' ^ 3 = ↑S'.u * S'.c ^ 3 ∧ IsCoprime a' b' ∧ ¬λ ∣ a' ∧ ¬λ ∣ b' ∧ λ ^ 2 ∣ a' + b'

Tactic:
exact ⟨S'.a, S'.b, S'.H, S'.coprime, S'.ha, S'.hb, h⟩

Result:
no goals

Proof state:
case inr.inr.refine_2
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 + ↑η ^ 2 * S'.b
⊢ IsCoprime S'.a (↑η ^ 2 * S'.b)

Tactic:
exact (isCoprime_mul_unit_left_right ((Units.isUnit η).pow _) _ _).2 S'.coprime

Result:
no goals

Proof state:
case inr.inr.refine_1
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 + ↑η ^ 2 * S'.b
⊢ S'.a ^ 3 + (↑η ^ 2 * S'.b) ^ 3 = ↑S'.u * S'.c ^ 3

Tactic:
rw [mul_pow, ← pow_mul, mul_comm 2, pow_mul, coe_eta, hζ.toInteger_cube_eq_one, one_pow,
  one_mul, S'.H]

Result:
no goals

Proof state:
case inr.inl.refine_2
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
⊢ IsCoprime S'.a (↑η * S'.b)

Tactic:
refine (isCoprime_mul_unit_left_right (Units.isUnit η) _ _).2 S'.coprime

Result:
no goals