no goals
α✝ : Type ?u.82278
β : Type u_2
γ : Type ?u.82284
ι : Type ?u.82287
inst✝² : ConditionallyCompleteLattice α✝
α : Type u_1
inst✝¹ : ConditionallyCompleteLattice β
f : Filter α
inst✝ : NeBot f
b : β
⊢ limsup (fun x => b) f = b
simpa only [limsup_eq, eventually_const] using csInf_Ici