awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) [[a, b]] volume
hE : CompleteSpace E
h_cont : ContinuousOn.{0, u_1} (Y := E) (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max 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 (mα := MeasureSpace.toMeasurableSpace) g (𝓝[J] f x) volume
this_1 : Fact (f x ∈ J)
this : HasDerivWithinAt (fun (u : ℝ) ↦ ∫ (x : ℝ) in f a..u, g x) (g (f x)) J (f x)
⊢ MapsTo f (Ioo x d) (f '' [[c, d]])

Tactic:
(mapsTo_image _ _).mono ?_ Subset.rfl

Premises used: Set.mapsTo_image, Set.MapsTo.mono, Set.Subset.rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) [[a, b]] volume
hE : CompleteSpace E
h_cont : ContinuousOn.{0, u_1} (Y := E) (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max 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 (mα := MeasureSpace.toMeasurableSpace) g (𝓝[J] f x) volume
this_1 : Fact (f x ∈ J)
this : HasDerivWithinAt (fun (u : ℝ) ↦ ∫ (x : ℝ) in f a..u, g x) (g (f x)) J (f x)
refine : Ioo x d ⊆ [[c, d]]
⊢ MapsTo f (Ioo x d) (f '' [[c, d]])

Tactic:
refine (mapsTo_image _ _).mono ?_ Subset.rfl

Premises used: Set.mapsTo_image, Set.MapsTo.mono, Set.Subset.rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) [[a, b]] volume
hE : CompleteSpace E
h_cont : ContinuousOn.{0, u_1} (Y := E) (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max 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 (mα := MeasureSpace.toMeasurableSpace) g (𝓝[J] f x) volume
this_1 : 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:
Ioo_subset_Icc_self.trans ((Icc_subset_Icc_left hc.2.le).trans Icc_subset_uIcc)

Premises used: Set.Ioo_subset_Icc_self, Set.Icc_subset_uIcc, Set.Icc_subset_Icc_left, HasSubset.Subset.trans, LT.lt.le, And.right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) [[a, b]] volume
hE : CompleteSpace E
h_cont : ContinuousOn.{0, u_1} (Y := E) (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max 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 (mα := MeasureSpace.toMeasurableSpace) g (𝓝[J] f x) volume
this_1 : 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)

Premises used: Set.Ioo_subset_Icc_self, Set.Icc_subset_uIcc, Set.Icc_subset_Icc_left, HasSubset.Subset.trans, LT.lt.le, And.right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
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 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) [[a, b]] volume
hE : CompleteSpace E
h_cont : ContinuousOn.{0, u_1} (Y := E) (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
⊢ ∀ x ∈ Ioo (min a b) (max a b),
    HasDerivWithinAt (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x

Tactic:
have h_der :
    ∀ x ∈ Ioo (min a b) (max a b),
      HasDerivWithinAt (fun u ↦ ∫ t in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x := by
    intro x hx
    obtain ⟨c, hc⟩ := nonempty_Ioo.mpr hx.1
    obtain ⟨d, hd⟩ := nonempty_Ioo.mpr hx.2
    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
    replace hg_cont := hg_cont.mono (image_mono cdsub)
    let J := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
    have hJ : f '' [[c, d]] = J := (hf.mono (cdsub.trans Ioo_subset_Icc_self)).image_uIcc
    rw [hJ] at hg_cont
    have h2x : f x ∈ J := by rw [← hJ]; exact mem_image_of_mem _ (mem_uIcc_of_le hc.2.le hd.1.le)
    have h2g : IntervalIntegrable g volume (f a) (f x) := by
      refine hg1.mono_set ?_
      rw [← hf.image_uIcc]
      exact hf.surjOn_uIcc left_mem_uIcc (Ioo_subset_Icc_self hx)
    have h3g : StronglyMeasurableAtFilter g (𝓝[J] f x) :=
      hg_cont.stronglyMeasurableAtFilter_nhdsWithin measurableSet_Icc (f x)
    haveI : Fact (f x ∈ J) := ⟨h2x⟩
    have : HasDerivWithinAt (fun u ↦ ∫ x in f a..u, g x) (g (f x)) J (f x) :=
      intervalIntegral.integral_hasDerivWithinAt_right h2g h3g (hg_cont (f x) h2x)
    refine (this.scomp x ((hff' x hx).Ioo_of_Ioi hd.1) ?_).Ioi_of_Ioo hd.1
    rw [← hJ]
    refine (mapsTo_image _ _).mono ?_ Subset.rfl
    exact Ioo_subset_Icc_self.trans ((Icc_subset_Icc_left hc.2.le).trans Icc_subset_uIcc)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
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 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) [[a, b]] volume
hE : CompleteSpace E
h_cont : ContinuousOn.{0, u_1} (Y := E) (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
h_der :
  ∀ x ∈ Ioo (min a b) (max a b),
    HasDerivWithinAt (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) volume a b

Tactic:
rw [← intervalIntegrable_iff'] at hg2

Premises used: intervalIntegrable_iff'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
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 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) [[a, b]] volume
hE : CompleteSpace E
h_cont : ContinuousOn.{0, u_1} (Y := E) (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
h_der :
  ∀ x ∈ Ioo (min a b) (max a b),
    HasDerivWithinAt (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
hg2₁ : IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) volume a b
⊢ CompleteSpace E

Tactic:
rw [← intervalIntegrable_iff'] at hg2

Premises used: intervalIntegrable_iff'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
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 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) [[a, b]] volume
hE : CompleteSpace E
h_cont : ContinuousOn.{0, u_1} (Y := E) (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
h_der :
  ∀ x ∈ Ioo (min a b) (max a b),
    HasDerivWithinAt (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
hg2₁ : IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) volume a b
hE₁ : CompleteSpace E
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]

Tactic:
rw [← intervalIntegrable_iff'] at hg2

Premises used: intervalIntegrable_iff'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
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 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) [[a, b]] volume
hE : CompleteSpace E
h_cont : ContinuousOn.{0, u_1} (Y := E) (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
h_der :
  ∀ x ∈ Ioo (min a b) (max a b),
    HasDerivWithinAt (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
hg2₁ : IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) volume a b
hE₁ : CompleteSpace E
h_cont₁ : ContinuousOn.{0, u_1} (Y := E) (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
⊢ ∀ x ∈ Ioo (min a b) (max a b),
    HasDerivWithinAt (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x

Tactic:
rw [← intervalIntegrable_iff'] at hg2

Premises used: intervalIntegrable_iff'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
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 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) volume a b
hE : CompleteSpace E
h_cont : ContinuousOn.{0, u_1} (Y := E) (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
h_der :
  ∀ x ∈ Ioo (min a b) (max a b),
    HasDerivWithinAt (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
pos : HSub.hSub (α := E) (∫ (t : ℝ) in f a..f b, g t) (∫ (t : ℝ) in f a..f a, g t) = ∫ (t : ℝ) in f a..f b, g t
pos₁ : HSub.hSub (α := E) (∫ (t : ℝ) in f a..f b, g t) 0 = ∫ (t : ℝ) in f a..f b, g t
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (u : ℝ) in f a..f b, g u)

Tactic:
simp_rw [integral_eq_sub_of_hasDeriv_right h_cont h_der hg2, integral_same, sub_zero]

Premises used: sub_zero, intervalIntegral.integral_same, intervalIntegral.integral_eq_sub_of_hasDeriv_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ 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]])
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (u : ℝ) in f a..f b, g u)

Tactic:
integral_deriv_smul_comp''' hf hff' (hg.mono <| image_mono Ioo_subset_Icc_self) ?_
    (hf'.smul (hg.comp hf <| subset_preimage_image f _)).integrableOn_Icc

Premises used: Set.Ioo_subset_Icc_self, ContinuousOn.integrableOn_Icc, Set.image_mono, ContinuousOn.comp, ContinuousOn.smul, ContinuousOn.mono, intervalIntegral.integral_deriv_smul_comp''', Set.subset_preimage_image
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ 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]])
refine : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' [[a, b]]) volume
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (u : ℝ) in f a..f b, g u)

Tactic:
refine integral_deriv_smul_comp''' hf hff' (hg.mono <| image_mono Ioo_subset_Icc_self) ?_
    (hf'.smul (hg.comp hf <| subset_preimage_image f _)).integrableOn_Icc

Premises used: Set.Ioo_subset_Icc_self, ContinuousOn.integrableOn_Icc, Set.image_mono, ContinuousOn.comp, ContinuousOn.smul, ContinuousOn.mono, intervalIntegral.integral_deriv_smul_comp''', Set.subset_preimage_image
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ 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]])
rw :
  ∀ (hg : ContinuousOn g [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]),
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]] volume
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' [[a, b]]) volume

Tactic:
rw [hf.image_uIcc] at hg ⊢

Premises used: ContinuousOn.image_uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ 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 (mα := MeasureSpace.toMeasurableSpace) g [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]] volume

Tactic:
hg.integrableOn_Icc

Premises used: ContinuousOn.integrableOn_Icc, Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ 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 (mα := MeasureSpace.toMeasurableSpace) g [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]] volume

Tactic:
exact hg.integrableOn_Icc

Premises used: ContinuousOn.integrableOn_Icc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
h : ∀ x ∈ [[a, b]], HasDerivAt f (f' x) x
h' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g (f '' [[a, b]])
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (x : ℝ) in f a..f b, g x)

Tactic:
integral_deriv_smul_comp'' (fun x hx ↦ (h x hx).continuousAt.continuousWithinAt)
    (fun x hx ↦ (h x <| Ioo_subset_Icc_self hx).hasDerivWithinAt) h' hg

Premises used: HasDerivAt.hasDerivWithinAt, Set.Ioo_subset_Icc_self, ContinuousAt.continuousWithinAt, HasDerivAt.continuousAt, intervalIntegral.integral_deriv_smul_comp''
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
h : ∀ x ∈ [[a, b]], HasDerivAt f (f' x) x
h' : ContinuousOn f' [[a, b]]
hg : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (x : ℝ) in f a..f b, g x)

Tactic:
integral_deriv_smul_comp' h h' hg.continuousOn

Premises used: intervalIntegral.integral_deriv_smul_comp', Continuous.continuousOn
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
hf'₁ : DifferentiableOn ℝ f (interior [[a, b]])
hf'_nonneg : ∀ x ∈ interior [[a, b]], 0 ≤ deriv f x
⊢ MonotoneOn f [[a, b]]

Tactic:
apply monotoneOn_of_deriv_nonneg (convex_uIcc a b) hf

Premises used: monotoneOn_of_deriv_nonneg, convex_uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
hf'₁ : DifferentiableOn ℝ f (Ioo (min a b) (max a b))
⊢ DifferentiableOn ℝ f (interior [[a, b]])

Tactic:
rw [uIcc, interior_Icc]

Premises used: interior_Icc, Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
⊢ DifferentiableOn ℝ f (Ioo (min a b) (max a b))

Tactic:
fun z hz ↦ (hff' z hz).differentiableAt.differentiableWithinAt

Premises used: HasDerivAt.differentiableAt, DifferentiableAt.differentiableWithinAt, DifferentiableOn
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
⊢ DifferentiableOn ℝ f (Ioo (min a b) (max a b))

Tactic:
exact fun z hz ↦ (hff' z hz).differentiableAt.differentiableWithinAt

Premises used: HasDerivAt.differentiableAt, DifferentiableAt.differentiableWithinAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
hf'_nonneg : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ deriv f x
⊢ ∀ x ∈ interior [[a, b]], 0 ≤ deriv f x

Tactic:
rw [uIcc, interior_Icc]

Premises used: interior_Icc, Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
z : ℝ
hz : z ∈ Ioo (min a b) (max a b)
⊢ 0 ≤ deriv f z

Tactic:
simpa [(hff' z hz).deriv] using hf' z hz

Premises used: HasDerivAt.deriv
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
⊢ MonotoneOn f [[a, b]]

Tactic:
have M : MonotoneOn f (uIcc a b) := by
    apply monotoneOn_of_deriv_nonneg (convex_uIcc a b) hf
    · rw [uIcc, interior_Icc]
      exact fun z hz ↦ (hff' z hz).differentiableAt.differentiableWithinAt
    · rw [uIcc, interior_Icc]
      intro z hz
      simpa [(hff' z hz).deriv] using hf' z hz
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
simp : Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (u : ℝ) in f a..f b, g u)

Tactic:
simp only [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
inl : ∀ (hab : a ≤ b), Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)
inr : ∀ (hab : b < a), Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)

Tactic:
rcases le_or_gt a b with hab | hab

Premises used: le_or_gt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : a ≤ b
inl : f a ≤ f b
inl₁ : ContinuousOn f (Icc a b)
inl₂ : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
inl₃ : ∀ x ∈ Ioo a b, 0 ≤ f' x
inl₄ : a ≤ b
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)

Tactic:
rw [integral_of_le hab, ← integral_Icc_eq_integral_Ioc,
      integral_Icc_deriv_smul_of_deriv_nonneg, integral_of_le, ← integral_Icc_eq_integral_Ioc]

Premises used: MeasureTheory.integral_Icc_deriv_smul_of_deriv_nonneg, intervalIntegral.integral_of_le, MeasureTheory.integral_Icc_eq_integral_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : a ≤ b
⊢ f a ≤ f b

Tactic:
apply M left_mem_uIcc right_mem_uIcc hab

Premises used: Set.right_mem_uIcc, Set.left_mem_uIcc