no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : DecidableEq β
f : α → β
s : Finset β
hf : BijOn f (f ⁻¹' ↑s) ↑s
⊢ ↑(image f (preimage s f (_ : InjOn f (f ⁻¹' ↑s)))) = ↑s
simpa using hf.image_eq