replace hζ := hζ.mem_nthRootsFinset hpri.out.pos
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hζ : IsPrimitiveRoot ζ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b