no goals
α : Type u_1
β : Type ?u.182852
γ : Type ?u.182855
ι : Type u_2
p : ι → Prop
s : ι → Set α
⊢ liminf s cofinite = {x | Set.Finite {n | ¬x ∈ s n}}
simp only [← cofinite.bliminf_true s, cofinite.bliminf_set_eq, true_and_iff]