no goals
α : Type u_3
β : Type u_2
γ : Type u_1
inst✝¹ : DecidableEq β
f g✝ : α → β
s : Finset α
t : Finset β
a : α
b c : β
inst✝ : DecidableEq γ
g : β → γ
⊢ (image g (image f s)).val = (image (g ∘ f) s).val
simp only [image_val, dedup_map_dedup_eq, Multiset.map_map]