α : Type u_1
β : Type ?u.19141
γ : Type ?u.19144
inst✝¹ : Fintype α
s✝ t : Finset α
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ Set.InjOn (fun a => insert a s) (↑sᶜ)
α : Type u_1
β : Type ?u.19141
γ : Type ?u.19144
inst✝¹ : Fintype α
s✝ t : Finset α
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ Set.InjOn (fun a => insert a s) ↑(sᶜ)
rw [coe_compl]
no goals
α : Type u_1
β : Type ?u.19141
γ : Type ?u.19144
inst✝¹ : Fintype α
s✝ t : Finset α
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ Set.InjOn (fun a => insert a s) (↑sᶜ)
exact s.insert_inj_on