simp[mem_imageOfFinset_iff]
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
a : α
ha : a ∈ s
⊢ f a ha ∈ s.imageOfFinset f
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
a : α
ha : a ∈ s
⊢ ∃ a_1, ∃ (ha_1 : a_1 ∈ s), f a_1 ha_1 = f a ha