no goals
α : Type u_1
β : Type u_2
γ : Type ?u.14121
δ : Type ?u.14124
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂
simp_rw [disjoint_left, mem_prod, not_and_or, Prod.forall, and_imp, ← @forall_or_right α, ←
  @forall_or_left β, ← @forall_or_right (_ ∈ s₁), ← @forall_or_left (_ ∈ t₁)]