α : Type u
β : Type v
γ : Type w
δ : Type ?u.91776
ι : Sort x
f g : Filter α
s✝ t : Set α
inst✝¹ : Subsingleton α
l : Filter α
inst✝ : NeBot l
s : Set α
hs : s ∈ l
⊢ s ∈ ⊤
α : Type u
β : Type v
γ : Type w
δ : Type ?u.91776
ι : Sort x
f g : Filter α
s t : Set α
inst✝¹ : Subsingleton α
l : Filter α
inst✝ : NeBot l
⊢ l = ⊤
refine' top_unique fun s hs => _
α : Type u
β : Type v
γ : Type w
δ : Type ?u.91776
ι : Sort x
f g : Filter α
s✝ t : Set α
inst✝¹ : Subsingleton α
l : Filter α
inst✝ : NeBot l
s : Set α
hs : s ∈ l
⊢ s = univ

α : Type u
β : Type v
γ : Type w
δ : Type ?u.91776
ι : Sort x
f g : Filter α
s t : Set α
inst✝¹ : Subsingleton α
l : Filter α
inst✝ : NeBot l
hs : univ ∈ l
⊢ univ ∈ ⊤
α : Type u
β : Type v
γ : Type w
δ : Type ?u.91776
ι : Sort x
f g : Filter α
s✝ t : Set α
inst✝¹ : Subsingleton α
l : Filter α
inst✝ : NeBot l
s : Set α
hs : s ∈ l
⊢ s ∈ ⊤
obtain rfl : s = univ
α : Type u
β : Type v
γ : Type w
δ : Type ?u.91776
ι : Sort x
f g : Filter α
s t : Set α
inst✝¹ : Subsingleton α
l : Filter α
inst✝ : NeBot l
hs : univ ∈ l
⊢ univ ∈ ⊤
α : Type u
β : Type v
γ : Type w
δ : Type ?u.91776
ι : Sort x
f g : Filter α
s✝ t : Set α
inst✝¹ : Subsingleton α
l : Filter α
inst✝ : NeBot l
s : Set α
hs : s ∈ l
⊢ s = univ

α : Type u
β : Type v
γ : Type w
δ : Type ?u.91776
ι : Sort x
f g : Filter α
s t : Set α
inst✝¹ : Subsingleton α
l : Filter α
inst✝ : NeBot l
hs : univ ∈ l
⊢ univ ∈ ⊤
exact Subsingleton.eq_univ_of_nonempty (nonempty_of_mem hs)
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.91776
ι : Sort x
f g : Filter α
s t : Set α
inst✝¹ : Subsingleton α
l : Filter α
inst✝ : NeBot l
hs : univ ∈ l
⊢ univ ∈ ⊤
exact univ_mem