no goals
α : Type u_2
β : Type u_1
γ : Type ?u.54283
ι : Type ?u.54286
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
⊢ (blimsup u f fun x => True) = limsup u f
simp [blimsup_eq, limsup_eq]