∀ {α : Type u_1} {β : Type v} {M : Type u_4} [inst : CommMonoid M] (s : Multiset α) (t : Multiset β) (f : α × β → M),
  (Multiset.map f (s ×ˢ t)).prod = (Multiset.map (fun i => (Multiset.map (fun j => f (i, j)) t).prod) s).prod