no goals
α : Type u_1
β : Type u_2
γ : Type ?u.71755
s s' : Finset α
t t' : Finset β
a✝ : α
b✝ : β
a : α
b : β
⊢ {a} ×ˢ {b} = {(a, b)}
simp only [product_singleton, Function.Embedding.coeFn_mk, map_singleton]