no goals
α : Type u_2
β : Type u_1
γ : Type ?u.62593
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
p : β → Prop
⊢ (∀ (b : β), b ∈ image f s → p b) ↔ ∀ (a : α), a ∈ s → p (f a)
simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]