ι : Type ?u.1904826
𝕜 : Type ?u.1904829
E : Type u_1
F : Type ?u.1904835
A : Type ?u.1904838
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
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]])
⊢ IntegrableOn g (f '' [[a, b]])
ι : Type ?u.1904826
𝕜 : Type ?u.1904829
E : Type u_1
F : Type ?u.1904835
A : Type ?u.1904838
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
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, f' x • (g ∘ f) x) = ∫ (u : ℝ) in f a..f b, g u
refine'
  integral_comp_smul_deriv''' hf hff' (hg.mono <| image_subset _ Ioo_subset_Icc_self) _
    (hf'.smul (hg.comp hf <| subset_preimage_image f _)).integrableOn_Icc
ι : Type ?u.1904826
𝕜 : Type ?u.1904829
E : Type u_1
F : Type ?u.1904835
A : Type ?u.1904838
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
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 [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]
⊢ IntegrableOn g [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]
ι : Type ?u.1904826
𝕜 : Type ?u.1904829
E : Type u_1
F : Type ?u.1904835
A : Type ?u.1904838
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
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]])
⊢ IntegrableOn g (f '' [[a, b]])
rw [hf.image_uIcc] at hg ⊢
no goals
ι : Type ?u.1904826
𝕜 : Type ?u.1904829
E : Type u_1
F : Type ?u.1904835
A : Type ?u.1904838
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' : ℝ → ℝ
g : ℝ → E
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 [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]
⊢ IntegrableOn g [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]
exact hg.integrableOn_Icc