no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
hf : InjOn f (f ⁻¹' ↑t)
⊢ (∀ (x : α), x ∈ s → f x ∈ t) ↔ s ⊆ preimage t f hf
simp only [subset_iff, mem_preimage]