rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
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 left.mk.mk
α : 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, ⋯⟩
x : Finset α
hx : s ∉ x
y : Finset α
hy : s ∉ y
hxy : b ⟨x, hx⟩ = b ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩