no goals
α : Type u_1
β : Type u_2
γ : Type ?u.516416
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
inst✝ : DecidableEq α
s : Multiset α
t : α → Multiset β
x : β
⊢ x ∈ toFinset (Multiset.bind s t) ↔ x ∈ Finset.biUnion (toFinset s) fun a => toFinset (t a)
simp only [Multiset.mem_toFinset, mem_biUnion, Multiset.mem_bind, exists_prop]