apply (integrableOn_iff_integrable_of_support_subset <|
       Function.support_mul_subset_of_subset fSupp).mp
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ 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)
Icc_sub : Icc a b ⊆ Ioi 0
fderivSupp : Function.support (deriv f) ⊆ Icc a b
fgSupp : Function.support (f * g) ⊆ Icc a b
⊢ IntegrableOn (f * deriv g) (Ioi 0) volume
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f g : ℝ → ℂ
ha : 0 < a
h : a ≤ b
fSupp : Function.support f ⊆ 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)
Icc_sub : Icc a b ⊆ Ioi 0
fderivSupp : Function.support (deriv f) ⊆ Icc a b
fgSupp : Function.support (f * g) ⊆ Icc a b
⊢ IntegrableOn (f * deriv g) (Icc a b) (volume.restrict (Ioi 0))