Mathlib Abel summation for sum 1/p: working recipe and pitfalls

To get Mertens-2-type bounds from sum_mul_eq_sub_sub_integral_mul c (ha : 0 ≤ a) (hab) hf_diff hf_int with f t = (log t)⁻¹: (1) HasDerivAt.inv on Real.hasDerivAt_log gives the derivative as -(t⁻¹) / log t ^ 2, but after simpa the function becomes log⁻¹ (Pi inverse) and no longer matches fun t ↦ (log t)⁻¹, so use convert h using 1 instead; (2) get IntegrableOn (deriv f) by hg_int.neg.congr_fun (fun t ht ↦ (hderiv t ht).symm) measurableSet_Icc, with hg_int from ContinuousOn.integrableOn_Icc; (3) integrability of g t * (∑_{k ≤ ⌊t⌋} c k) is integrableOn_mul_sum_Icc c ha hg_int; (4) the FTC antiderivatives log(log t) and -(log t)⁻¹ go through intervalIntegral.integral_eq_sub_of_hasDerivAt (pass (f := ...) explicitly, or a CompleteSpace metavariable gets stuck), then intervalIntegral.integral_of_le converts to ∫ t in Set.Ioc a b; (5) for the error integral use norm_integral_le_of_norm_le (f := ...) (hint.const_mul A) with filter_upwards [ae_restrict_mem measurableSet_Ioc]. The whole theorem is about 100 lines.