no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
⊢ Set.Finite (s ×ˢ t) ↔ (Set.Finite s ∨ t = ∅) ∧ (Set.Finite t ∨ s = ∅)
simp only [← not_infinite, Set.infinite_prod, not_or, not_and_or, not_nonempty_iff_eq_empty]