integral_exp_div_neg_eq

lemma integral_exp_div_neg_eq {ε : ℝ} (hε : 0 < ε) :    ∫ u in (-1/ε)..(-ε), exp u / u = -(∫ t in ε..(1/ε), exp (-t) / t) := by  -- Apply the substitution $u = -t$ and adjust the limits of integration accordingly.  have h_subst : ∫ u in (-1 / ε)..(-ε), Real.exp u / u = ∫ t in (ε : ℝ)..1 / ε, Real.exp (-t) / (-t) := by    have h_sub : ∀ a b : ℝ, ∫ u in a..b, Real.exp u / u = ∫ t in (-b)..(-a), Real.exp (-t) / (-t) := by      norm_num [ ← intervalIntegral.integral_comp_neg ]    grind;  simpa [ div_neg ] using h_subst