no goals
α : Type u_1
β : Type u_2
γ : Type ?u.189730
ι : Sort ?u.189733
κ : ι → Sort ?u.189738
inst✝¹ : Preorder α
inst✝ : Preorder β
s s₁ s₂ : LowerSet α
t t₁ t₂ : LowerSet β
x : α × β
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂
simp_rw [disjoint_iff, prod_inf_prod, prod_eq_bot]