no goals
α : Type u_1
β : Type ?u.73832
γ : Type ?u.73835
δ : Type ?u.73838
σ : α → Type u_2
a✝ : α
s✝ : Multiset α
t✝ : (a : α) → Multiset (σ a)
s : Multiset α
t : (a : α) → Multiset (σ a)
a : α
b : σ a
⊢ { fst := a, snd := b } ∈ Multiset.sigma s t ↔
    { fst := a, snd := b }.fst ∈ s ∧ { fst := a, snd := b }.snd ∈ t { fst := a, snd := b }.fst
simp [Multiset.sigma, and_assoc, and_left_comm]