no goals
α : Type u_1
β : Type ?u.182390
γ : Type ?u.182393
ι : Type u_2
p : ι → Prop
s : ι → Set α
⊢ limsup s cofinite = {x | Set.Infinite {n | x ∈ s n}}
simp only [← cofinite.blimsup_true s, cofinite.blimsup_set_eq, true_and_iff]