no goals
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.31281
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
n : β → Multiset γ
f : α → β
⊢ bind (map f 0) n = bind 0 fun a => n (f a)
simp
no goals
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.31281
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
n : β → Multiset γ
f : α → β
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    (bind (map f s) n = bind s fun a => n (f a)) → bind (map f (a ::ₘ s)) n = bind (a ::ₘ s) fun a => n (f a)
simp (config := { contextual := true })