Li2Bounds.setDiff_integral_eq_split

theorem setDiff_integral_eq_split (ε x : ℝ) (hε : 0 < ε) (hε1 : ε < 1) (hx : 2 ≤ x) :    ∫ t in Set.Ioc 0 x \ Set.Ioo (1 - ε) (1 + ε), 1 / log t =      (∫ t in (0 : ℝ)..(1 - ε), 1 / log t) + ∫ t in (1 + ε)..x, 1 / log t := by  rw [setDiff_decompose ε x hε hx, setIntegral_union (by grind) measurableSet_Icc,    intervalIntegral.integral_of_le (by linarith),    integral_Icc_eq_integral_Ioc,    intervalIntegral.integral_of_le (by linarith)]  · have hlog_neg : log (1 - ε) < 0 := Real.log_neg (by linarith) (by linarith)    have hcont : ContinuousOn (fun t => 1 / log t) (Set.Ioc 0 (1 - ε)) :=      ContinuousOn.div continuousOn_const        (Real.continuousOn_log.mono fun x hx => ne_of_gt hx.1)        fun x hx => Real.log_ne_zero_of_pos_of_ne_one hx.1 (by linarith [hx.2])    refine IntegrableOn.of_bound measure_Ioc_lt_top      (hcont.aestronglyMeasurable measurableSet_Ioc) (-1 / log (1 - ε)) ?_    filter_upwards [ae_restrict_mem measurableSet_Ioc] with t ht    simp only [Set.mem_Ioc] at ht    rw [norm_div, norm_one, Real.norm_eq_abs,      abs_of_neg (Real.log_neg ht.1 (by linarith [ht.2])),      show (-1 : ℝ) / log (1 - ε) = 1 / (-log (1 - ε)) from by ring]    exact one_div_le_one_div_of_le (neg_pos.mpr hlog_neg)      (by linarith [Real.log_le_log ht.1 ht.2])  · exact ContinuousOn.integrableOn_compact isCompact_Icc      (ContinuousOn.div continuousOn_const        (Real.continuousOn_log.mono fun x hx => ne_of_gt (by linarith [hx.1] : (0 : ℝ) < x))        fun x hx => Real.log_ne_zero_of_pos_of_ne_one (by linarith [hx.1] : 0 < x)          (by linarith [hx.1]))