tendsto_integral_exp_sub_one_div

lemma tendsto_integral_exp_sub_one_div {y : ℝ} (hy : 0 < y) :    Tendsto (fun ε => ∫ u in ε..y, (exp u - 1) / u)      (𝓝[>] (0 : ℝ)) (𝓝 (∫ u in (0:ℝ)..y, (exp u - 1) / u)) := by  -- The function (exp(u)-1)/u is integrable on (0,y].  have h_integrable : MeasureTheory.IntegrableOn (fun u => (Real.exp u - 1) / u) (Set.Ioc 0 y) := by    exact integrableOn_exp_sub_one_div hy;  -- Let's choose any $M > 0$ such that $y < M$.  obtain ⟨M, hM⟩ : ∃ M > y, True := by    exact ⟨ y + 1, by linarith, trivial ⟩;  -- The integral of (exp(u)-1)/u over (0, M) is continuous at 0.  have h_cont : ContinuousOn (fun ε => ∫ u in ε..y, (Real.exp u - 1) / u) (Set.Icc 0 M) := by    have h_integrable_M : MeasureTheory.IntegrableOn (fun u => (Real.exp u - 1) / u) (Set.Ioc 0 M) := by      have h_integrable_M : MeasureTheory.IntegrableOn (fun u => (Real.exp u - 1) / u) (Set.Ioc y M) := by        exact ContinuousOn.integrableOn_Icc ( by exact continuousOn_of_forall_continuousAt fun u hu => ContinuousAt.div ( ContinuousAt.sub ( Real.continuous_exp.continuousAt ) continuousAt_const ) continuousAt_id <| by linarith [ hu.1 ] ) |> fun h => h.mono_set <| Set.Ioc_subset_Icc_self;      convert h_integrable.union h_integrable_M using 1 ; rw [ Set.Ioc_union_Ioc_eq_Ioc ] <;> linarith;    have h_cont : ContinuousOn (fun ε => ∫ u in (y)..ε, (Real.exp u - 1) / u) (Set.Icc 0 M) := by      intro ε hε; apply_rules [ intervalIntegral.continuousWithinAt_primitive ] ; aesop;      rw [ min_eq_right hy.le, max_eq_right hM.1.le ] ; rw [ intervalIntegrable_iff_integrableOn_Ioc_of_le ( by linarith ) ] ; aesop;    exact ContinuousOn.congr ( h_cont.fun_neg ) fun x hx => by rw [ ← intervalIntegral.integral_symm ] ;  have := h_cont 0 ⟨ by norm_num, by linarith ⟩;  convert this.tendsto.mono_left _ using 2;  norm_num [ nhdsWithin, Filter.mem_inf_principal ];  exact Filter.eventually_of_mem ( Iio_mem_nhds <| show 0 < M by linarith ) fun x hx => fun hx' => ⟨ le_of_lt hx', le_of_lt hx ⟩