doc-next-gen

Mathlib.Data.Multiset.Bind

Module docstring

{"# Bind operation for multisets

This file defines a few basic operations on Multiset, notably the monadic bind.

Main declarations

  • Multiset.join: The join, aka union or sum, of multisets.
  • Multiset.bind: The bind of a multiset-indexed family of multisets.
  • Multiset.product: Cartesian product of two multisets.
  • Multiset.sigma: Disjoint sum of multisets in a sigma type. ","### Join ","### Bind ","### Product of two multisets ","### Disjoint sum of multisets "}
Multiset.join definition
: Multiset (Multiset α) → Multiset α
Full source 
/-- `join S`, where `S` is a multiset of multisets, is the lift of the list join
  operation, that is, the union of all the sets.
     join {{1, 2}, {1, 2}, {0, 1}} = {0, 1, 1, 1, 2, 2} -/
def join : Multiset (Multiset α) → Multiset α :=
  sum
Union of multisets
Informal description
Given a multiset $S$ of multisets over a type $\alpha$, the join of $S$ is the multiset obtained by taking the union (sum) of all the multisets in $S$. For example, $\text{join} \{\{1, 2\}, \{1, 2\}, \{0, 1\}\} = \{0, 1, 1, 1, 2, 2\}$.
Multiset.coe_join theorem
: ∀ L : List (List α), join (L.map ((↑) : List α → Multiset α) : Multiset (Multiset α)) = L.flatten
Full source 
theorem coe_join : ∀ L : List (List α), join (L.map ((↑) : List α → Multiset α) :
    Multiset (Multiset α)) = L.flatten
  | [] => rfl
  | l :: L => by
      exact congr_arg (fun s : Multiset α => ↑l + s) (coe_join L)
Join of Lifted Lists Equals Flattened List
Informal description
For any list of lists $L$ over a type $\alpha$, the join of the multiset obtained by lifting each list in $L$ to a multiset is equal to the flattened list of $L$, i.e., $\text{join}(\{\![ l \mid l \in L ]\!\}) = \text{flatten}(L)$, where $\{\![\cdot]\!\}$ denotes the multiset constructor and $\text{flatten}(L)$ is the concatenation of all lists in $L$.
Multiset.join_zero theorem
: @join α 0 = 0
Full source 
@[simp]
theorem join_zero : @join α 0 = 0 :=
  rfl
Join of Empty Multiset is Empty
Informal description
The join of the empty multiset of multisets over a type $\alpha$ is the empty multiset, i.e., $\text{join}(0) = 0$.
Multiset.join_cons theorem
(s S) : @join α (s ::ₘ S) = s + join S
Full source 
@[simp]
theorem join_cons (s S) : @join α (s ::ₘ S) = s + join S :=
  sum_cons _ _
Join of Multiset Insertion Equals Sum with Join
Informal description
For any multiset $s$ over a type $\alpha$ and any multiset $S$ of multisets over $\alpha$, the join of the multiset obtained by inserting $s$ into $S$ equals the sum of $s$ and the join of $S$, i.e., $\text{join}(s \cup S) = s + \text{join}(S)$.
Multiset.join_add theorem
(S T) : @join α (S + T) = join S + join T
Full source 
@[simp]
theorem join_add (S T) : @join α (S + T) = join S + join T :=
  sum_add _ _
Join Distributes Over Addition of Multisets
Informal description
For any multisets $S$ and $T$ of multisets over a type $\alpha$, the join of their sum equals the sum of their joins, i.e., $\text{join}(S + T) = \text{join}(S) + \text{join}(T)$.
Multiset.singleton_join theorem
(a) : join ({ a } : Multiset (Multiset α)) = a
Full source 
@[simp]
theorem singleton_join (a) : join ({a} : Multiset (Multiset α)) = a :=
  sum_singleton _
Join of Singleton Multiset Equals Its Element
Informal description
For any multiset $a$ over a type $\alpha$, the join of the singleton multiset $\{a\}$ is equal to $a$, i.e., $\text{join}(\{a\}) = a$.
Multiset.mem_join theorem
{a S} : a ∈ @join α S ↔ ∃ s ∈ S, a ∈ s
Full source 
@[simp]
theorem mem_join {a S} : a ∈ @join α Sa ∈ @join α S ↔ ∃ s ∈ S, a ∈ s :=
  Multiset.induction_on S (by simp) <| by
    simp +contextual [or_and_right, exists_or]
Membership in Multiset Join
Informal description
For any element $a$ of type $\alpha$ and any multiset $S$ of multisets over $\alpha$, the element $a$ belongs to the join of $S$ if and only if there exists a multiset $s$ in $S$ such that $a$ belongs to $s$. In symbols: \[ a \in \text{join}(S) \leftrightarrow \exists s \in S, a \in s \]
Multiset.card_join theorem
(S) : card (@join α S) = sum (map card S)
Full source 
@[simp]
theorem card_join (S) : card (@join α S) = sum (map card S) :=
  Multiset.induction_on S (by simp) (by simp)
Cardinality of Multiset Join Equals Sum of Cardinalities
Informal description
For any multiset $S$ of multisets over a type $\alpha$, the cardinality of the join of $S$ is equal to the sum of the cardinalities of the multisets in $S$. In symbols: \[ |\text{join}(S)| = \sum_{s \in S} |s| \]
Multiset.map_join theorem
(f : α → β) (S : Multiset (Multiset α)) : map f (join S) = join (map (map f) S)
Full source 
@[simp]
theorem map_join (f : α → β) (S : Multiset (Multiset α)) :
    map f (join S) = join (map (map f) S) := by
  induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]
Map and Join Commute for Multisets
Informal description
For any function $f : \alpha \to \beta$ and any multiset $S$ of multisets over $\alpha$, the image under $f$ of the join of $S$ is equal to the join of the multiset obtained by applying $f$ to each element of each multiset in $S$. In symbols: \[ \text{map}\, f\, (\text{join}\, S) = \text{join}\, (\text{map}\, (\text{map}\, f)\, S) \]
Multiset.prod_join theorem
[CommMonoid α] {S : Multiset (Multiset α)} : prod (join S) = prod (map prod S)
Full source 
@[to_additive (attr := simp)]
theorem prod_join [CommMonoid α] {S : Multiset (Multiset α)} :
    prod (join S) = prod (map prod S) := by
  induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]
Product of Join Equals Product of Products in Commutative Monoid
Informal description
Let $\alpha$ be a commutative monoid. For any multiset $S$ of multisets over $\alpha$, the product of the elements in the join of $S$ is equal to the product of the products of the elements in each multiset of $S$. In symbols: \[ \prod (\text{join}\, S) = \prod (\text{map}\, \prod\, S) \]
Multiset.rel_join theorem
{r : α → β → Prop} {s t} (h : Rel (Rel r) s t) : Rel r s.join t.join
Full source 
theorem rel_join {r : α → β → Prop} {s t} (h : Rel (Rel r) s t) : Rel r s.join t.join := by
  induction h with
  | zero => simp
  | cons hab hst ih => simpa using hab.add ih
Preservation of Lifted Relation under Multiset Join: $\text{Rel}\, (\text{Rel}\, r)\, s\, t \to \text{Rel}\, r\, (\text{join}\, s)\, (\text{join}\, t)$
Informal description
Let $r$ be a relation between elements of types $\alpha$ and $\beta$, and let $s$ and $t$ be multisets of multisets over $\alpha$ and $\beta$ respectively. If the lifted relation $\text{Rel}\, (\text{Rel}\, r)$ holds between $s$ and $t$, then the relation $\text{Rel}\, r$ holds between their joins $\text{join}\, s$ and $\text{join}\, t$.
Multiset.bind definition
(s : Multiset α) (f : α → Multiset β) : Multiset β
Full source 
/-- `s.bind f` is the monad bind operation, defined as `(s.map f).join`. It is the union of `f a` as
`a` ranges over `s`. -/
def bind (s : Multiset α) (f : α → Multiset β) : Multiset β :=
  (s.map f).join
Multiset monadic bind operation
Informal description
Given a multiset $s$ over a type $\alpha$ and a function $f : \alpha \to \text{Multiset} \beta$, the bind operation $\text{bind}(s, f)$ is defined as the union (sum) of all multisets $f(a)$ where $a$ ranges over $s$. In other words, it is the monadic bind operation for multisets, computed as the join of the multiset obtained by mapping $f$ over $s$.
Multiset.coe_bind theorem
(l : List α) (f : α → List β) : (@bind α β l fun a => f a) = l.flatMap f
Full source 
@[simp]
theorem coe_bind (l : List α) (f : α → List β) : (@bind α β l fun a => f a) = l.flatMap f := by
  rw [List.flatMap, ← coe_join, List.map_map]
  rfl
Multiset Bind of Coerced List Equals List FlatMap
Informal description
For any list $l$ of elements of type $\alpha$ and any function $f : \alpha \to \text{List} \beta$, the bind operation applied to $l$ (viewed as a multiset) and $f$ (composed with the multiset coercion) is equal to the flatMap of $l$ with $f$, i.e., $\text{bind}(l, f) = \text{flatMap}(f, l)$.
Multiset.zero_bind theorem
: bind 0 f = 0
Full source 
@[simp]
theorem zero_bind : bind 0 f = 0 :=
  rfl
Bind of Empty Multiset Yields Empty Multiset
Informal description
For any function $f : \alpha \to \text{Multiset} \beta$, the bind operation applied to the empty multiset $0$ yields the empty multiset, i.e., $\text{bind}(0, f) = 0$.
Multiset.cons_bind theorem
: (a ::ₘ s).bind f = f a + s.bind f
Full source 
@[simp]
theorem cons_bind : (a ::ₘ s).bind f = f a + s.bind f := by simp [bind]
Bind Operation on Multiset Insertion: $\text{bind}(a \cup s, f) = f(a) + \text{bind}(s, f)$
Informal description
For any element $a$ of type $\alpha$, any multiset $s$ over $\alpha$, and any function $f : \alpha \to \text{Multiset} \beta$, the bind operation satisfies: \[ \text{bind}(a \cup s, f) = f(a) + \text{bind}(s, f), \] where $a \cup s$ denotes the multiset obtained by inserting $a$ into $s$.
Multiset.singleton_bind theorem
: bind { a } f = f a
Full source 
@[simp]
theorem singleton_bind : bind {a} f = f a := by simp [bind]
Bind Operation on Singleton Multiset: $\text{bind}(\{a\}, f) = f(a)$
Informal description
For any element $a$ of type $\alpha$ and any function $f : \alpha \to \text{Multiset} \beta$, the bind operation applied to the singleton multiset $\{a\}$ satisfies $\text{bind}(\{a\}, f) = f(a)$.
Multiset.add_bind theorem
: (s + t).bind f = s.bind f + t.bind f
Full source 
@[simp]
theorem add_bind : (s + t).bind f = s.bind f + t.bind f := by simp [bind]
Additivity of Multiset Bind Operation
Informal description
For any multisets $s$ and $t$ over a type $\alpha$ and any function $f : \alpha \to \text{Multiset} \beta$, the bind operation satisfies: \[ (s + t) \bind f = (s \bind f) + (t \bind f). \]
Multiset.bind_zero theorem
: s.bind (fun _ => 0 : α → Multiset β) = 0
Full source 
@[simp]
theorem bind_zero : s.bind (fun _ => 0 : α → Multiset β) = 0 := by simp [bind, join, nsmul_zero]
Bind with Zero Function Yields Zero Multiset
Informal description
For any multiset $s$ over a type $\alpha$, the bind operation with the constant function that returns the empty multiset satisfies $s \bind (\lambda \_. 0) = 0$.
Multiset.bind_add theorem
: (s.bind fun a => f a + g a) = s.bind f + s.bind g
Full source 
@[simp]
theorem bind_add : (s.bind fun a => f a + g a) = s.bind f + s.bind g := by simp [bind, join]
Distributivity of Multiset Bind over Addition
Informal description
For any multiset $s$ over a type $\alpha$ and any two functions $f, g : \alpha \to \text{Multiset} \beta$, the bind operation satisfies the distributive property: \[ s \bind (\lambda a, f(a) + g(a)) = (s \bind f) + (s \bind g). \]
Multiset.bind_cons theorem
(f : α → β) (g : α → Multiset β) : (s.bind fun a => f a ::ₘ g a) = map f s + s.bind g
Full source 
@[simp]
theorem bind_cons (f : α → β) (g : α → Multiset β) :
    (s.bind fun a => f a ::ₘ g a) = map f s + s.bind g :=
  Multiset.induction_on s (by simp)
    (by simp +contextual [add_comm, add_left_comm, add_assoc])
Bind-Map Identity for Multisets: $\text{bind}(s, f \mathbin{::} g) = \text{map}(f, s) + \text{bind}(s, g)$
Informal description
For any function $f : \alpha \to \beta$, any function $g : \alpha \to \text{Multiset} \beta$, and any multiset $s$ over $\alpha$, the bind operation satisfies: \[ \text{bind}(s, \lambda a, f(a) \mathbin{::} g(a)) = \text{map}(f, s) + \text{bind}(s, g), \] where $f(a) \mathbin{::} g(a)$ denotes the multiset obtained by inserting $f(a)$ into $g(a)$.
Multiset.bind_singleton theorem
(f : α → β) : (s.bind fun x => ({f x} : Multiset β)) = map f s
Full source 
@[simp]
theorem bind_singleton (f : α → β) : (s.bind fun x => ({f x} : Multiset β)) = map f s :=
  Multiset.induction_on s (by rw [zero_bind, map_zero]) (by simp [singleton_add])
Bind with Singleton Yields Map: $\text{bind}(s, \{f(\cdot)\}) = \text{map}(f, s)$
Informal description
For any function $f : \alpha \to \beta$ and multiset $s$ over $\alpha$, the bind operation of $s$ with the function mapping each $x \in \alpha$ to the singleton multiset $\{f(x)\}$ is equal to the image of $s$ under $f$. In symbols: \[ \text{bind}(s, \lambda x, \{f(x)\}) = \text{map}(f, s) \]
Multiset.mem_bind theorem
{b s} {f : α → Multiset β} : b ∈ bind s f ↔ ∃ a ∈ s, b ∈ f a
Full source 
@[simp]
theorem mem_bind {b s} {f : α → Multiset β} : b ∈ bind s fb ∈ bind s f ↔ ∃ a ∈ s, b ∈ f a := by
  simp [bind]
Membership in Multiset Bind Operation
Informal description
For any element $b$ of type $\beta$, multiset $s$ over type $\alpha$, and function $f : \alpha \to \text{Multiset} \beta$, the element $b$ belongs to the bind of $s$ with $f$ if and only if there exists an element $a \in s$ such that $b \in f(a)$. In symbols: $$b \in \text{bind}(s, f) \leftrightarrow \exists a \in s, b \in f(a)$$
Multiset.card_bind theorem
: card (s.bind f) = (s.map (card ∘ f)).sum
Full source 
@[simp]
theorem card_bind : card (s.bind f) = (s.map (cardcard ∘ f)).sum := by simp [bind]
Cardinality of Multiset Bind Equals Sum of Cardinalities
Informal description
For any multiset $s$ over a type $\alpha$ and any function $f : \alpha \to \text{Multiset} \beta$, the cardinality of the bind operation $\text{bind}(s, f)$ is equal to the sum of the cardinalities of the multisets $f(a)$ for each $a \in s$. In symbols: \[ |\text{bind}(s, f)| = \sum_{a \in s} |f(a)| \]
Multiset.bind_congr theorem
{f g : α → Multiset β} {m : Multiset α} : (∀ a ∈ m, f a = g a) → bind m f = bind m g
Full source 
theorem bind_congr {f g : α → Multiset β} {m : Multiset α} :
    (∀ a ∈ m, f a = g a) → bind m f = bind m g := by simp +contextual [bind]
Congruence of Multiset Bind Operation: $\text{bind}(m, f) = \text{bind}(m, g)$ when $f(a) = g(a)$ for all $a \in m$
Informal description
For any two functions $f, g : \alpha \to \text{Multiset} \beta$ and any multiset $m$ over $\alpha$, if $f(a) = g(a)$ for all $a \in m$, then the bind operations $\text{bind}(m, f)$ and $\text{bind}(m, g)$ are equal.
Multiset.bind_hcongr theorem
{β' : Type v} {m : Multiset α} {f : α → Multiset β} {f' : α → Multiset β'} (h : β = β') (hf : ∀ a ∈ m, HEq (f a) (f' a)) : HEq (bind m f) (bind m f')
Full source 
theorem bind_hcongr {β' : Type v} {m : Multiset α} {f : α → Multiset β} {f' : α → Multiset β'}
    (h : β = β') (hf : ∀ a ∈ m, HEq (f a) (f' a)) : HEq (bind m f) (bind m f') := by
  subst h
  simp only [heq_eq_eq] at hf
  simp [bind_congr hf]
Heterogeneous Congruence of Multiset Bind Operation
Informal description
Let $β'$ be a type, $m$ a multiset over type $α$, and $f : α → \text{Multiset} β$, $f' : α → \text{Multiset} β'$ two functions. If $β = β'$ and for every $a \in m$ the multisets $f(a)$ and $f'(a)$ are heterogeneously equal, then the bind operations $\text{bind}(m, f)$ and $\text{bind}(m, f')$ are also heterogeneously equal.
Multiset.map_bind theorem
(m : Multiset α) (n : α → Multiset β) (f : β → γ) : map f (bind m n) = bind m fun a => map f (n a)
Full source 
theorem map_bind (m : Multiset α) (n : α → Multiset β) (f : β → γ) :
    map f (bind m n) = bind m fun a => map f (n a) := by simp [bind]
Commutativity of Map and Bind for Multisets: $\text{map}\, f \circ \text{bind}\, m\, n = \text{bind}\, m\, (\text{map}\, f \circ n)$
Informal description
For any multiset $m$ over a type $\alpha$, any function $n : \alpha \to \text{Multiset} \beta$, and any function $f : \beta \to \gamma$, the following equality holds: \[ \text{map}\, f\, (\text{bind}\, m\, n) = \text{bind}\, m\, \left(\lambda a, \text{map}\, f\, (n a)\right). \]
Multiset.bind_map theorem
(m : Multiset α) (n : β → Multiset γ) (f : α → β) : bind (map f m) n = bind m fun a => n (f a)
Full source 
theorem bind_map (m : Multiset α) (n : β → Multiset γ) (f : α → β) :
    bind (map f m) n = bind m fun a => n (f a) :=
  Multiset.induction_on m (by simp) (by simp +contextual)
Commutativity of Bind and Map for Multisets: $\text{bind}(\text{map}(f, m), n) = \text{bind}(m, n \circ f)$
Informal description
For any multiset $m$ over a type $\alpha$, any function $n : \beta \to \text{Multiset} \gamma$, and any function $f : \alpha \to \beta$, the following equality holds: \[ \text{bind}(\text{map}(f, m), n) = \text{bind}(m, \lambda a, n(f(a))). \] Here, $\text{map}(f, m)$ denotes the multiset obtained by applying $f$ to each element of $m$, and $\text{bind}$ is the monadic bind operation for multisets.
Multiset.bind_assoc theorem
{s : Multiset α} {f : α → Multiset β} {g : β → Multiset γ} : (s.bind f).bind g = s.bind fun a => (f a).bind g
Full source 
theorem bind_assoc {s : Multiset α} {f : α → Multiset β} {g : β → Multiset γ} :
    (s.bind f).bind g = s.bind fun a => (f a).bind g :=
  Multiset.induction_on s (by simp) (by simp +contextual)
Associativity of Multiset Bind Operation
Informal description
For any multiset $s$ over a type $\alpha$, any function $f : \alpha \to \text{Multiset} \beta$, and any function $g : \beta \to \text{Multiset} \gamma$, the following associativity property holds: \[ (s \bind f) \bind g = s \bind \left(\lambda a, (f a) \bind g\right). \]
Multiset.bind_bind theorem
(m : Multiset α) (n : Multiset β) {f : α → β → Multiset γ} : ((bind m) fun a => (bind n) fun b => f a b) = (bind n) fun b => (bind m) fun a => f a b
Full source 
theorem bind_bind (m : Multiset α) (n : Multiset β) {f : α → β → Multiset γ} :
    ((bind m) fun a => (bind n) fun b => f a b) = (bind n) fun b => (bind m) fun a => f a b :=
  Multiset.induction_on m (by simp) (by simp +contextual)
Commutativity of Nested Multiset Binds: $(m \bind \lambda a, n \bind \lambda b, f a b) = (n \bind \lambda b, m \bind \lambda a, f a b)$
Informal description
For any multisets $m$ over type $\alpha$ and $n$ over type $\beta$, and any function $f : \alpha \to \beta \to \text{Multiset} \gamma$, the following equality holds: \[ m \bind \left(\lambda a, n \bind \left(\lambda b, f a b\right)\right) = n \bind \left(\lambda b, m \bind \left(\lambda a, f a b\right)\right). \]
Multiset.bind_map_comm theorem
(m : Multiset α) (n : Multiset β) {f : α → β → γ} : ((bind m) fun a => n.map fun b => f a b) = (bind n) fun b => m.map fun a => f a b
Full source 
theorem bind_map_comm (m : Multiset α) (n : Multiset β) {f : α → β → γ} :
    ((bind m) fun a => n.map fun b => f a b) = (bind n) fun b => m.map fun a => f a b :=
  Multiset.induction_on m (by simp) (by simp +contextual)
Commutativity of Bind and Map Operations on Multisets: $m \bind (a \mapsto n \map (b \mapsto f a b)) = n \bind (b \mapsto m \map (a \mapsto f a b))$
Informal description
For any multisets $m$ over type $\alpha$ and $n$ over type $\beta$, and any function $f : \alpha \to \beta \to \gamma$, the following equality holds: \[ m \bind \left(\lambda a, n \map \left(\lambda b, f a b\right)\right) = n \bind \left(\lambda b, m \map \left(\lambda a, f a b\right)\right), \] where $\bind$ denotes the multiset bind operation and $\map$ denotes the multiset map operation.
Multiset.prod_bind theorem
[CommMonoid β] (s : Multiset α) (t : α → Multiset β) : (s.bind t).prod = (s.map fun a => (t a).prod).prod
Full source 
@[to_additive (attr := simp)]
theorem prod_bind [CommMonoid β] (s : Multiset α) (t : α → Multiset β) :
    (s.bind t).prod = (s.map fun a => (t a).prod).prod := by simp [bind]
Product of Bind Equals Product of Products in Commutative Monoid
Informal description
Let $\beta$ be a commutative monoid. For any multiset $s$ over a type $\alpha$ and any function $t : \alpha \to \text{Multiset} \beta$, the product of the elements in the bind of $s$ and $t$ is equal to the product of the products of the elements in each multiset $t(a)$ for $a \in s$. In symbols: \[ \prod (s \bind t) = \prod \left(s \map \left(\lambda a, \prod (t a)\right)\right). \]
Multiset.rel_bind theorem
{r : α → β → Prop} {p : γ → δ → Prop} {s t} {f : α → Multiset γ} {g : β → Multiset δ} (h : (r ⇒ Rel p) f g) (hst : Rel r s t) : Rel p (s.bind f) (t.bind g)
Full source 
theorem rel_bind {r : α → β → Prop} {p : γ → δ → Prop} {s t} {f : α → Multiset γ}
    {g : β → Multiset δ} (h : (r ⇒ Rel p) f g) (hst : Rel r s t) :
    Rel p (s.bind f) (t.bind g) := by
  apply rel_join
  rw [rel_map]
  exact hst.mono fun a _ b _ hr => h hr
Preservation of Lifted Relation under Multiset Bind Operation: $\text{Rel}\, p\, (\text{bind}\, s\, f)\, (\text{bind}\, t\, g)$
Informal description
Let $r$ be a relation between types $\alpha$ and $\beta$, and $p$ a relation between types $\gamma$ and $\delta$. Given functions $f : \alpha \to \text{Multiset} \gamma$ and $g : \beta \to \text{Multiset} \delta$ such that for all $a \in \alpha$ and $b \in \beta$ with $r(a,b)$, the lifted relation $\text{Rel}\, p$ holds between $f(a)$ and $g(b)$, and given multisets $s$ over $\alpha$ and $t$ over $\beta$ with $\text{Rel}\, r\, s\, t$, then the relation $\text{Rel}\, p$ holds between the binds $\text{bind}(s, f)$ and $\text{bind}(t, g)$.
Multiset.count_sum theorem
[DecidableEq α] {m : Multiset β} {f : β → Multiset α} {a : α} : count a (map f m).sum = sum (m.map fun b => count a <| f b)
Full source 
theorem count_sum [DecidableEq α] {m : Multiset β} {f : β → Multiset α} {a : α} :
    count a (map f m).sum = sum (m.map fun b => count a <| f b) :=
  Multiset.induction_on m (by simp) (by simp)
Count Preservation under Sum of Mapped Multisets: $\text{count}(a, \sum (m \map f)) = \sum (m \map (\lambda b, \text{count}(a, f b)))$
Informal description
For any type $\alpha$ with decidable equality, given a multiset $m$ over a type $\beta$, a function $f : \beta \to \text{Multiset} \alpha$, and an element $a \in \alpha$, the multiplicity of $a$ in the sum of the multisets obtained by mapping $f$ over $m$ is equal to the sum of the multiplicities of $a$ in each multiset $f(b)$ for $b \in m$. In symbols: \[ \text{count}(a, \sum (m \map f)) = \sum (m \map (\lambda b, \text{count}(a, f b))). \]
Multiset.count_bind theorem
[DecidableEq α] {m : Multiset β} {f : β → Multiset α} {a : α} : count a (bind m f) = sum (m.map fun b => count a <| f b)
Full source 
theorem count_bind [DecidableEq α] {m : Multiset β} {f : β → Multiset α} {a : α} :
    count a (bind m f) = sum (m.map fun b => count a <| f b) :=
  count_sum
Multiplicity Preservation under Multiset Bind Operation
Informal description
For any type $\alpha$ with decidable equality, given a multiset $m$ over a type $\beta$, a function $f : \beta \to \text{Multiset} \alpha$, and an element $a \in \alpha$, the multiplicity of $a$ in the bind of $m$ with $f$ is equal to the sum of the multiplicities of $a$ in each multiset $f(b)$ for $b \in m$. In symbols: \[ \text{count}(a, \text{bind}(m, f)) = \sum_{b \in m} \text{count}(a, f(b)). \]
Multiset.le_bind theorem
{α β : Type*} {f : α → Multiset β} (S : Multiset α) {x : α} (hx : x ∈ S) : f x ≤ S.bind f
Full source 
theorem le_bind {α β : Type*} {f : α → Multiset β} (S : Multiset α) {x : α} (hx : x ∈ S) :
    f x ≤ S.bind f := by
  classical
  refine le_iff_count.2 fun a ↦ ?_
  obtain ⟨m', hm'⟩ := exists_cons_of_mem <| mem_map_of_mem (fun b ↦ count a (f b)) hx
  rw [count_bind, hm', sum_cons]
  exact Nat.le_add_right _ _
Submultiset Property of Bind Operation: $f(x) \leq \text{bind}(S, f)$ for $x \in S$
Informal description
For any multisets $S$ over a type $\alpha$ and $f : \alpha \to \text{Multiset} \beta$, and for any element $x \in S$, the multiset $f(x)$ is a submultiset of the bind operation $\text{bind}(S, f)$. In other words, $f(x) \leq \text{bind}(S, f)$.
Multiset.attach_bind_coe theorem
(s : Multiset α) (f : α → Multiset β) : (s.attach.bind fun i => f i) = s.bind f
Full source 
@[simp]
theorem attach_bind_coe (s : Multiset α) (f : α → Multiset β) :
    (s.attach.bind fun i => f i) = s.bind f :=
  congr_arg join <| attach_map_val' _ _
Equality of Bind Operations on Attached and Original Multisets
Informal description
For any multiset $s$ over a type $\alpha$ and any function $f : \alpha \to \text{Multiset} \beta$, the bind operation applied to the attached multiset $s.\text{attach}$ (where each element is paired with its proof of membership) yields the same result as applying the bind operation directly to $s$. That is, $$\text{bind}(s.\text{attach}, \lambda i, f(i)) = \text{bind}(s, f).$$
Multiset.nodup_bind theorem
: Nodup (bind s f) ↔ (∀ a ∈ s, Nodup (f a)) ∧ s.Pairwise (Disjoint on f)
Full source 
@[simp] lemma nodup_bind :
    NodupNodup (bind s f) ↔ (∀ a ∈ s, Nodup (f a)) ∧ s.Pairwise (Disjoint on f) := by
  have : ∀ a, ∃ l : List β, f a = l := fun a => Quot.induction_on (f a) fun l => ⟨l, rfl⟩
  choose f' h' using this
  have : f = fun a ↦ ofList (f' a) := funext h'
  have hd : Symmetric fun a b ↦ List.Disjoint (f' a) (f' b) := fun a b h ↦ h.symm
  exact Quot.induction_on s <| by
    unfold Function.onFun
    simp [this, List.nodup_flatMap, pairwise_coe_iff_pairwise hd]
No-Duplicates Condition for Multiset Bind Operation
Informal description
For a multiset $s$ over a type $\alpha$ and a function $f : \alpha \to \text{Multiset} \beta$, the bind operation $\text{bind}(s, f)$ has no duplicates if and only if: 1. For every element $a \in s$, the multiset $f(a)$ has no duplicates, and 2. The multiset $s$ is pairwise disjoint with respect to $f$, meaning that for any two distinct elements $a, b \in s$, the multisets $f(a)$ and $f(b)$ are disjoint.
Multiset.dedup_bind_dedup theorem
[DecidableEq α] [DecidableEq β] (s : Multiset α) (f : α → Multiset β) : (s.dedup.bind f).dedup = (s.bind f).dedup
Full source 
@[simp]
lemma dedup_bind_dedup [DecidableEq α] [DecidableEq β] (s : Multiset α) (f : α → Multiset β) :
    (s.dedup.bind f).dedup = (s.bind f).dedup := by
  ext x
  -- Porting note: was `simp_rw [count_dedup, mem_bind, mem_dedup]`
  simp_rw [count_dedup]
  congr 1
  simp
Deduplication Commutes with Bind Operation on Multisets
Informal description
For any multisets $s$ over a type $\alpha$ and any function $f : \alpha \to \text{Multiset} \beta$, the deduplicated version of the bind operation applied to the deduplicated multiset $s$ is equal to the deduplicated version of the bind operation applied to $s$ itself. That is, $$\operatorname{dedup}(\operatorname{bind}(\operatorname{dedup}(s), f)) = \operatorname{dedup}(\operatorname{bind}(s, f)).$$
Multiset.fold_bind theorem
{ι : Type*} (s : Multiset ι) (t : ι → Multiset α) (b : ι → α) (b₀ : α) : (s.bind t).fold op ((s.map b).fold op b₀) = (s.map fun i => (t i).fold op (b i)).fold op b₀
Full source 
theorem fold_bind {ι : Type*} (s : Multiset ι) (t : ι → Multiset α) (b : ι → α) (b₀ : α) :
    (s.bind t).fold op ((s.map b).fold op b₀) =
    (s.map fun i => (t i).fold op (b i)).fold op b₀ := by
  induction' s using Multiset.induction_on with a ha ih
  · rw [zero_bind, map_zero, map_zero, fold_zero]
  · rw [cons_bind, map_cons, map_cons, fold_cons_left, fold_cons_left, fold_add, ih]
Distributivity of Fold over Bind and Map: $\text{fold}\, *\, (\text{fold}\, *\, b_0\, (\text{map}\, b\, s))\, (\text{bind}\, s\, t) = \text{fold}\, *\, b_0\, (\text{map}\, (\lambda i \mapsto \text{fold}\, *\, (b\, i)\, (t\, i))\, s)$
Informal description
Let $\alpha$ and $\iota$ be types, and let $*$ be a commutative and associative binary operation on $\alpha$. For any multiset $s$ over $\iota$, any function $t : \iota \to \text{Multiset} \alpha$, any function $b : \iota \to \alpha$, and any initial value $b_0 \in \alpha$, the following equality holds: \[ \text{fold}\, *\, \left(\text{fold}\, *\, b_0\, (\text{map}\, b\, s)\right)\, (\text{bind}\, s\, t) = \text{fold}\, *\, b_0\, \left(\text{map}\, (\lambda i \mapsto \text{fold}\, *\, (b\, i)\, (t\, i))\, s\right). \] Here, $\text{bind}\, s\, t$ denotes the union of all multisets $t(i)$ for $i \in s$, and $\text{fold}\, *\, b_0\, s$ denotes the fold of the multiset $s$ with operation $*$ and initial value $b_0$.
Multiset.product definition
(s : Multiset α) (t : Multiset β) : Multiset (α × β)
Full source 
/-- The multiplicity of `(a, b)` in `s ×ˢ t` is
  the product of the multiplicity of `a` in `s` and `b` in `t`. -/
def product (s : Multiset α) (t : Multiset β) : Multiset (α × β) :=
  s.bind fun a => t.map <| Prod.mk a
Cartesian product of multisets
Informal description
Given two multisets $s$ over type $\alpha$ and $t$ over type $\beta$, their Cartesian product $s \times t$ is the multiset over $\alpha \times \beta$ where the multiplicity of each pair $(a, b)$ is the product of the multiplicity of $a$ in $s$ and $b$ in $t$. This is computed by taking the union of all multisets obtained by pairing each element $a$ of $s$ with every element $b$ of $t$.
Multiset.instSProd instance
: SProd (Multiset α) (Multiset β) (Multiset (α × β))
Full source 
instance instSProd : SProd (Multiset α) (Multiset β) (Multiset (α × β)) where
  sprod := Multiset.product
Cartesian Product Operation on Multisets
Informal description
For any types $\alpha$ and $\beta$, the Cartesian product operation $\timesˢ$ is defined on multisets over $\alpha$ and $\beta$, yielding a multiset over $\alpha \times \beta$.
Multiset.coe_product theorem
(l₁ : List α) (l₂ : List β) : (l₁ : Multiset α) ×ˢ (l₂ : Multiset β) = (l₁ ×ˢ l₂)
Full source 
@[simp]
theorem coe_product (l₁ : List α) (l₂ : List β) :
    (l₁ : Multiset α) ×ˢ (l₂ : Multiset β) = (l₁ ×ˢ l₂) := by
  dsimp only [SProd.sprod]
  rw [product, List.product, ← coe_bind]
  simp
Equality of Multiset and List Cartesian Products: $(l₁) \timesˢ (l₂) = (l₁ \timesˢ l₂)$
Informal description
For any lists $l₁$ of elements of type $\alpha$ and $l₂$ of elements of type $\beta$, the Cartesian product of the multisets obtained by coercing $l₁$ and $l₂$ is equal to the multiset obtained by coercing the list Cartesian product of $l₁$ and $l₂$. That is, \[ (l₁ : \text{Multiset} \alpha) \timesˢ (l₂ : \text{Multiset} \beta) = (l₁ \timesˢ l₂ : \text{Multiset} (\alpha \times \beta)). \]
Multiset.zero_product theorem
: (0 : Multiset α) ×ˢ t = 0
Full source 
@[simp]
theorem zero_product : (0 : Multiset α) ×ˢ t = 0 :=
  rfl
Cartesian Product with Empty Multiset Yields Empty Multiset
Informal description
For any multiset $t$ over a type $\beta$, the Cartesian product of the empty multiset (denoted $0$) over a type $\alpha$ with $t$ is the empty multiset, i.e., $0 \timesˢ t = 0$.
Multiset.cons_product theorem
: (a ::ₘ s) ×ˢ t = map (Prod.mk a) t + s ×ˢ t
Full source 
@[simp]
theorem cons_product : (a ::ₘ s) ×ˢ t = map (Prod.mk a) t + s ×ˢ t := by simp [SProd.sprod, product]
Cartesian Product of Multiset Insertion: $(a \cup s) \timesˢ t = \text{map} (a, \cdot)\, t + s \timesˢ t$
Informal description
For any element $a$ of type $\alpha$, any multiset $s$ over $\alpha$, and any multiset $t$ over $\beta$, the Cartesian product of the multiset obtained by inserting $a$ into $s$ with $t$ satisfies: \[ (a \cup s) \timesˢ t = \text{map} (\lambda b \mapsto (a, b))\, t + s \timesˢ t, \] where $a \cup s$ denotes the multiset insertion of $a$ into $s$, $\timesˢ$ denotes the Cartesian product of multisets, and $\text{map}$ applies the pairing with $a$ to each element of $t$.
Multiset.product_zero theorem
: s ×ˢ (0 : Multiset β) = 0
Full source 
@[simp]
theorem product_zero : s ×ˢ (0 : Multiset β) = 0 := by simp [SProd.sprod, product]
Cartesian Product with Empty Multiset Yields Empty Multiset
Informal description
For any multiset $s$ over a type $\alpha$, the Cartesian product of $s$ with the empty multiset (denoted $0$) over a type $\beta$ is the empty multiset, i.e., $s \timesˢ 0 = 0$.
Multiset.product_cons theorem
: s ×ˢ (b ::ₘ t) = (s.map fun a => (a, b)) + s ×ˢ t
Full source 
@[simp]
theorem product_cons : s ×ˢ (b ::ₘ t) = (s.map fun a => (a, b)) + s ×ˢ t := by
  simp [SProd.sprod, product]
Cartesian Product with Multiset Insertion: $s \timesˢ (b \cup t) = \text{map} ((\cdot, b))\, s + s \timesˢ t$
Informal description
For any multiset $s$ over a type $\alpha$, any element $b$ of type $\beta$, and any multiset $t$ over $\beta$, the Cartesian product of $s$ with the multiset obtained by inserting $b$ into $t$ satisfies: \[ s \timesˢ (b \cup t) = \text{map} (\lambda a \mapsto (a, b))\, s + s \timesˢ t, \] where $b \cup t$ denotes the multiset insertion of $b$ into $t$, $\timesˢ$ denotes the Cartesian product of multisets, and $\text{map}$ applies the pairing with $b$ to each element of $s$.
Multiset.product_singleton theorem
: ({ a } : Multiset α) ×ˢ ({ b } : Multiset β) = {(a, b)}
Full source 
@[simp]
theorem product_singleton : ({a} : Multiset α) ×ˢ ({b} : Multiset β) = {(a, b)} := by
  simp only [SProd.sprod, product, bind_singleton, map_singleton]
Cartesian Product of Singleton Multisets: $\{a\} \timesˢ \{b\} = \{(a, b)\}$
Informal description
For any elements $a$ in a type $\alpha$ and $b$ in a type $\beta$, the Cartesian product of the singleton multisets $\{a\}$ and $\{b\}$ is the singleton multiset $\{(a, b)\}$.
Multiset.add_product theorem
(s t : Multiset α) (u : Multiset β) : (s + t) ×ˢ u = s ×ˢ u + t ×ˢ u
Full source 
@[simp]
theorem add_product (s t : Multiset α) (u : Multiset β) : (s + t) ×ˢ u = s ×ˢ u + t ×ˢ u := by
  simp [SProd.sprod, product]
Distributivity of Cartesian Product over Multiset Addition
Informal description
For any multisets $s, t$ over a type $\alpha$ and any multiset $u$ over a type $\beta$, the Cartesian product satisfies: \[ (s + t) \timesˢ u = (s \timesˢ u) + (t \timesˢ u). \]
Multiset.product_add theorem
(s : Multiset α) : ∀ t u : Multiset β, s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
Full source 
@[simp]
theorem product_add (s : Multiset α) : ∀ t u : Multiset β, s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u :=
  Multiset.induction_on s (fun _ _ => rfl) fun a s IH t u => by
    rw [cons_product, IH]
    simp [add_comm, add_left_comm, add_assoc]
Distributivity of Cartesian Product over Multiset Addition (Right)
Informal description
For any multiset $s$ over a type $\alpha$ and any multisets $t, u$ over a type $\beta$, the Cartesian product of $s$ with the sum of $t$ and $u$ satisfies: \[ s \timesˢ (t + u) = (s \timesˢ t) + (s \timesˢ u). \]
Multiset.card_product theorem
: card (s ×ˢ t) = card s * card t
Full source 
@[simp]
theorem card_product : card (s ×ˢ t) = card s * card t := by simp [SProd.sprod, product]
Cardinality of Cartesian Product of Multisets: $|s \times t| = |s| \cdot |t|$
Informal description
For any multisets $s$ over a type $\alpha$ and $t$ over a type $\beta$, the cardinality of their Cartesian product $s \timesˢ t$ is equal to the product of the cardinalities of $s$ and $t$. In symbols: \[ |s \timesˢ t| = |s| \cdot |t| \]
Multiset.mem_product theorem
: ∀ {p : α × β}, p ∈ @product α β s t ↔ p.1 ∈ s ∧ p.2 ∈ t
Full source 
@[simp] lemma mem_product : ∀ {p : α × β}, p ∈ @product α β s tp ∈ @product α β s t ↔ p.1 ∈ s ∧ p.2 ∈ t
  | (a, b) => by simp [product, and_left_comm]
Membership in Cartesian Product of Multisets: $(a, b) \in s \times t \leftrightarrow a \in s \land b \in t$
Informal description
For any pair $p = (a, b)$ in the Cartesian product of types $\alpha \times \beta$, $p$ is an element of the Cartesian product multiset $s \times t$ if and only if $a$ is an element of the multiset $s$ and $b$ is an element of the multiset $t$.
Multiset.Nodup.product theorem
: Nodup s → Nodup t → Nodup (s ×ˢ t)
Full source 
protected theorem Nodup.product : Nodup s → Nodup t → Nodup (s ×ˢ t) :=
  Quotient.inductionOn₂ s t fun l₁ l₂ d₁ d₂ => by simp [List.Nodup.product d₁ d₂]
Cartesian Product Preserves Duplicate-Freeness for Multisets
Informal description
If multisets $s$ over type $\alpha$ and $t$ over type $\beta$ are both duplicate-free (i.e., `Nodup s` and `Nodup t` hold), then their Cartesian product multiset $s \timesˢ t$ is also duplicate-free.
Multiset.sigma definition
(s : Multiset α) (t : ∀ a, Multiset (σ a)) : Multiset (Σ a, σ a)
Full source 
/-- `Multiset.sigma s t` is the dependent version of `Multiset.product`. It is the sum of
  `(a, b)` as `a` ranges over `s` and `b` ranges over `t a`. -/
protected def sigma (s : Multiset α) (t : ∀ a, Multiset (σ a)) : Multiset (Σa, σ a) :=
  s.bind fun a => (t a).map <| Sigma.mk a
Dependent sum of multisets
Informal description
Given a multiset $s$ over a type $\alpha$ and a family of multisets $t(a)$ over types $\sigma(a)$ for each $a \in \alpha$, the sigma operation $\text{sigma}(s, t)$ constructs the multiset of dependent pairs $(a, b)$ where $a$ ranges over $s$ and $b$ ranges over $t(a)$. This is the dependent version of the Cartesian product of multisets.
Multiset.coe_sigma theorem
(l₁ : List α) (l₂ : ∀ a, List (σ a)) : (@Multiset.sigma α σ l₁ fun a => l₂ a) = l₁.sigma l₂
Full source 
@[simp]
theorem coe_sigma (l₁ : List α) (l₂ : ∀ a, List (σ a)) :
    (@Multiset.sigma α σ l₁ fun a => l₂ a) = l₁.sigma l₂ := by
  rw [Multiset.sigma, List.sigma, ← coe_bind]
  simp
Multiset Sigma of Coerced Lists Equals List Sigma Operation
Informal description
For any list $l₁$ of elements of type $\alpha$ and any family of lists $l₂(a)$ of elements of type $\sigma(a)$ for each $a \in \alpha$, the dependent sum of $l₁$ (viewed as a multiset) and $l₂$ (composed with the multiset coercion) is equal to the list sigma operation applied to $l₁$ and $l₂$, i.e., $\text{sigma}(l₁, l₂) = l₁.\text{sigma}\ l₂$.
Multiset.zero_sigma theorem
: @Multiset.sigma α σ 0 t = 0
Full source 
@[simp]
theorem zero_sigma : @Multiset.sigma α σ 0 t = 0 :=
  rfl
Empty Multiset Sigma Property: $\text{sigma}(0, t) = 0$
Informal description
For any family of multisets $t(a)$ indexed by elements of type $\alpha$, the dependent sum of the empty multiset $0$ with $t$ is equal to the empty multiset $0$, i.e., $\text{sigma}(0, t) = 0$.
Multiset.cons_sigma theorem
: (a ::ₘ s).sigma t = (t a).map (Sigma.mk a) + s.sigma t
Full source 
@[simp]
theorem cons_sigma : (a ::ₘ s).sigma t = (t a).map (Sigma.mk a) + s.sigma t := by
  simp [Multiset.sigma]
Dependent Sum of Multiset Insertion: $\text{sigma}(a \cup s, t) = \text{map}(\Sigma.\text{mk}\ a, t(a)) + \text{sigma}(s, t)$
Informal description
For any element $a$ of type $\alpha$, any multiset $s$ over $\alpha$, and any family of multisets $t(a)$ over types $\sigma(a)$ for each $a \in \alpha$, the dependent sum operation satisfies: \[ \text{sigma}(a \cup s, t) = \text{map}(\Sigma.\text{mk}\ a, t(a)) + \text{sigma}(s, t), \] where $a \cup s$ denotes the multiset obtained by inserting $a$ into $s$, and $\Sigma.\text{mk}\ a$ is the constructor for dependent pairs.
Multiset.sigma_singleton theorem
(b : α → β) : (({ a } : Multiset α).sigma fun a => ({b a} : Multiset β)) = {⟨a, b a⟩}
Full source 
@[simp]
theorem sigma_singleton (b : α → β) :
    (({a} : Multiset α).sigma fun a => ({b a} : Multiset β)) = {⟨a, b a⟩} :=
  rfl
Singleton Sigma Property: $\text{sigma}(\{a\}, \lambda a. \{b(a)\}) = \{\langle a, b(a) \rangle\}$
Informal description
Given a singleton multiset $\{a\}$ over a type $\alpha$ and a function $b : \alpha \to \beta$, the dependent sum of $\{a\}$ with the family of singleton multisets $\{b(a)\}$ is equal to the singleton multiset $\{\langle a, b(a) \rangle\}$.
Multiset.add_sigma theorem
(s t : Multiset α) (u : ∀ a, Multiset (σ a)) : (s + t).sigma u = s.sigma u + t.sigma u
Full source 
@[simp]
theorem add_sigma (s t : Multiset α) (u : ∀ a, Multiset (σ a)) :
    (s + t).sigma u = s.sigma u + t.sigma u := by simp [Multiset.sigma]
Additivity of Dependent Sum Operation on Multisets
Informal description
For any multisets $s$ and $t$ over a type $\alpha$ and any family of multisets $u(a)$ over types $\sigma(a)$ for each $a \in \alpha$, the dependent sum operation satisfies: \[ (s + t).\sigma u = s.\sigma u + t.\sigma u. \]
Multiset.sigma_add theorem
: ∀ t u : ∀ a, Multiset (σ a), (s.sigma fun a => t a + u a) = s.sigma t + s.sigma u
Full source 
@[simp]
theorem sigma_add :
    ∀ t u : ∀ a, Multiset (σ a), (s.sigma fun a => t a + u a) = s.sigma t + s.sigma u :=
  Multiset.induction_on s (fun _ _ => rfl) fun a s IH t u => by
    rw [cons_sigma, IH]
    simp [add_comm, add_left_comm, add_assoc]
Distributivity of Dependent Sum over Multiset Addition
Informal description
For any family of multisets $t(a)$ and $u(a)$ over types $\sigma(a)$ for each $a \in \alpha$, the dependent sum operation on a multiset $s$ satisfies: \[ \text{sigma}(s, \lambda a.\, t(a) + u(a)) = \text{sigma}(s, t) + \text{sigma}(s, u). \]
Multiset.card_sigma theorem
: card (s.sigma t) = sum (map (fun a => card (t a)) s)
Full source 
@[simp]
theorem card_sigma : card (s.sigma t) = sum (map (fun a => card (t a)) s) := by
  simp [Multiset.sigma, (· ∘ ·)]
Cardinality of Dependent Sum of Multisets Equals Sum of Cardinalities
Informal description
For any multiset $s$ over a type $\alpha$ and any family of multisets $t(a)$ over types $\sigma(a)$ for each $a \in \alpha$, the cardinality of the dependent sum multiset $\text{sigma}(s, t)$ is equal to the sum of the cardinalities of the multisets $t(a)$ for each $a \in s$. In symbols: \[ |\text{sigma}(s, t)| = \sum_{a \in s} |t(a)| \]
Multiset.mem_sigma theorem
: ∀ {p : Σ a, σ a}, p ∈ @Multiset.sigma α σ s t ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
Full source 
@[simp] lemma mem_sigma : ∀ {p : Σa, σ a}, p ∈ @Multiset.sigma α σ s tp ∈ @Multiset.sigma α σ s t ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
  | ⟨a, b⟩ => by simp [Multiset.sigma, and_assoc, and_left_comm]
Membership Criterion for Multiset Sigma Construction
Informal description
For any dependent pair $p = (a, b)$ in the sigma type $\Sigma a, \sigma a$, $p$ is an element of the multiset sigma construction $\text{sigma}(s, t)$ if and only if $a$ is an element of the multiset $s$ and $b$ is an element of the multiset $t(a)$.
Multiset.Nodup.sigma theorem
{σ : α → Type*} {t : ∀ a, Multiset (σ a)} : Nodup s → (∀ a, Nodup (t a)) → Nodup (s.sigma t)
Full source 
protected theorem Nodup.sigma {σ : α → Type*} {t : ∀ a, Multiset (σ a)} :
    Nodup s → (∀ a, Nodup (t a)) → Nodup (s.sigma t) :=
  Quot.induction_on s fun l₁ => by
    choose f hf using fun a => Quotient.exists_rep (t a)
    simpa [← funext hf] using List.Nodup.sigma
Preservation of Distinctness in Dependent Sum of Multisets
Informal description
Let $\alpha$ be a type and $\sigma : \alpha \to \text{Type}$ be a family of types. Given a multiset $s$ over $\alpha$ and a family of multisets $t(a)$ over $\sigma(a)$ for each $a \in \alpha$, if $s$ has no duplicates and each $t(a)$ has no duplicates, then the dependent sum multiset $\text{sigma}(s, t)$ also has no duplicates.