LiSeries.eulerMascheroni_eq_neg_integral

theorem eulerMascheroni_eq_neg_integral :    eulerMascheroniConstant = -(∫ t in Ioi (0 : ℝ), log t * exp (-t)) := by  -- Step 1: Get the complex derivative of GammaIntegral at s = 1  have hpos : (0 : ℝ) < (1 : ℂ).re := by simp  have hderiv_integral := Complex.hasDerivAt_GammaIntegral hpos  -- Step 2: Gamma = GammaIntegral on {s | 0 < s.re}, which is a nhd of 1  have heq : Complex.Gamma =ᶠ[𝓝 1] Complex.GammaIntegral := by    have : {s : ℂ | 0 < s.re} ∈ 𝓝 (1 : ℂ) := by      apply IsOpen.mem_nhds      · exact isOpen_lt continuous_const Complex.continuous_re      · simp    exact Filter.eventuallyEq_iff_exists_mem.mpr ⟨{s : ℂ | 0 < s.re}, this,      fun s hs => Complex.Gamma_eq_integral hs⟩  -- Step 3: So Gamma has the same derivative as GammaIntegral at 1  have hderiv_Gamma := hderiv_integral.congr_of_eventuallyEq heq  -- Step 4: But we also know the derivative of complex Gamma at 1  have hderiv_known := Complex.hasDerivAt_Gamma_one  -- Step 5: By uniqueness of derivatives  have key := hderiv_Gamma.unique hderiv_known  -- Step 6: Simplify the integral in `key`  -- The integrand is ↑t ^ (1 - 1) * (↑(log t) * ↑(rexp (-t)))  -- Simplify to ↑(log t * exp(-t)) using t^0 = 1  have simp_integral : (∫ t : ℝ in Ioi 0,      (t : ℂ) ^ ((1 : ℂ) - 1) * (↑(log t) * ↑(rexp (-t)))) =      ↑(∫ t : ℝ in Ioi 0, log t * rexp (-t)) := by    rw [show (1 : ℂ) - 1 = 0 from sub_self 1]    simp_rw [Complex.cpow_zero, one_mul, ← Complex.ofReal_mul]    exact integral_ofReal  rw [simp_integral] at key  -- key : ↑(∫ t in Ioi 0, log t * rexp (-t)) = -↑eulerMascheroniConstant  rw [← Complex.ofReal_neg] at key  have := Complex.ofReal_injective key.symm  linarith