simp only [and_comm, ← filter_filter, filter_ne']
F✝ : Type u_1
inst✝⁴ : Fintype F✝
inst✝³ : Field F✝
F : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ Finset.card (filter IsSquare univ) = Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) + 1
F✝ : Type u_1
inst✝⁴ : Fintype F✝
inst✝³ : Field F✝
F : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ Finset.card (filter IsSquare univ) = Finset.card (erase (filter (fun a => IsSquare a) univ) 0) + 1