integrableOn_one_sub_exp_neg_div

lemma integrableOn_one_sub_exp_neg_div :    IntegrableOn (fun t => (1 - exp (-t)) / t) (Ioc 0 1) := by  -- We'll use the fact that \( \frac{1 - e^{-t}}{t} \) is bounded above by 1 on the interval (0, 1].  have h_bound : ∀ t ∈ Set.Ioc 0 1, (1 - Real.exp (-t)) / t ≤ 1 := by    exact fun t ht => by rw [ div_le_iff₀ ht.1 ] ; linarith [ Real.add_one_le_exp ( -t ) ] ;  refine' MeasureTheory.Integrable.mono' _ _ _;  exacts [ fun t => 1, by norm_num, by exact Measurable.aestronglyMeasurable ( by exact Measurable.div ( measurable_const.sub ( Real.continuous_exp.measurable.comp ( measurable_neg ) ) ) measurable_id' ), Filter.eventually_of_mem ( MeasureTheory.ae_restrict_mem measurableSet_Ioc ) fun t ht => by rw [ Real.norm_of_nonneg ( div_nonneg ( sub_nonneg.2 <| Real.exp_le_one_iff.2 <| by linarith [ ht.1, ht.2 ] ) ht.1.le ) ] ; exact h_bound t ht ]