no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
hs : Set.Finite s
ht : Set.Finite t
⊢ ∀ (a : α × β), a ∈ Finite.toFinset hs ×ˢ Finite.toFinset ht ↔ a ∈ Finite.toFinset (_ : Set.Finite (s ×ˢ t))
simp