no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → β
s : Finset β
hf : Injective f
⊢ ↑(preimage (sᶜ) f (_ : InjOn f (f ⁻¹' ↑(sᶜ)))) = ↑(preimage s f (_ : InjOn f (f ⁻¹' ↑s))ᶜ)
simp