integral_Ioi_exp_neg_mul_sin

theorem integral_Ioi_exp_neg_mul_sin (a : ℝ) (ha : 0 < a) :    ∫ x : ℝ in Set.Ioi 0, Real.exp (-a * x) * Real.sin x = 1 / (a ^ 2 + 1) := by  let z : ℂ := (-(a : ℂ)) + Complex.I  have hzre : z.re < 0 := by simp [z, ha]  have hint : Integrable (fun x : ℝ => Complex.exp (z * x)) (volume.restrict (Set.Ioi 0)) := by    exact integrableOn_exp_mul_complex_Ioi (a := z) hzre 0  have him := integral_im (μ := volume.restrict (Set.Ioi 0)) hint  have hpoint : (fun x : ℝ => Real.exp (-a * x) * Real.sin x) =      fun x : ℝ => (Complex.exp (z * x)).im := by    funext x    simp [z, Complex.exp_im, mul_add, mul_comm]  calc    ∫ x : ℝ in Set.Ioi 0, Real.exp (-a * x) * Real.sin x        = ∫ x : ℝ in Set.Ioi 0, (Complex.exp (z * x)).im := by          rw [hpoint]    _ = (∫ x : ℝ in Set.Ioi 0, Complex.exp (z * x)).im := by          simpa using him    _ = (-Complex.exp (z * (0 : ℝ)) / z).im := by          rw [integral_exp_mul_complex_Ioi (a := z) hzre 0]    _ = 1 / (a ^ 2 + 1) := by          simp [z, Complex.div_im, Complex.normSq]          ring