have key : ↑(p : ℤ) ∣ ∑ j in range p, f0k₂ a b j • ζ ^ j := by
  convert hdiv using 1
  simp_rw [f0k₂, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right zero_ne_one,
    Finset.range_filter_eq]
  simp only [hpri.pos, hpri.one_lt, if_true, zsmul_eq_mul, Int.cast_sub, sum_singleton,
    _root_.pow_zero, mul_one, pow_one, Ne, zero_smul, sum_const_zero, add_zero, Fin.val_mk]
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
⊢ False
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
key : ↑↑p ∣ ∑ j ∈ range p, f0k₂ a b j • ζ ^ j
⊢ False