no goals
α : Type u_2
β : Type u_1
γ : Type ?u.20058
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
x✝ : α × β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ t ↔ (x, y) ∈ Finset.biUnion t fun b => image (fun a => (a, b)) s
simp only [mem_product, mem_biUnion, mem_image, exists_prop, Prod.mk.inj_iff, and_left_comm,
  exists_and_left, exists_eq_right, exists_eq_left]