no goals
α : Type u_1
inst✝ : CommSemiring α
s : Multiset (Multiset α)
⊢ prod (map sum 0) = sum (map prod (Sections 0))
simp
no goals
α : Type u_1
inst✝ : CommSemiring α
s✝ : Multiset (Multiset α)
a : Multiset α
s : Multiset (Multiset α)
ih : prod (map sum s) = sum (map prod (Sections s))
⊢ prod (map sum (a ::ₘ s)) = sum (map prod (Sections (a ::ₘ s)))
simp [ih, map_bind, sum_map_mul_left, sum_map_mul_right]