no goals
α : Type u_1
β : Type ?u.77099
γ : Type ?u.77102
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
inst✝ : DecidableEq α
x✝ : α
⊢ x✝ ∈ image id s ↔ x✝ ∈ s
simp only [mem_image, exists_prop, id, exists_eq_right]