case inl
ι : Type ?u.270965
ι' : Type ?u.270968
α : Type u_1
β : Type u_2
γ : Type ?u.270977
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝ : IsEmpty α
⊢ atTop ×ˢ atTop = atTop

case inr
ι : Type ?u.270965
ι' : Type ?u.270968
α : Type u_1
β : Type u_2
γ : Type ?u.270977
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝ : Nonempty α
⊢ atTop ×ˢ atTop = atTop
ι : Type ?u.270965
ι' : Type ?u.270968
α : Type u_1
β : Type u_2
γ : Type ?u.270977
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ atTop ×ˢ atTop = atTop
cases isEmpty_or_nonempty α
case inr
ι : Type ?u.270965
ι' : Type ?u.270968
α : Type u_1
β : Type u_2
γ : Type ?u.270977
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝ : Nonempty α
⊢ atTop ×ˢ atTop = atTop
case inl
ι : Type ?u.270965
ι' : Type ?u.270968
α : Type u_1
β : Type u_2
γ : Type ?u.270977
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝ : IsEmpty α
⊢ atTop ×ˢ atTop = atTop

case inr
ι : Type ?u.270965
ι' : Type ?u.270968
α : Type u_1
β : Type u_2
γ : Type ?u.270977
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝ : Nonempty α
⊢ atTop ×ˢ atTop = atTop
exact Subsingleton.elim _ _
case inr.inl
ι : Type ?u.270965
ι' : Type ?u.270968
α : Type u_1
β : Type u_2
γ : Type ?u.270977
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ atTop ×ˢ atTop = atTop

case inr.inr
ι : Type ?u.270965
ι' : Type ?u.270968
α : Type u_1
β : Type u_2
γ : Type ?u.270977
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ atTop ×ˢ atTop = atTop
case inr
ι : Type ?u.270965
ι' : Type ?u.270968
α : Type u_1
β : Type u_2
γ : Type ?u.270977
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝ : Nonempty α
⊢ atTop ×ˢ atTop = atTop
cases isEmpty_or_nonempty β
case inr.inr
ι : Type ?u.270965
ι' : Type ?u.270968
α : Type u_1
β : Type u_2
γ : Type ?u.270977
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ atTop ×ˢ atTop = atTop
case inr.inl
ι : Type ?u.270965
ι' : Type ?u.270968
α : Type u_1
β : Type u_2
γ : Type ?u.270977
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ atTop ×ˢ atTop = atTop

case inr.inr
ι : Type ?u.270965
ι' : Type ?u.270968
α : Type u_1
β : Type u_2
γ : Type ?u.270977
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ atTop ×ˢ atTop = atTop
exact Subsingleton.elim _ _
no goals
case inr.inr
ι : Type ?u.270965
ι' : Type ?u.270968
α : Type u_1
β : Type u_2
γ : Type ?u.270977
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ atTop ×ˢ atTop = atTop
simpa [atTop, prod_iInf_left, prod_iInf_right, iInf_prod] using iInf_comm