case h
α : Type u_1
β : Type ?u.126298
γ : Type ?u.126301
ι : Sort ?u.126304
κ : ι → Sort ?u.126309
inst✝¹ : Preorder α
inst✝ : Preorder β
s✝ t : Set α
x : α
s : Set α
x✝ : α
⊢ x✝ ∈ ↑(lowerClosure s) ↔ x✝ ∈ ⋃ (a : α) (_ : a ∈ s), Iic a
α : Type u_1
β : Type ?u.126298
γ : Type ?u.126301
ι : Sort ?u.126304
κ : ι → Sort ?u.126309
inst✝¹ : Preorder α
inst✝ : Preorder β
s✝ t : Set α
x : α
s : Set α
⊢ ↑(lowerClosure s) = ⋃ (a : α) (_ : a ∈ s), Iic a
ext
no goals
case h
α : Type u_1
β : Type ?u.126298
γ : Type ?u.126301
ι : Sort ?u.126304
κ : ι → Sort ?u.126309
inst✝¹ : Preorder α
inst✝ : Preorder β
s✝ t : Set α
x : α
s : Set α
x✝ : α
⊢ x✝ ∈ ↑(lowerClosure s) ↔ x✝ ∈ ⋃ (a : α) (_ : a ∈ s), Iic a
simp