no goals
ι : Type ?u.1940354
𝕜 : Type ?u.1940357
E : Type ?u.1940360
F : Type ?u.1940363
A : Type ?u.1940366
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' 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, b]])
⊢ (∫ (x : ℝ) in a..b, (g ∘ f) x * f' x) = ∫ (u : ℝ) in f a..f b, g u
simpa [mul_comm] using integral_comp_smul_deriv'' hf hff' hf' hg