Li2Bounds.limit_integral_g

theorem limit_integral_g :    Filter.Tendsto (fun ε => ∫ u in ε..1, g u) (nhdsWithin 0 (Ioi 0))      (nhds (∫ u in (0 : ℝ)..1, g u)) := by  have heq' : (fun ε => ∫ u in ε..(1 : ℝ), g u) = (fun ε => -∫ u in (1 : ℝ)..ε, g u) :=    funext fun ε => intervalIntegral.integral_symm 1 ε  have hval : -∫ u in (1 : ℝ)..0, g u = ∫ u in (0 : ℝ)..1, g u := by    rw [intervalIntegral.integral_symm 0 1]; ring  rw [heq', ← hval]  have hcont : ContinuousOn (fun x => ∫ u in (1 : ℝ)..x, g u) (Icc 0 1) := by    rw [← Set.uIcc_of_le (by norm_num : (0 : ℝ) ≤ 1)]    exact intervalIntegral.continuousOn_primitive_interval' g_intervalIntegrable_full      (by simp)  exact ((hcont.neg 0 (Set.left_mem_Icc.2 (by norm_num))).mono_left    (nhdsWithin_mono 0 Ioo_subset_Icc_self)).mono_left    (le_of_eq (nhdsWithin_Ioo_eq_nhdsGT (by norm_num : (0 : ℝ) < 1)).symm)