∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
  [OrderClosedTopology α] [PreconnectedSpace X] {a : X} {l : Filter X} [l.NeBot] {f g : X → α},
  Continuous f → Continuous g → f a ≤ g a → g ≤ᶠ[l] f → ∃ x, f x = g x