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