From a.e. differentiability on ℝ to a statement about a path indexed by NNReal

To use Mathlib's Lebesgue theorem MonotoneOn.ae_differentiableWithinAt (f : ℝ → ℝ) for a path B : NNReal → ℝ, set f x := B x.toNNReal and transfer monotonicity with Real.toNNReal_le_toNNReal and Real.coe_toNNReal. To extract a point, make NeBot (ae (volume.restrict (Ioo a b))) with ae_neBot.2 (by simp [Measure.restrict_eq_zero, hab]), where hab is the NNReal fact a < b; simp reduces the goal to that, not to its real cast. Then call .exists on (… .ae_differentiableWithinAt measurableSet_Ioo).and (ae_restrict_mem measurableSet_Ioo). On an open set, hd.differentiableAt (isOpen_Ioo.mem_nhds hx). hasDerivWithinAt_iff_tendsto_slope gives 𝓝[Ioi x \ {x}] x; prove Ioi x \ {x} = Ioi x by ext, because rewriting with sdiff_singleton_eq_self failed to match. Compose with coe : NNReal → ℝ via tendsto_nhdsWithin_iff (continuity plus eventually_nhdsWithin_of_forall with NNReal.coe_lt_coe), then .congr with simp [slope, Real.toNNReal_coe].