constructor
α : 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, ⋯⟩
⊢ Function.Bijective b
case left
α : 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, ⋯⟩
⊢ Function.Injective b

case right
α : 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, ⋯⟩
⊢ Function.Surjective b