no goals
α : Type u_2
β : Type u_1
γ : Type ?u.175653
ι : Type ?u.175656
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : NeBot f
a : α
⊢ liminf u f \ a = liminf (fun b => u b \ a) f
simp only [sdiff_eq, inf_comm (b := aᶜ), inf_liminf]