no goals
α : Type u_1
β : Type u_2
γ : Type ?u.177622
ι : Sort ?u.177625
κ : ι → Sort ?u.177630
inst✝¹ : Preorder α
inst✝ : Preorder β
s s₁ s₂ : UpperSet α
t t₁ t₂ : UpperSet β
x : α × β
⊢ Codisjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Codisjoint s₁ s₂ ∨ Codisjoint t₁ t₂
simp_rw [codisjoint_iff, prod_sup_prod, prod_eq_top]