no goals
α : Type u_1
β : Type u_2
γ : Type ?u.62033
δ : Type ?u.62036
a✝ : α
b✝ : β
s✝ : Multiset α
t✝ : Multiset β
s : Multiset α
t : Multiset β
a : α
b : β
⊢ (a, b) ∈ product s t ↔ (a, b).fst ∈ s ∧ (a, b).snd ∈ t
simp [product, and_left_comm]