α : Type u_1
β : Type u_2
γ : Type ?u.176800
ι : Sort ?u.176803
κ : ι → Sort ?u.176808
inst✝¹ : Preorder α
inst✝ : Preorder β
s s₁ s₂ : UpperSet α
t t₁ t₂ : UpperSet β
x : α × β
⊢ ↑(s ×ˢ t) = ↑⊤ ↔ ↑s = ↑⊤ ∨ ↑t = ↑⊤
α : Type u_1
β : Type u_2
γ : Type ?u.176800
ι : Sort ?u.176803
κ : ι → Sort ?u.176808
inst✝¹ : Preorder α
inst✝ : Preorder β
s s₁ s₂ : UpperSet α
t t₁ t₂ : UpperSet β
x : α × β
⊢ s ×ˢ t = ⊤ ↔ s = ⊤ ∨ t = ⊤
simp_rw [SetLike.ext'_iff]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.176800
ι : Sort ?u.176803
κ : ι → Sort ?u.176808
inst✝¹ : Preorder α
inst✝ : Preorder β
s s₁ s₂ : UpperSet α
t t₁ t₂ : UpperSet β
x : α × β
⊢ ↑(s ×ˢ t) = ↑⊤ ↔ ↑s = ↑⊤ ∨ ↑t = ↑⊤
exact prod_eq_empty_iff