integrableOn_exp_sub_one_div

lemma integrableOn_exp_sub_one_div {y : ℝ} (hy : 0 < y) :    IntegrableOn (fun u => (exp u - 1) / u) (Ioc 0 y) := by  -- Since $(Real.exp u - 1) / u$ is bounded on $(0, y]$, we can apply the Integrable.mono' lemma.  have h_bounded : ∀ u ∈ Set.Ioc 0 y, |(Real.exp u - 1) / u| ≤ Real.exp y := by    norm_num [ abs_div ];    intro u hu huy; rw [ abs_of_nonneg ( sub_nonneg_of_le ( Real.one_le_exp hu.le ) ), abs_of_nonneg hu.le ] ; rw [ div_le_iff₀ hu ] ; nlinarith [ Real.exp_pos u, Real.exp_le_exp.2 huy, Real.exp_neg u, mul_inv_cancel₀ ( ne_of_gt ( Real.exp_pos u ) ), Real.add_one_le_exp u, Real.add_one_le_exp ( -u ) ] ;  refine' MeasureTheory.Integrable.mono' _ _ _;  exacts [ fun u => Real.exp y, by norm_num, by exact Measurable.aestronglyMeasurable ( by exact Measurable.div ( Real.continuous_exp.measurable.sub measurable_const ) measurable_id' ), Filter.eventually_of_mem ( MeasureTheory.ae_restrict_mem measurableSet_Ioc ) fun u hu => h_bounded u hu ]