-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_comp_smul_deriv''' {f f' : ℝ → ℝ} {g : ℝ → G} (hf : ContinuousOn f [[a, b]])
    (hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x)
    (hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))) (hg1 : IntegrableOn g (f '' [[a, b]]))
    (hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]) :
    (∫ x in a..b, f' x • (g ∘ f) x) = ∫ u in f a..f b, g u

Proof state:
case intro.intro
a b : ℝ
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f f' : ℝ → ℝ
g : ℝ → G
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]] volume
hG : CompleteSpace G
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (a ⊓ b) (a ⊔ b)
c : ℝ
hc : c ∈ Ioo (a ⊓ b) x
d : ℝ
hd : d ∈ Ioo x (a ⊔ b)
cdsub : [[c, d]] ⊆ Ioo (a ⊓ b) (a ⊔ b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
h2g : IntervalIntegrable g volume (f a) (f x)
h3g : StronglyMeasurableAtFilter g (𝓝[J] f x) volume
this✝ : Fact (f x ∈ J)
this : HasDerivWithinAt (fun u => ∫ (x : ℝ) in f a..u, g x) (g (f x)) J (f x)
⊢ Ioo x d ⊆ [[c, d]]

Tactic:
exact Ioo_subset_Icc_self.trans ((Icc_subset_Icc_left hc.2.le).trans Icc_subset_uIcc)

Result:
no goals

Proof state:
case intro.intro
a b : ℝ
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f f' : ℝ → ℝ
g : ℝ → G
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]] volume
hG : CompleteSpace G
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (a ⊓ b) (a ⊔ b)
c : ℝ
hc : c ∈ Ioo (a ⊓ b) x
d : ℝ
hd : d ∈ Ioo x (a ⊔ b)
cdsub : [[c, d]] ⊆ Ioo (a ⊓ b) (a ⊔ b)
hg_cont : ContinuousOn g (f '' [[c, d]])
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x

Tactic:
have hJ : f '' [[c, d]] = J := (hf.mono (cdsub.trans Ioo_subset_Icc_self)).image_uIcc

Result:
case intro.intro
a b : ℝ
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f f' : ℝ → ℝ
g : ℝ → G
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]] volume
hG : CompleteSpace G
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (a ⊓ b) (a ⊔ b)
c : ℝ
hc : c ∈ Ioo (a ⊓ b) x
d : ℝ
hd : d ∈ Ioo x (a ⊔ b)
cdsub : [[c, d]] ⊆ Ioo (a ⊓ b) (a ⊔ b)
hg_cont : ContinuousOn g (f '' [[c, d]])
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hJ : f '' [[c, d]] = J
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x

Proof state:
case intro.intro
a b : ℝ
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f f' : ℝ → ℝ
g : ℝ → G
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (a ⊓ b) (a ⊔ b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]] volume
hG : CompleteSpace G
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (a ⊓ b) (a ⊔ b)
c : ℝ
hc : c ∈ Ioo (a ⊓ b) x
d : ℝ
hd : d ∈ Ioo x (a ⊔ b)
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x

Tactic:
have cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b) := by
  rw [uIcc_of_le (hc.2.trans hd.1).le]
  exact Icc_subset_Ioo hc.1 hd.2

Result:
case intro.intro
a b : ℝ
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f f' : ℝ → ℝ
g : ℝ → G
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (a ⊓ b) (a ⊔ b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]] volume
hG : CompleteSpace G
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (a ⊓ b) (a ⊔ b)
c : ℝ
hc : c ∈ Ioo (a ⊓ b) x
d : ℝ
hd : d ∈ Ioo x (a ⊔ b)
cdsub : [[c, d]] ⊆ Ioo (a ⊓ b) (a ⊔ b)
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x

Proof state:
a b : ℝ
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f f' : ℝ → ℝ
g : ℝ → G
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]] volume
hG : CompleteSpace G
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (a ⊓ b) (a ⊔ b)
c : ℝ
hc : c ∈ Ioo (a ⊓ b) x
d : ℝ
hd : d ∈ Ioo x (a ⊔ b)
cdsub : [[c, d]] ⊆ Ioo (a ⊓ b) (a ⊔ b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
⊢ [[f a, f x]] ⊆ [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]

Tactic:
rw [← hf.image_uIcc]

Result:
a b : ℝ
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f f' : ℝ → ℝ
g : ℝ → G
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]] volume
hG : CompleteSpace G
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (a ⊓ b) (a ⊔ b)
c : ℝ
hc : c ∈ Ioo (a ⊓ b) x
d : ℝ
hd : d ∈ Ioo x (a ⊔ b)
cdsub : [[c, d]] ⊆ Ioo (a ⊓ b) (a ⊔ b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
⊢ [[f a, f x]] ⊆ f '' [[a, b]]

Proof state:
case intro.intro
a b : ℝ
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f f' : ℝ → ℝ
g : ℝ → G
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]] volume
hG : CompleteSpace G
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (a ⊓ b) (a ⊔ b)
c : ℝ
hc : c ∈ Ioo (a ⊓ b) x
d : ℝ
hd : d ∈ Ioo x (a ⊔ b)
cdsub : [[c, d]] ⊆ Ioo (a ⊓ b) (a ⊔ b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x

Tactic:
have h2x : f x ∈ J := by rw [← hJ]; exact mem_image_of_mem _ (mem_uIcc_of_le hc.2.le hd.1.le)

Result:
case intro.intro
a b : ℝ
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f f' : ℝ → ℝ
g : ℝ → G
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]] volume
hG : CompleteSpace G
h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (a ⊓ b) (a ⊔ b)
c : ℝ
hc : c ∈ Ioo (a ⊓ b) x
d : ℝ
hd : d ∈ Ioo x (a ⊔ b)
cdsub : [[c, d]] ⊆ Ioo (a ⊓ b) (a ⊔ b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
⊢ HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x