let b : {a : Finset α // s ∉ a} → {a : Finset α // s ∈ a} :=
   fun ⟨a, ha⟩ ↦ ⟨Finset.cons s a ha, Finset.mem_cons_self s a⟩
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
⊢ Fintype.card { a // s ∈ a } = Fintype.card { a // s ∉ a }
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
b : { a // s ∉ a } → { a // s ∈ a } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.cons s a ha, ⋯⟩
⊢ Fintype.card { a // s ∈ a } = Fintype.card { a // s ∉ a }