no goals
α : Type u_2
β : Type u_1
γ : Type ?u.453885
inst✝¹ : DecidableEq α
s t : Multiset α
inst✝ : DecidableEq β
m : Multiset α
f : α → Multiset β
⊢ toFinset (bind (dedup m) f) = toFinset (bind m f)
simp_rw [toFinset, dedup_bind_dedup]