no goals
α : Type u_2
β : Type u_1
γ : Type ?u.18111
δ : Type ?u.18114
a : α
s t : Multiset α
f✝ g : α → Multiset β
f : α → β
⊢ (bind 0 fun x => {f x}) = map f 0
rw [zero_bind, map_zero]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.18111
δ : Type ?u.18114
a : α
s t : Multiset α
f✝ g : α → Multiset β
f : α → β
⊢ ∀ ⦃a : α⦄ {s : Multiset α}, (bind s fun x => {f x}) = map f s → (bind (a ::ₘ s) fun x => {f x}) = map f (a ::ₘ s)
simp [singleton_add]