Mertens.integral_one_div_mul_log

lemma integral_one_div_mul_log {x : ℝ} (hx : 2 ≤ x) :    ∫ t in 2..x, 1 / (t * log t) = log (log x) - log (log 2) := by  rw [← intervalIntegral.integral_deriv_eq_sub (f := fun t ↦ log (log t))]  · refine intervalIntegral.integral_congr fun t ht ↦ ?_    rw [deriv_log_log]    rw [Set.uIcc_of_le hx, Set.mem_Icc] at ht    linarith  · intro t ht    rw [Set.uIcc_of_le hx, Set.mem_Icc] at ht    have : log t ≠ 0 := by simp; grind    fun_prop (disch := grind)  · refine ContinuousOn.intervalIntegrable ?_    apply ContinuousOn.congr (f := (fun t ↦ 1 / (t * log t)))    · refine fun t ht ↦ ContinuousAt.continuousWithinAt ?_      rw [Set.uIcc_of_le hx, Set.mem_Icc] at ht      have : log t ≠ 0 := by simp; grind      fun_prop (disch := grind)    · intro t ht      rw [Set.uIcc_of_le hx, Set.mem_Icc] at ht      exact deriv_log_log (by linarith)