no goals
α : Type u_1
β : Type u_2
γ : Type ?u.59441
δ : Type ?u.59444
a : α
b : β
s✝ : Multiset α
t✝ : Multiset β
s t : Multiset α
u : Multiset β
⊢ (s + t) ×ˢ u = s ×ˢ u + t ×ˢ u
simp [SProd.sprod, product]