∀ {α : Type u_1} {β : Type u_2} {f : Filter α} [inst : ConditionallyCompleteLinearOrder β] {u : α → β} {b : β},
  b < Filter.liminf u f →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) Filter.eventually_lt_of_lt_liminf._auto_1 →
      ∀ᶠ (a : α) in f, b < u a