case a.h
α : Type u_1
β : Type u_2
γ : Type ?u.195438
ι : Sort ?u.195441
κ : ι → Sort ?u.195446
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
x✝ : α × β
⊢ x✝ ∈ ↑(lowerClosure (s ×ˢ t)) ↔ x✝ ∈ ↑(lowerClosure s ×ˢ lowerClosure t)
α : Type u_1
β : Type u_2
γ : Type ?u.195438
ι : Sort ?u.195441
κ : ι → Sort ?u.195446
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
⊢ lowerClosure (s ×ˢ t) = lowerClosure s ×ˢ lowerClosure t
ext
no goals
case a.h
α : Type u_1
β : Type u_2
γ : Type ?u.195438
ι : Sort ?u.195441
κ : ι → Sort ?u.195446
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
x✝ : α × β
⊢ x✝ ∈ ↑(lowerClosure (s ×ˢ t)) ↔ x✝ ∈ ↑(lowerClosure s ×ˢ lowerClosure t)
simp [Prod.le_def, @and_and_and_comm _ (_ ∈ t)]