case a.h
α : Type u_1
β : Type ?u.158776
γ : Type ?u.158779
ι : Sort ?u.158782
κ : ι → Sort ?u.158787
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
x a x✝ : α
⊢ x✝ ∈ ↑(lowerClosure {a}) ↔ x✝ ∈ ↑(LowerSet.Iic a)
α : Type u_1
β : Type ?u.158776
γ : Type ?u.158779
ι : Sort ?u.158782
κ : ι → Sort ?u.158787
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
x a : α
⊢ lowerClosure {a} = LowerSet.Iic a
ext
no goals
case a.h
α : Type u_1
β : Type ?u.158776
γ : Type ?u.158779
ι : Sort ?u.158782
κ : ι → Sort ?u.158787
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
x a x✝ : α
⊢ x✝ ∈ ↑(lowerClosure {a}) ↔ x✝ ∈ ↑(LowerSet.Iic a)
simp