PartialIntegration_of_support_in_Icc

lemma PartialIntegration_of_support_in_Icc {a b : ℝ} (f g : ℝ → ℂ) (ha : 0 < a)    (h : a ≤ b)    (fSupp : f.support ⊆ Set.Icc a b)    (fDiff : DifferentiableOn ℝ f (Ioi 0))    (gDiff : DifferentiableOn ℝ g (Ioi 0))    (fderivCont : ContinuousOn (deriv f) (Ioi 0))    (gderivCont : ContinuousOn (deriv g) (Ioi 0)) :    ∫ x in Ioi 0, f x * deriv g x = -∫ x in Ioi 0, deriv f x * g x := by  have Icc_sub : Icc a b ⊆ Ioi 0 := (Icc_subset_Ioi_iff h).mpr ha  have fderivSupp := Function.support_deriv_subset_Icc fSupp  have fgSupp : (f * g).support ⊆ Icc a b := Function.support_mul_subset_of_subset fSupp  have fDerivgInt : IntegrableOn (f * deriv g) (Ioi 0) := by    apply (integrableOn_iff_integrable_of_support_subset <|           Function.support_mul_subset_of_subset fSupp).mp    exact fDiff.continuousOn.mono Icc_sub |>.mul (gderivCont.mono Icc_sub) |>.integrableOn_Icc  have gDerivfInt : IntegrableOn (deriv f * g) (Ioi 0) := by    apply (integrableOn_iff_integrable_of_support_subset <|           Function.support_mul_subset_of_subset fderivSupp).mp    exact fderivCont.mono Icc_sub |>.mul (gDiff.continuousOn.mono Icc_sub) |>.integrableOn_Icc  have lim_at_zero : Tendsto (f * g) (𝓝[>]0) (𝓝 0) :=    TendstoAtZero_of_support_in_Icc (f * g) ha fgSupp  have lim_at_inf : Tendsto (f * g) atTop (𝓝 0) := TendstoAtTop_of_support_in_Icc (f * g) fgSupp  apply PartialIntegration f g fDiff gDiff fDerivgInt gDerivfInt lim_at_zero lim_at_inf