no goals
α : Type u_1
β : Type u_2
xs : List α
ys : List β
x : α
y : β
⊢ (x, y) ∈ product xs ys ↔ x ∈ xs ∧ y ∈ ys
simp only [product, and_imp, exists_prop, mem_map, Prod.mk.injEq,
  exists_eq_right_right, mem_bind, iff_self]