FKS2.Li_le_two_lt_e

lemma Li_le_two_lt_e {x : ℝ} (hx2 : 2 ≤ x) (hxe : x < Real.exp 1) : Li x ≤ 2 := by  have hlog2 : (0:ℝ) < Real.log 2 := Real.log_pos (by norm_num)  have hint : IntervalIntegrable (fun t => 1 / Real.log t) MeasureTheory.volume 2 x := by    apply ContinuousOn.intervalIntegrable    apply continuousOn_of_forall_continuousAt    intro t ht    rw [Set.uIcc_of_le hx2, Set.mem_Icc] at ht    exact ContinuousAt.div continuousAt_const      (Real.continuousAt_log (by linarith [ht.1])) (Real.log_pos (by linarith [ht.1])).ne'  have hmono : Li x ≤ ∫ _t in (2:ℝ)..x, 1 / Real.log 2 := by    unfold Li    apply intervalIntegral.integral_mono_on hx2 hint intervalIntegrable_const    intro t ht    simp only [Set.mem_Icc] at ht    exact div_le_div_of_nonneg_left (by norm_num) hlog2 (Real.log_le_log (by norm_num) ht.1)  rw [intervalIntegral.integral_const, smul_eq_mul] at hmono  have he3 : Real.exp 1 < 3 := by nlinarith [Real.exp_one_lt_d9]  have : (x - 2) * (1 / Real.log 2) ≤ 2 := by    rw [mul_one_div, div_le_iff₀ hlog2]; nlinarith [Real.log_two_gt_d9, hxe, he3]  linarith [hmono]