no goals
α : Type u_2
β : Type u_1
γ : Type ?u.13993
δ : Type ?u.13996
a : α
s t : Multiset α
f✝ g✝ : α → Multiset β
f : α → β
g : α → Multiset β
⊢ (bind 0 fun a => f a ::ₘ g a) = map f 0 + bind 0 g
simp
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.13993
δ : Type ?u.13996
a : α
s t : Multiset α
f✝ g✝ : α → Multiset β
f : α → β
g : α → Multiset β
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    (bind s fun a => f a ::ₘ g a) = map f s + bind s g →
      (bind (a ::ₘ s) fun a => f a ::ₘ g a) = map f (a ::ₘ s) + bind (a ::ₘ s) g
simp (config := { contextual := true }) [add_comm, add_left_comm, add_assoc]