Mertens.deriv_gamma_add_γ_eq_zero

@[blueprint  "Euler-Mascheroni-eq"  (title := "Compatibility with Mathlib Euler-Mascheroni constant")  (statement := /-- $\gamma$ is the Euler--Mascheroni constant.-/)  (proof := /-- Take limits as $s \to 1$ in the previous asymptotic using known asymptotics for $\zeta(s)$, and using that $- \Gamma'(1)$ is the Euler--Mascheroni constant. -/)  (latexEnv := "theorem")  (discussion := 1320)]theorem deriv_gamma_add_γ_eq_zero : deriv Gamma 1 + γ = 0 := by  -- For `s > 1`, `log_zeta_eq` rearranges to a constant identity.  have key : ∀ s : ℝ, 1 < s →      (Real.log (riemannZeta (s:ℂ)).re + Real.log (s - 1))        - (s - 1) * ∫ x in Set.Ioi 1, E₂Λ x * x ^ (-s) = deriv Gamma 1 + γ := by    intro s hs    have h := log_zeta_eq s hs    linarith  -- The LHS is eventually constant, so its limit is that constant.  have hconst : Filter.Tendsto      (fun s : ℝ => (Real.log (riemannZeta (s:ℂ)).re + Real.log (s - 1))        - (s - 1) * ∫ x in Set.Ioi 1, E₂Λ x * x ^ (-s))      (nhdsWithin 1 (Set.Ioi 1)) (nhds (deriv Gamma 1 + γ)) := by    refine Filter.Tendsto.congr' ?_ tendsto_const_nhds    filter_upwards [self_mem_nhdsWithin] with s hs    exact (key s hs).symm  -- But the same function tends to `0 - 0` by the two limit lemmas.  have hlim := log_zeta_limit.sub sub_one_mul_integral_E₂Λ_tendsto  rw [sub_zero] at hlim  exact tendsto_nhds_unique hconst hlim