α : Type u_1
β : Type u_2
γ : Type ?u.176896
ι : Type ?u.176899
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ (a \ liminf u f)ᶜ = limsup (fun b => a \ u b) fᶜ
α : Type u_1
β : Type u_2
γ : Type ?u.176896
ι : Type ?u.176899
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ a \ liminf u f = limsup (fun b => a \ u b) f
rw [← compl_inj_iff]