English
Given S', there exists S1 with the same multiplicity as S'.multiplicity.
Русский
Пусть дано S'; существует S1 с такой же кратностью, как и у S'.multiplicity.
LaTeX
$$$\exists S_1 \;\text{such that } S_1.multiplicity = S'.multiplicity$$$
Lean4
/-- Given `S' : Solution'`, we may assume that `λ ^ 2` divides `S'.a + S'.b ∨ λ ^ 2` (see also the
result below). -/
theorem 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' :=
by
rcases lambda_sq_dvd_or_dvd_or_dvd S' with h | h | h
· exact ⟨S'.a, S'.b, S'.H, S'.coprime, S'.ha, S'.hb, h⟩
· refine ⟨S'.a, η * S'.b, ?_, ?_, S'.ha, fun ⟨x, hx⟩ ↦ S'.hb ⟨η ^ 2 * x, ?_⟩, h⟩
· simp [mul_pow, hζ.toInteger_cube_eq_one, one_mul, S'.H]
· refine (isCoprime_mul_unit_left_right (Units.isUnit η) _ _).2 S'.coprime
·
rw [mul_comm _ x, ← mul_assoc, ← hx, mul_comm _ S'.b, mul_assoc, ← pow_succ', coe_eta, hζ.toInteger_cube_eq_one,
mul_one]
· refine ⟨S'.a, η ^ 2 * S'.b, ?_, ?_, S'.ha, fun ⟨x, hx⟩ ↦ S'.hb ⟨η * x, ?_⟩, h⟩
· rw [mul_pow, ← pow_mul, mul_comm 2, pow_mul, coe_eta, hζ.toInteger_cube_eq_one, one_pow, one_mul, S'.H]
· exact (isCoprime_mul_unit_left_right ((Units.isUnit η).pow _) _ _).2 S'.coprime
·
rw [mul_comm _ x, ← mul_assoc, ← hx, mul_comm _ S'.b, mul_assoc, ← pow_succ, coe_eta, hζ.toInteger_cube_eq_one,
mul_one]
