no goals
α : Type u_1
β : Type u_2
γ : Type ?u.175540
ι : Sort ?u.175543
κ : ι → Sort ?u.175548
inst✝¹ : Preorder α
inst✝ : Preorder β
s s₁ s₂ : UpperSet α
t t₁ t₂ : UpperSet β
x : α × β
⊢ ↑s₂ ⊆ ↑s₁ ∧ ↑t₂ ⊆ ↑t₁ ∨ ↑s₂ = ∅ ∨ ↑t₂ = ∅ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₂ = ⊤ ∨ t₂ = ⊤
simp