have H₁ := congr_arg (algebraMap ℤ R) 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, ⋯⟩ ℚ))
⊢ ∃ 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₁ :
  (algebraMap ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) (a ^ p + b ^ p) = (algebraMap ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) (c ^ p)
⊢ ∃ I, span {↑a + ζ * ↑b} = I ^ p