exact (hu'.mul_continuousOn h2v).add (hv'.continuousOn_mul h2u)
case hint
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a b : ℝ
u v u' v' : ℝ → A
hu : ∀ x ∈ [[a, b]], HasDerivWithinAt u (u' x) [[a, b]] x
hv : ∀ x ∈ [[a, b]], HasDerivWithinAt v (v' x) [[a, b]] x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
h2u : ContinuousOn u [[a, b]]
h2v : ContinuousOn v [[a, b]]
⊢ IntervalIntegrable (fun y => u' y * v y + u y * v' y) volume a b
no goals