no goals
α : Type u_1
β : Type u_2
γ : Type ?u.68091
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
s : Finset α
t : Finset β
⊢ s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅
rw [← not_nonempty_iff_eq_empty, nonempty_product, not_and_or, not_nonempty_iff_eq_empty,
  not_nonempty_iff_eq_empty]