rw [sum_ite, sum_const_zero, zero_add, sum_ite, sum_const, sum_const, nsmul_eq_mul, nsmul_eq_mul,
  mul_neg, mul_one, mul_one, add_neg_eq_zero, Nat.cast_inj, filter_filter, filter_filter] 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 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
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.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) 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