have cf := quadraticChar_sum_zero hF
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
⊢ 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 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