no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
inst✝¹ : Fintype ↑s
f : α → β
inst✝ : Fintype ↑(f '' s)
H : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y → x = y
this : (a : Prop) → Decidable a
⊢ ∀ (x : β), x ∈ Finset.image f (toFinset s) ↔ x ∈ f '' s
simp