no goals
α : Type u_1
β : Type u_2
γ : Type ?u.1583
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝ : DecidableEq α
i : α
⊢ i ∈ image Prod.fst (s ×ˢ t) → i ∈ s
simp (config := { contextual := true }) [mem_image]