tendsto_integral_one_sub_exp_neg_div

lemma tendsto_integral_one_sub_exp_neg_div :    Tendsto (fun ε => ∫ t in ε..1, (1 - exp (-t)) / t)      (𝓝[>] (0 : ℝ)) (𝓝 (∫ t in (0:ℝ)..1, (1 - exp (-t)) / t)) := by  -- The function (1 - exp(-t))/t is integrable on (0, 1] by the provided lemma.  have h_integrable : MeasureTheory.IntegrableOn (fun t : ℝ => (1 - Real.exp (-t)) / t) (Set.Ioc 0 1) := by    exact integrableOn_one_sub_exp_neg_div;  -- The integral of a continuous function over a compact interval is continuous, hence the limit can be passed inside.  have h_cont : ContinuousOn (fun ε => ∫ t in (ε)..1, (1 - Real.exp (-t)) / t) (Set.Icc 0 1) := by    have h_cont : ContinuousOn (fun ε => ∫ t in (1 : ℝ)..ε, (1 - Real.exp (-t)) / t) (Set.Icc 0 1) := by      intro ε hε; apply_rules [ intervalIntegral.continuousWithinAt_primitive ] ; aesop;      rw [ intervalIntegrable_iff_integrableOn_Ioc_of_le ] <;> aesop;    exact ContinuousOn.congr ( h_cont.fun_neg ) fun x hx => by rw [ ← intervalIntegral.integral_symm ] ;  have := h_cont 0 ( by norm_num );  convert this.tendsto.mono_left _ using 2 ; norm_num [ Set.Ioi_subset_Ici_self ];  exact nhdsWithin_mono _ <| Set.Ioi_subset_Ici_self