no goals
α : Type u_2
β : Type u_1
γ : Type ?u.94256
s✝ t : Set α
inst✝² : DecidableEq β
f : α → β
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑(f '' s)
⊢ ↑(toFinset (f '' s)) = ↑(Finset.image f (toFinset s))
simp