refine' filter_congr _
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ ∀ x ∈ univ, ¬IsSquare x ↔ x ≠ 0 ∧ ¬IsSquare x