no goals
α : Type u_1
β : Type ?u.70742
γ : Type ?u.70745
δ : Type ?u.70748
σ : α → Type u_2
a : α
s✝ : Multiset α
t✝ : (a : α) → Multiset (σ a)
s t : Multiset α
u : (a : α) → Multiset (σ a)
⊢ Multiset.sigma (s + t) u = Multiset.sigma s u + Multiset.sigma t u
simp [Multiset.sigma]