Multiset.mem_disjSum

theorem Multiset.mem_disjSum : ∀ {α : Type u_1} {β : Type u_2} {s : Multiset α} {t : Multiset β} {x : α ⊕ β}, x ∈ s.disjSum t ↔ (∃ a ∈ s, Sum.inl a = x) ∨ ∃ b ∈ t, Sum.inr b = x

The theorem `Multiset.mem_disjSum` states that for any types `α` and `β`, multisets `s` of type `α` and `t` of type `β`, and element `x` of the disjoint sum type `α ⊕ β`, `x` is in the disjoint sum of `s` and `t` if and only if `x` is the left injection `Sum.inl a` of some element `a` in `s` or the right injection `Sum.inr b` of some element `b` in `t`. In other words, an element is in the disjoint sum of two multisets if it comes from one of the two multisets, being tagged accordingly to differentiate between the two original sets.

More concisely: For any multisets $s$ of type $\alpha$ and $t$ of type $\beta$, and any $x$ in the disjoint sum $\alpha \oplus \beta$, $x$ is in the multiset union of $s$ and $t$ if and only if $x$ is the injection of some element in $s$ or the injection of some element in $t$.