no goals
ι : Type ?u.1946471
𝕜 : Type ?u.1946474
E : Type ?u.1946477
F : Type ?u.1946480
A : Type ?u.1946483
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' g : ℝ → ℝ
h : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt f (f' x) x
h' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g (f '' [[a, b]])
⊢ (∫ (x : ℝ) in a..b, (g ∘ f) x * f' x) = ∫ (x : ℝ) in f a..f b, g x
simpa [mul_comm] using integral_comp_smul_deriv' h h' hg