obtain ⟨k, hk⟩ := FltRegular.CaseI.exists_int_sum_eq_zero hζ' hP hpri.out a b 1 hu.symm
case intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑a + ↑b * ↑(hζ'.unit' ^ 1) - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑(hζ'.unit' ^ (-1))) ∈ span {↑↑⟨p, ⋯⟩}
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂