refine' Finset.exists_eq_pow_of_mul_eq_pow_of_coprime (fun η₁ hη₁ η₂ hη₂ hη => ?_) H₁ ζ hζ
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑⟨p, ⋯⟩
H₁ : ∏ i ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)), span {↑a + i * ↑b} = span {↑c} ^ p
⊢ ∃ I, span {↑a + ζ * ↑b} = I ^ p
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑⟨p, ⋯⟩
H₁ : ∏ i ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)), span {↑a + i * ↑b} = span {↑c} ^ p
η₁ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hη₁ : η₁ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
η₂ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hη₂ : η₂ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hη : η₁ ≠ η₂
⊢ IsCoprime (span {↑a + η₁ * ↑b}) (span {↑a + η₂ * ↑b})