∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (f : ℝ → F) [CompleteSpace F]
  [inst_3 : MeasurableSpace F] [BorelSpace F] (μ : MeasureTheory.Measure ℝ),
  AEMeasurable (fun x => derivWithin f (Set.Ici x) x) μ