have h2v : ContinuousOn v [[a, b]] := fun x hx ↦ (hv x hx).continuousWithinAt
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]]
⊢ ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a
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]]
⊢ ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a