rw [Fintype.card_of_bijective hb]
α : 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, ⋯⟩
hb : Function.Bijective b
⊢ Fintype.card { a // s ∈ a } = Fintype.card { a // s ∉ a }
no goals