∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f f' : ℝ → F} {d b η : ℝ},
  d ≤ b →
    (∀ᵐ (x : ℝ), x ∈ Set.Ioo d b → HasDerivAt f (f' x) x) →
      0 < η →
        ∃ u,
          (∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η) ∧
            (u.PairwiseDisjoint fun z => Set.Icc z.1 z.2) ∧ HasSum (fun z => (↑z).2 - (↑z).1) (b - d)