simp (config := { contextual := true })
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)
this : filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ ∪ {0} = univ
h' :
  Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ) +
      Finset.card {0} =
    Finset.card univ
⊢ ∀ ⦃a : F⦄, a ∈ filter (fun x => x ≠ 0 ∧ IsSquare x) univ → a ∉ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
no goals