Maps and filters of a product of multisets

The Multiset analogues of Finset.prodMap_image_product and Finset.filter_product: mapping s ×ˢ t by a function on each coordinate maps each factor, and filtering it by a predicate on each coordinate filters each factor. [UPSTREAM] candidates; eventual mathlib home Mathlib.Data.Multiset.Bind.

theorem Multiset.prodMap_map_product {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ) (s : Multiset α) (t : Multiset β) : map (Prod.map f g) (s ×ˢ t) = map f s ×ˢ map g t

theorem Multiset.map_map_product_distrib {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {α' : Type u_5} {β' : Type u_6} {f : α × β → γ} {g : γ → δ} {f' : α' × β' → δ} {g₁ : α → α'} {g₂ : β → β'} (h : ∀ (a : α) (b : β), g (f (a, b)) = f' (g₁ a, g₂ b)) (s : Multiset α) (t : Multiset β) : map g (map f (s ×ˢ t)) = map f' (map g₁ s ×ˢ map g₂ t)

A map that sends a binary operation f to f' along g₁ and g₂ carries the f-image of a product to the f'-image of the product of the images (Finset.image_image₂_distrib analogue).

theorem Multiset.filter_product {α : Type u_1} {β : Type u_2} {s : Multiset α} {t : Multiset β} (p : α → Prop) (q : β → Prop) [DecidablePred p] [DecidablePred q] : filter (fun (x : α × β) => p x.1 ∧ q x.2) (s ×ˢ t) = filter p s ×ˢ filter q t