case empty
α : Type u_2
β : Type ?u.10571
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
ι : Type u_1
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun i => fold op (b i) (t i)) 0)

case cons
α : Type u_2
β : Type ?u.10571
op : α → α → α
hc : IsCommutative α op
ha✝ : IsAssociative α op
ι : Type u_1
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (bind ha t) = fold op b₀ (map (fun i => fold op (b i) (t i)) ha)
⊢ fold op (fold op b₀ (map b (a ::ₘ ha))) (bind (a ::ₘ ha) t) =
    fold op b₀ (map (fun i => fold op (b i) (t i)) (a ::ₘ ha))
α : Type u_2
β : Type ?u.10571
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
ι : Type u_1
s : Multiset ι
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ (map b s)) (bind s t) = fold op b₀ (map (fun i => fold op (b i) (t i)) s)
induction' s using Multiset.induction_on with a ha ih
no goals
case empty
α : Type u_2
β : Type ?u.10571
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
ι : Type u_1
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun i => fold op (b i) (t i)) 0)
rw [zero_bind, map_zero, map_zero, fold_zero]
no goals
case cons
α : Type u_2
β : Type ?u.10571
op : α → α → α
hc : IsCommutative α op
ha✝ : IsAssociative α op
ι : Type u_1
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (bind ha t) = fold op b₀ (map (fun i => fold op (b i) (t i)) ha)
⊢ fold op (fold op b₀ (map b (a ::ₘ ha))) (bind (a ::ₘ ha) t) =
    fold op b₀ (map (fun i => fold op (b i) (t i)) (a ::ₘ ha))
rw [cons_bind, map_cons, map_cons, fold_cons_left, fold_cons_left, fold_add, ih]