An integrability lemma

theorem MeasureTheory.integrable_f_rnDeriv_of_derivAtTop_ne_top {α : Type u_1} {mα : MeasurableSpace α} {f : ℝ → ℝ} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hf : MeasureTheory.StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_deriv : derivAtTop f ≠ ⊤) : MeasureTheory.Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν