awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : CompleteSpace E
inst_6 : IsScalarTower ℝ 𝕜 E
u u' : ℝ → 𝕜
v v' : ℝ → E
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable.{u_2} (ε := E) (fun (x : ℝ) ↦ u x • v' x + u' x • v x) volume a b

Tactic:
(hv'.continuousOn_smul hu).add (hu'.smul_continuousOn hv)

Premises used: IntervalIntegrable.smul_continuousOn, IntervalIntegrable.add, IntervalIntegrable.continuousOn_smul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : CompleteSpace E
inst_6 : IsScalarTower ℝ 𝕜 E
u u' : ℝ → 𝕜
v v' : ℝ → E
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable.{u_2} (ε := E) (fun (x : ℝ) ↦ u x • v' x + u' x • v x) volume a b

Tactic:
exact (hv'.continuousOn_smul hu).add (hu'.smul_continuousOn hv)

Premises used: IntervalIntegrable.smul_continuousOn, IntervalIntegrable.add, IntervalIntegrable.continuousOn_smul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : CompleteSpace E
inst_6 : IsScalarTower ℝ 𝕜 E
u u' : ℝ → 𝕜
v v' : ℝ → E
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
rw : Eq.{u_2 + 1} (α := E) (∫ (x : ℝ) in a..b, u x • v' x) (∫ (x : ℝ) in a..b, u' x • v x + u x • v' x - u' x • v x)
hf : IntervalIntegrable.{u_2} (ε := E) (fun (x : ℝ) ↦ u' x • v x + u x • v' x) volume a b
hg : IntervalIntegrable.{u_2} (ε := E) (fun (x : ℝ) ↦ u' x • v x) volume a b
⊢ ∫ (x : ℝ) in a..b, u x • v' x = u b • v b - u a • v a - ∫ (x : ℝ) in a..b, u' x • v x

Tactic:
rw [← integral_deriv_smul_eq_sub_of_hasDeriv_right hu hv huu' hvv' hu' hv', ← integral_sub]

Premises used: intervalIntegral.integral_deriv_smul_eq_sub_of_hasDeriv_right, intervalIntegral.integral_sub
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : CompleteSpace E
inst_6 : IsScalarTower ℝ 𝕜 E
u u' : ℝ → 𝕜
v v' : ℝ → E
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : ℝ) in a..b, u x • v' x) (∫ (x : ℝ) in a..b, u' x • v x + u x • v' x - u' x • v x)

Tactic:
simp_rw [add_sub_cancel_left]

Premises used: add_sub_cancel_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : CompleteSpace E
inst_6 : IsScalarTower ℝ 𝕜 E
u u' : ℝ → 𝕜
v v' : ℝ → E
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable.{u_2} (ε := E) (fun (x : ℝ) ↦ u' x • v x + u x • v' x) volume a b

Tactic:
(hu'.smul_continuousOn hv).add (hv'.continuousOn_smul hu)

Premises used: IntervalIntegrable.smul_continuousOn, IntervalIntegrable.add, IntervalIntegrable.continuousOn_smul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : CompleteSpace E
inst_6 : IsScalarTower ℝ 𝕜 E
u u' : ℝ → 𝕜
v v' : ℝ → E
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable.{u_2} (ε := E) (fun (x : ℝ) ↦ u' x • v x + u x • v' x) volume a b

Tactic:
exact (hu'.smul_continuousOn hv).add (hv'.continuousOn_smul hu)

Premises used: IntervalIntegrable.smul_continuousOn, IntervalIntegrable.add, IntervalIntegrable.continuousOn_smul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : CompleteSpace E
inst_6 : IsScalarTower ℝ 𝕜 E
u u' : ℝ → 𝕜
v v' : ℝ → E
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable.{u_2} (ε := E) (fun (x : ℝ) ↦ u' x • v x) volume a b

Tactic:
hu'.smul_continuousOn hv

Premises used: IntervalIntegrable.smul_continuousOn
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : CompleteSpace E
inst_6 : IsScalarTower ℝ 𝕜 E
u u' : ℝ → 𝕜
v v' : ℝ → E
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable.{u_2} (ε := E) (fun (x : ℝ) ↦ u' x • v x) volume a b

Tactic:
exact hu'.smul_continuousOn hv

Premises used: IntervalIntegrable.smul_continuousOn
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : CompleteSpace E
inst_6 : IsScalarTower ℝ 𝕜 E
u u' : ℝ → 𝕜
v v' : ℝ → E
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt u (u' x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt v (v' x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ ∫ (x : ℝ) in a..b, u x • v' x = u b • v b - u a • v a - ∫ (x : ℝ) in a..b, u' x • v x

Tactic:
integral_smul_deriv_eq_deriv_smul_of_hasDeriv_right hu hv
        (fun x hx ↦ (huu' x hx).hasDerivWithinAt) (fun x hx ↦ (hvv' x hx).hasDerivWithinAt) hu' hv'

Premises used: HasDerivAt.hasDerivWithinAt, intervalIntegral.integral_smul_deriv_eq_deriv_smul_of_hasDeriv_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : CompleteSpace E
inst_6 : IsScalarTower ℝ 𝕜 E
u u' : ℝ → 𝕜
v v' : ℝ → E
hu : ∀ x ∈ [[a, b]], HasDerivWithinAt u (u' x) [[a, b]] x
hv : ∀ x ∈ [[a, b]], HasDerivWithinAt v (v' x) [[a, b]] x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ ∫ (x : ℝ) in a..b, u x • v' x = u b • v b - u a • v a - ∫ (x : ℝ) in a..b, u' x • v x

Tactic:
integral_smul_deriv_eq_deriv_smul_of_hasDerivAt
    (fun x hx ↦ (hu x hx).continuousWithinAt)
    (fun x hx ↦ (hv x hx).continuousWithinAt)
    (fun x hx ↦ hu x (mem_Icc_of_Ioo hx) |>.hasDerivAt (Icc_mem_nhds hx.1 hx.2))
    (fun x hx ↦ hv x (mem_Icc_of_Ioo hx) |>.hasDerivAt (Icc_mem_nhds hx.1 hx.2))
    hu' hv'

Premises used: intervalIntegral.integral_smul_deriv_eq_deriv_smul_of_hasDerivAt, Set.mem_Icc_of_Ioo, And.right, And.left, HasDerivWithinAt.hasDerivAt, HasDerivWithinAt.continuousWithinAt, Icc_mem_nhds
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : CompleteSpace E
inst_6 : IsScalarTower ℝ 𝕜 E
u u' : ℝ → 𝕜
v v' : ℝ → E
hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x
hv : ∀ x ∈ [[a, b]], HasDerivAt v (v' x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ ∫ (x : ℝ) in a..b, u x • v' x = u b • v b - u a • v a - ∫ (x : ℝ) in a..b, u' x • v x

Tactic:
integral_smul_deriv_eq_deriv_smul_of_hasDerivWithinAt
    (fun x hx ↦ (hu x hx).hasDerivWithinAt) (fun x hx ↦ (hv x hx).hasDerivWithinAt) hu' hv'

Premises used: HasDerivAt.hasDerivWithinAt, intervalIntegral.integral_smul_deriv_eq_deriv_smul_of_hasDerivWithinAt
-- 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 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' [[a, b]]) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) [[a, b]] volume
pos : ∀ (hE : CompleteSpace E), Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (u : ℝ) in f a..f b, g u)
neg :
  ∀ (hE : ¬CompleteSpace E), 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:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- 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 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' [[a, b]]) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) [[a, b]] volume
hE : ¬CompleteSpace E
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (u : ℝ) in f a..f b, g u)

Tactic:
simp [intervalIntegral, integral, hE]

Premises used: intervalIntegral, MeasureTheory.integral
-- 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 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' [[a, b]]) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) [[a, b]] volume
hE : CompleteSpace E
⊢ IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))

Tactic:
rw [hf.image_uIcc, ← intervalIntegrable_iff'] at hg1

Premises used: intervalIntegrable_iff', 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
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' [[a, b]]) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) [[a, b]] volume
hE : CompleteSpace E
hg1₁ : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) [[a, b]] volume

Tactic:
rw [hf.image_uIcc, ← intervalIntegrable_iff'] at hg1

Premises used: intervalIntegrable_iff', 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
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' [[a, b]]) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) [[a, b]] volume
hE : CompleteSpace E
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
⊢ CompleteSpace E

Tactic:
rw [hf.image_uIcc, ← intervalIntegrable_iff'] at hg1

Premises used: intervalIntegrable_iff', 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
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
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]

Tactic:
(continuousOn_primitive_interval' hg1 ?_).comp hf ?_

Premises used: intervalIntegral, ContinuousOn.comp, intervalIntegral.continuousOn_primitive_interval'
-- 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
refine_1 : f a ∈ [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]
refine_2 : MapsTo f [[a, b]] [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]

Tactic:
refine (continuousOn_primitive_interval' hg1 ?_).comp hf ?_

Premises used: ContinuousOn.comp, intervalIntegral.continuousOn_primitive_interval'
-- 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
refine_1 : f a ∈ f '' [[a, b]]
⊢ f a ∈ [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]

Tactic:
rw [← hf.image_uIcc]

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
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
⊢ f a ∈ f '' [[a, b]]

Tactic:
mem_image_of_mem f left_mem_uIcc

Premises used: Set.left_mem_uIcc, Set.mem_image_of_mem
-- 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
⊢ f a ∈ f '' [[a, b]]

Tactic:
exact mem_image_of_mem f left_mem_uIcc

Premises used: Set.left_mem_uIcc, Set.mem_image_of_mem
-- 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
refine_2 : MapsTo f [[a, b]] (f '' [[a, b]])
⊢ MapsTo f [[a, b]] [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]

Tactic:
rw [← hf.image_uIcc]

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
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
⊢ MapsTo f [[a, b]] (f '' [[a, b]])

Tactic:
mapsTo_image _ _

Premises used: Set.mapsTo_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
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
⊢ MapsTo f [[a, b]] (f '' [[a, b]])

Tactic:
exact mapsTo_image _ _

Premises used: Set.mapsTo_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
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
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]

Tactic:
have h_cont : ContinuousOn (fun u ↦ ∫ t in f a..f u, g t) [[a, b]] := by
    refine (continuousOn_primitive_interval' hg1 ?_).comp hf ?_
    · rw [← hf.image_uIcc]; exact mem_image_of_mem f left_mem_uIcc
    · rw [← hf.image_uIcc]; exact mapsTo_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
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 : ℝ
hx : x ∈ Ioo (min a b) (max a b)
obtain :
  ∀ (c : ℝ) (hc : c ∈ Ioo (min a b) x),
    HasDerivWithinAt (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
⊢ HasDerivWithinAt (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x

Tactic:
obtain ⟨c, hc⟩ := nonempty_Ioo.mpr hx.1

Premises used: Iff.mpr, Set.nonempty_Ioo, And.left
-- 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 : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
obtain :
  ∀ (d : ℝ) (hd : d ∈ Ioo x (max a b)),
    HasDerivWithinAt (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
⊢ HasDerivWithinAt (fun (u : ℝ) ↦ ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x

Tactic:
obtain ⟨d, hd⟩ := nonempty_Ioo.mpr hx.2

Premises used: Iff.mpr, Set.nonempty_Ioo, 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 : ℝ
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)
rw : Icc c d ⊆ Ioo (min a b) (max a b)
⊢ [[c, d]] ⊆ Ioo (min a b) (max a b)

Tactic:
rw [uIcc_of_le (hc.2.trans hd.1).le]

Premises used: Set.uIcc_of_le, LT.lt.le, And.right, And.left, LT.lt.trans