simp [hpri.one_lt, Nat.sub_lt hpri.pos, sub_eq_add_neg]
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
⊢ ∑ x ∈ if 1 < p then {1} else ∅, b • ζ ^ x +
      (∑ x ∈ if p.pred < p then {p.pred} else ∅, -b • ζ ^ x +
        ∑ x ∈ filter (fun a => a ≠ 1 ∧ a ≠ p.pred) (range p), 0 • ζ ^ x) =
    ↑b * ζ ^ 1 - ↑b * ζ ^ p.pred
no goals