no goals
α : Type u_1
β : Type u_2
γ : Type ?u.79454
δ : Type ?u.79457
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅
simp only [not_nonempty_iff_eq_empty.symm, prod_nonempty_iff, not_and_or]