no goals
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
a : α
b : β
⊢ (a, b) ∈ l₁ ×ˢ l₂ ↔ a ∈ l₁ ∧ b ∈ l₂
simp_all [SProd.sprod, product, mem_bind, mem_map, Prod.ext_iff, exists_prop, and_left_comm,
  exists_and_left, exists_eq_left, exists_eq_right]