no goals
α : Type u_1
β : Type u_2
γ : Type ?u.20373
δ : Type ?u.20376
a : α
s✝ t : Multiset α
f✝ g : α → Multiset β
b : β
s : Multiset α
f : α → Multiset β
⊢ b ∈ bind s f ↔ ∃ a, a ∈ s ∧ b ∈ f a
simp [bind]