α : Type u_1
β : Type ?u.85338
γ : Type ?u.85341
ι : Type ?u.85344
inst✝ : CompleteLattice α
⊢ ∀ (b : α), (∀ (x : α), x ≤ b) → b = ⊤
α : Type u_1
β : Type ?u.85338
γ : Type ?u.85341
ι : Type ?u.85344
inst✝ : CompleteLattice α
⊢ ∀ (b : α), b ∈ {a | ∀ᶠ (n : α) in ⊤, n ≤ a} → ⊤ ≤ b
simp [eq_univ_iff_forall]
no goals
α : Type u_1
β : Type ?u.85338
γ : Type ?u.85341
ι : Type ?u.85344
inst✝ : CompleteLattice α
⊢ ∀ (b : α), (∀ (x : α), x ≤ b) → b = ⊤
exact fun b hb => top_unique <| hb _