have h : 1 ≠ p.pred := fun h => by linarith [pred_eq_succ_iff.1 h.symm]
case h.e'_4
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
⊢ ∑ j ∈ range p, f0k₁ b p j • ζ ^ j = ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
case h.e'_4
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
h : 1 ≠ p.pred
⊢ ∑ j ∈ range p, f0k₁ b p j • ζ ^ j = ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩