no goals
α : Type u_2
β : Type u_1
γ : Type ?u.74073
inst✝ : DecidableEq β
f✝ g : α → β
s : Finset α
t : Finset β
a : α
b c : β
f : α → β
⊢ ∀ (x : β), x ∈ ↑(image f s) ↔ x ∈ f '' ↑s
simp only [mem_coe, mem_image, Set.mem_image, implies_true]