ι : Type ?u.24415
ι' : Type ?u.24418
α✝ : Type ?u.24421
β : Type ?u.24424
γ : Type ?u.24427
α : Type u_1
inst✝¹ : Subsingleton α
inst✝ : Preorder α
s : Set α
hs : s ∈ atTop
x : α
⊢ x ∈ s
ι : Type ?u.24415
ι' : Type ?u.24418
α✝ : Type ?u.24421
β : Type ?u.24424
γ : Type ?u.24427
α : Type u_1
inst✝¹ : Subsingleton α
inst✝ : Preorder α
⊢ atTop = ⊤
refine' top_unique fun s hs x => _
ι : Type ?u.24415
ι' : Type ?u.24418
α✝ : Type ?u.24421
β : Type ?u.24424
γ : Type ?u.24427
α : Type u_1
inst✝¹ : Subsingleton α
inst✝ : Preorder α
s : Set α
x : α
hs : Ici x ⊆ s
⊢ x ∈ s
ι : Type ?u.24415
ι' : Type ?u.24418
α✝ : Type ?u.24421
β : Type ?u.24424
γ : Type ?u.24427
α : Type u_1
inst✝¹ : Subsingleton α
inst✝ : Preorder α
s : Set α
hs : s ∈ atTop
x : α
⊢ x ∈ s
rw [atTop, ciInf_subsingleton x, mem_principal] at hs
no goals
ι : Type ?u.24415
ι' : Type ?u.24418
α✝ : Type ?u.24421
β : Type ?u.24424
γ : Type ?u.24427
α : Type u_1
inst✝¹ : Subsingleton α
inst✝ : Preorder α
s : Set α
x : α
hs : Ici x ⊆ s
⊢ x ∈ s
exact hs left_mem_Ici