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