α : Type u_1
β : Type ?u.56847
β₂ : Type ?u.56850
γ : Type ?u.56853
ι : Sort ?u.56856
ι' : Sort ?u.56859
κ : ι → Sort ?u.56864
κ' : ι' → Sort ?u.56869
inst✝ : CompleteLattice α
s✝ t : Set α
a b : α
s : Set α
h_sup : sSup s = ⊥
hne : Set.Nonempty s
⊢ Set.Nonempty s ∧ ∀ (x : α), x ∈ s → x = ⊥
α : Type u_1
β : Type ?u.56847
β₂ : Type ?u.56850
γ : Type ?u.56853
ι : Sort ?u.56856
ι' : Sort ?u.56859
κ : ι → Sort ?u.56864
κ' : ι' → Sort ?u.56869
inst✝ : CompleteLattice α
s✝ t : Set α
a b : α
s : Set α
h_sup : sSup s = ⊥
hne : Set.Nonempty s
⊢ s = {⊥}
rw [Set.eq_singleton_iff_nonempty_unique_mem]
α : Type u_1
β : Type ?u.56847
β₂ : Type ?u.56850
γ : Type ?u.56853
ι : Sort ?u.56856
ι' : Sort ?u.56859
κ : ι → Sort ?u.56864
κ' : ι' → Sort ?u.56869
inst✝ : CompleteLattice α
s✝ t : Set α
a b : α
s : Set α
h_sup : ∀ (a : α), a ∈ s → a = ⊥
hne : Set.Nonempty s
⊢ Set.Nonempty s ∧ ∀ (x : α), x ∈ s → x = ⊥
α : Type u_1
β : Type ?u.56847
β₂ : Type ?u.56850
γ : Type ?u.56853
ι : Sort ?u.56856
ι' : Sort ?u.56859
κ : ι → Sort ?u.56864
κ' : ι' → Sort ?u.56869
inst✝ : CompleteLattice α
s✝ t : Set α
a b : α
s : Set α
h_sup : sSup s = ⊥
hne : Set.Nonempty s
⊢ Set.Nonempty s ∧ ∀ (x : α), x ∈ s → x = ⊥
rw [sSup_eq_bot] at h_sup
no goals
α : Type u_1
β : Type ?u.56847
β₂ : Type ?u.56850
γ : Type ?u.56853
ι : Sort ?u.56856
ι' : Sort ?u.56859
κ : ι → Sort ?u.56864
κ' : ι' → Sort ?u.56869
inst✝ : CompleteLattice α
s✝ t : Set α
a b : α
s : Set α
h_sup : ∀ (a : α), a ∈ s → a = ⊥
hne : Set.Nonempty s
⊢ Set.Nonempty s ∧ ∀ (x : α), x ∈ s → x = ⊥
exact ⟨hne, h_sup⟩