no goals
α : Type u_1
β : Type u_2
γ : Type ?u.80867
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
s₁ s₂ : Finset α
h : s₁ ⊆ s₂
⊢ image f s₁ ⊆ image f s₂
simp only [subset_def, image_val, subset_dedup', dedup_subset', Multiset.map_subset_map h]