FKS2.Li_identity

theorem Li_identity {x} (hx : 2 ≤ x) :    Li x = x / log x - 2 / log 2 + ∫ t in 2..x, 1 / (log t ^ 2) := by  have hnt {t} (ht : t ∈ Set.uIcc 2 x) : t ≠ 0 := by simp_all; linarith  rw [Li, funext fun t ↦ (mul_one (1 / log t)).symm,    intervalIntegral.integral_mul_deriv_eq_deriv_mul (u := fun t ↦ 1 / log t)    (u' := fun t ↦ -(1 / t) / log t ^ 2) _ (fun t _ ↦ hasDerivAt_id' t) _    intervalIntegrable_const]  · suffices ∫ (x : ℝ) in 2..x, - (1 / x) / log x ^ 2 * x      = ∫ (x : ℝ) in 2..x, - (1 / (log x ^ 2)) from by      rw [this, intervalIntegral.integral_neg]; ring    refine intervalIntegral.integral_congr fun t ht ↦ ?_    ring_nf    rw [mul_inv_cancel₀ (hnt ht), one_mul]  · intro t ht    simpa using! HasDerivAt.inv (hasDerivAt_log (hnt ht)) (by simp_all; grind)  · simp only [neg_div, div_div]    simpa using! (l0 (refl 2) hx).intervalIntegrable.neg