∀ {α : Type u_1} {f : Filter α} [inst : ConditionallyCompleteLinearOrder α] {a : α},
  autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) f) Filter.frequently_lt_of_lt_limsSup._auto_1 →
    a < f.limsSup → ∃ᶠ (n : α) in f, a < n