no goals
α : Type u_1
β : Type u_2
γ : Type ?u.77766
s s' : Finset α
t t' : Finset β
a : α
b : β
⊢ _root_.Disjoint (s ×ˢ t) (s' ×ˢ t') ↔ _root_.Disjoint s s' ∨ _root_.Disjoint t t'
simp_rw [← disjoint_coe, coe_product, Set.disjoint_prod]