no goals
α : Type u_2
β : Type u_1
γ : Type ?u.47547
δ : Type ?u.47550
a : α
s✝ t✝ : Multiset α
f g : α → Multiset β
inst✝ : CommMonoid β
s : Multiset α
t : α → Multiset β
⊢ prod (bind 0 t) = prod (map (fun a => prod (t a)) 0)
simp
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.47547
δ : Type ?u.47550
a✝ : α
s✝¹ t✝ : Multiset α
f g : α → Multiset β
inst✝ : CommMonoid β
s✝ : Multiset α
t : α → Multiset β
a : α
s : Multiset α
ih : prod (bind s t) = prod (map (fun a => prod (t a)) s)
⊢ prod (bind (a ::ₘ s) t) = prod (map (fun a => prod (t a)) (a ::ₘ s))
simp [ih, cons_bind]