li.sub_Li

@[blueprint  "li_minus_Li"  (title := "li minus Li")  (statement := /-- $\li(x) - \Li(x) = \li(2)$. -/)  (proof := /--    This follows from the previous estimate. -/)  (latexEnv := "remark")  (discussion := 758)]theorem li.sub_Li (x : ℝ) (h2x : 2 ≤ x) : li x - Li x = li 2 := by  have : Filter.Tendsto (fun ε => ∫ t in Set.Ioc 0 x \ Set.Ioo (1 - ε) (1 + ε), 1 / log t)      (𝓝[>] 0) (nhds (Li2Bounds.li2_symmetric + Li x)) := by    apply Filter.Tendsto.congr' (f₁ := fun ε ↦      (∫ t in (0:ℝ)..(1 - ε), 1 / log t) + (∫ t in (1 + ε)..2, 1 / log t) + Li x)    · filter_upwards [Ioo_mem_nhdsGT (by linarith : (0 : ℝ) < 1)] with ε hε      rw [Li2Bounds.setDiff_integral_eq_split ε x hε.1 hε.2 h2x]      unfold Li      rw [add_assoc, intervalIntegral.integral_add_adjacent_intervals]      all_goals        apply ContinuousOn.intervalIntegrable fun t ht ↦          ContinuousAt.continuousWithinAt ?_        rw [Set.uIcc_of_le (by grind)] at ht        have : log t ≠ 0 := by          simp only [ne_eq, log_eq_zero]          grind        fun_prop (disch := grind)    · apply Filter.Tendsto.add_const      apply Li2Bounds.pv_tendsto_li2_symmetric.congr'      filter_upwards [Ioo_mem_nhdsGT (by linarith : (0 : ℝ) < 1)] with ε hε using        Li2Bounds.setDiff_integral_eq_split ε 2 hε.1 hε.2 (by rfl)  have : li x = Li2Bounds.li2_symmetric + Li x :=    this.limUnder_eq  rw [this, Li2Bounds.li2_symmetric_eq_li2]  simp only [add_sub_cancel_right]  rfl