simp only [quadraticChar_apply, quadraticCharFun] at cf
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf : (Finset.sum univ fun a => ↑(quadraticChar F) a) = 0
⊢ Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) = Fintype.card F / 2 ∧
    Finset.card (filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ) = Fintype.card F / 2
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf : (Finset.sum univ fun x => if x = 0 then 0 else if IsSquare x then 1 else -1) = 0
⊢ Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) = Fintype.card F / 2 ∧
    Finset.card (filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ) = Fintype.card F / 2