no goals
ι : Type ?u.1953788
𝕜 : Type ?u.1953791
E : Type ?u.1953794
F : Type ?u.1953797
A : Type ?u.1953800
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g'✝ g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' g g' : ℝ → ℝ
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hf' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g [[f a, f b]]
hgg' : ∀ (x : ℝ), x ∈ Ioo (min (f a) (f b)) (max (f a) (f b)) → HasDerivWithinAt g (g' x) (Ioi x) x
hg' : ContinuousOn g' (f '' [[a, b]])
⊢ (∫ (x : ℝ) in a..b, (g' ∘ f) x * f' x) = (g ∘ f) b - (g ∘ f) a
simpa [mul_comm] using integral_deriv_comp_smul_deriv' hf hff' hf' hg hgg' hg'