∀ {α : Type u} {β : Type v} [inst : TopologicalSpace β] [inst_1 : Preorder β] [inst_2 : OrderBot β] [OrderTopology β]
  {l : Filter α} {f g : α → β}, Filter.Tendsto f l (nhds ⊥) → g ≤ᶠ[l] f → Filter.Tendsto g l (nhds ⊥)