no goals
α : Type u_1
β : Type u_2
γ : Type ?u.171159
ι : Type ?u.171162
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
⊢ liminf u fᶜ = limsup (compl ∘ u) f
simp only [limsup_eq_iInf_iSup, compl_iInf, compl_iSup, liminf_eq_iSup_iInf, Function.comp_apply]