∀ {X : Type u_1} {Y : Type u_2} [inst : ConditionallyCompleteLinearOrder X] [DenselyOrdered X]
  [inst_2 : TopologicalSpace X] [OrderTopology X] [inst_4 : LinearOrder Y] [inst_5 : TopologicalSpace Y]
  [OrderTopology Y] {f : X → Y} {a b : X} {l : Y},
  a < b →
    ContinuousOn f (Set.Ioo a b) →
      Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds l) →
        Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds l) → ∃ c ∈ Set.Ioo a b, IsLocalExtr f c