FKS2.hasDerivAt_Li

lemma hasDerivAt_Li {x : ℝ} (hx : x ∈ Set.Ioi 6.58) : HasDerivAt Li (1 / log x) x := by  have hf (x) (hx : x ∈ Set.Ioi 6.58) : ContinuousAt (fun x ↦ 1 / log x) x := by    have := log_pos (by linarith [Set.mem_Ioi.mp hx]) |>.ne'    fun_prop (disch := simp_all)  refine intervalIntegral.integral_hasDerivAt_right ?_ ?_ (hf x hx)  · have := Set.uIcc_of_le (show 2 ≤ x by linarith [Set.mem_Ioi.mp hx])    apply intervalIntegral.intervalIntegrable_one_div (by grind [log_eq_zero])    fun_prop (disch := grind)  · grind [ContinuousAt.stronglyMeasurableAtFilter isOpen_Ioi hf]