have key : ↑(p : ℤ) ∣ ∑ j in range p, f1k₂ a j • ζ ^ j := by
  suffices ∑ j in range p, f1k₂ a j • ζ ^ j = ↑a - ↑a * ζ ^ 2 by
    rwa [this]
  simp_rw [f1k₂, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right
    (show 0 ≠ 2 by norm_num), Finset.range_filter_eq]
  simp only [hpri.pos, ite_true, zsmul_eq_mul, sum_singleton, _root_.pow_zero, mul_one, two_lt hp5, neg_smul,
sum_neg_distrib, ne_eq, mem_range, not_and, not_not, zero_smul, sum_const_zero, add_zero]
  ring
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
⊢ False
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
key : ↑↑p ∣ ∑ j ∈ range p, f1k₂ a j • ζ ^ j
⊢ False