rw [pow_add_pow_eq_prod_add_zeta_runity_mul
  (hpri.out.eq_two_or_odd.resolve_left fun h => by simp [h] at h5p) hζ'] at 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₁ : ↑a ^ p + ↑b ^ p = ↑c ^ p
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑⟨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₁ : ∏ ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)), (↑a + ζ * ↑b) = ↑c ^ p
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑⟨p, ⋯⟩
⊢ ∃ I, span {↑a + ζ * ↑b} = I ^ p