awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
hf : ContDiff ℝ 1 f
h'f : HasCompactSupport f
x : ℝ
I : F →L[ℝ] Completion F := Completion.toComplL
f' : ℝ → Completion F := (⇑I : (a : F) → Completion F) ∘ f
hf' : ContDiff ℝ 1 f'
h'f' : HasCompactSupport f'
this : ‖f' x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f' y‖ₑ
⊢ ‖f x‖ₑ = ‖f' x‖ₑ

Tactic:
simp [f', I, Completion.enorm_coe]

Premises used: UniformSpace.Completion.enorm_coe
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
hf : ContDiff ℝ 1 f
h'f : HasCompactSupport f
x : ℝ
I : F →L[ℝ] Completion F := Completion.toComplL
f' : ℝ → Completion F := (⇑I : (a : F) → Completion F) ∘ f
hf' : ContDiff ℝ 1 f'
h'f' : HasCompactSupport f'
this : ‖f' x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f' y‖ₑ
y : ℝ
h :
  ‖deriv f y‖ₑ =
    enorm (E := Completion F)
      ((fderiv ℝ (⇑I : (a : F) → Completion F) (f y) : (a : F) → Completion F) (deriv f y) : Completion F)
⊢ ‖deriv f y‖ₑ = ‖deriv f' y‖ₑ

Tactic:
rw [fderiv_comp_deriv _ I.differentiableAt (hf.differentiable one_ne_zero _)]

Premises used: fderiv_comp_deriv, ContinuousLinearMap.differentiableAt, ContDiff.differentiable, one_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
hf : ContDiff ℝ 1 f
h'f : HasCompactSupport f
x : ℝ
I : F →L[ℝ] Completion F := Completion.toComplL
f' : ℝ → Completion F := (⇑I : (a : F) → Completion F) ∘ f
hf' : ContDiff ℝ 1 f'
h'f' : HasCompactSupport f'
this : ‖f' x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f' y‖ₑ
y : ℝ
h : ‖deriv f y‖ₑ = enorm (E := Completion F) ((I : (a : F) → Completion F) (deriv f y) : Completion F)
⊢ ‖deriv f y‖ₑ =
    enorm (E := Completion F)
      ((fderiv ℝ (⇑I : (a : F) → Completion F) (f y) : (a : F) → Completion F) (deriv f y) : Completion F)

Tactic:
simp only [ContinuousLinearMap.fderiv]

Premises used: ContinuousLinearMap.fderiv
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
hf : ContDiff ℝ 1 f
h'f : HasCompactSupport f
x : ℝ
I : F →L[ℝ] Completion F := Completion.toComplL
f' : ℝ → Completion F := (⇑I : (a : F) → Completion F) ∘ f
hf' : ContDiff ℝ 1 f'
h'f' : HasCompactSupport f'
this : ‖f' x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f' y‖ₑ
y : ℝ
⊢ ‖deriv f y‖ₑ = enorm (E := Completion F) ((I : (a : F) → Completion F) (deriv f y) : Completion F)

Tactic:
simp [I]
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
m n : E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f' volume
hbot : Tendsto f atBot (𝓝 m)
htop : Tendsto f atTop (𝓝 n)
rw : f 0 - m + (n - f 0) = n - m
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f' x) = n - m

Tactic:
rw [← setIntegral_univ, ← Set.Iic_union_Ioi (a := 0),
    setIntegral_union (Iic_disjoint_Ioi le_rfl) measurableSet_Ioi hf'.integrableOn hf'.integrableOn,
    integral_Iic_of_hasDerivAt_of_tendsto' (fun x _ ↦ hderiv x) hf'.integrableOn hbot,
    integral_Ioi_of_hasDerivAt_of_tendsto' (fun x _ ↦ hderiv x) hf'.integrableOn htop]

Premises used: MeasureTheory.setIntegral_union, le_rfl, Set.Iic_disjoint_Ioi, MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto', measurableSet_Ioi, Set.Iic_union_Ioi, MeasureTheory.Integrable.integrableOn, MeasureTheory.integral_Iic_of_hasDerivAt_of_tendsto', MeasureTheory.setIntegral_univ
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
m n : E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f' volume
hbot : Tendsto f atBot (𝓝 m)
htop : Tendsto f atTop (𝓝 n)
⊢ f 0 - m + (n - f 0) = n - m

Tactic:
abel
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f' volume
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
pos :
  ∀ (hE : CompleteSpace E),
    Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f' x) 0
neg :
  ∀ (hE : ¬CompleteSpace E),
    Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f' x) 0
⊢ Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f' x) 0

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f' volume
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hE : ¬CompleteSpace E
⊢ Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f' x) 0

Tactic:
simp [integral, hE]

Premises used: MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f' volume
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hE : CompleteSpace E
⊢ Tendsto f atBot (𝓝 0)

Tactic:
have A : Tendsto f atBot (𝓝 0) :=
    tendsto_zero_of_hasDerivAt_of_integrableOn_Iic (a := 0) (fun x _hx ↦ hderiv x)
      hf'.integrableOn hf.integrableOn
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f' volume
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hE : CompleteSpace E
A : Tendsto f atBot (𝓝 0)
⊢ Tendsto f atTop (𝓝 0)

Tactic:
have B : Tendsto f atTop (𝓝 0) :=
    tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi (a := 0) (fun x _hx ↦ hderiv x)
      hf'.integrableOn hf.integrableOn
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f' volume
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hE : CompleteSpace E
A : Tendsto f atBot (𝓝 0)
B : Tendsto f atTop (𝓝 0)
⊢ Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f' x) 0

Tactic:
simpa using integral_of_hasDerivAt_of_tendsto hderiv hf' A B

Premises used: MeasureTheory.integral_of_hasDerivAt_of_tendsto
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
rw : Ioo a (max a b) ⊆ Ioi a
⊢ Ioo (min a b) (max a b) ⊆ Ioi a

Tactic:
rw [min_eq_left hb.le]

Premises used: LT.lt.le, min_eq_left
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
⊢ Ioo a (max a b) ⊆ Ioi a

Tactic:
Ioo_subset_Ioi_self

Premises used: Set.Ioo_subset_Ioi_self
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
⊢ Ioo a (max a b) ⊆ Ioi a

Tactic:
exact Ioo_subset_Ioi_self

Premises used: Set.Ioo_subset_Ioi_self
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
⊢ Ioo (min a b) (max a b) ⊆ Ioi a

Tactic:
have i1 : Ioo (min a b) (max a b) ⊆ Ioi a := by
      rw [min_eq_left hb.le]
      exact Ioo_subset_Ioi_self
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
rw : Icc a b ⊆ Ici a
⊢ [[a, b]] ⊆ Ici a

Tactic:
rw [uIcc_of_le hb.le]

Premises used: Set.uIcc_of_le, LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
⊢ Icc a b ⊆ Ici a

Tactic:
Icc_subset_Ici_self

Premises used: Set.Icc_subset_Ici_self
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
⊢ Icc a b ⊆ Ici a

Tactic:
exact Icc_subset_Ici_self

Premises used: Set.Icc_subset_Ici_self
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
⊢ [[a, b]] ⊆ Ici a

Tactic:
have i2 : [[a, b]] ⊆ Ici a := by rw [uIcc_of_le hb.le]; exact Icc_subset_Ici_self
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
i2 : [[a, b]] ⊆ Ici a
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (u : ℝ) in f a..f b, g u)

Tactic:
intervalIntegral.integral_deriv_smul_comp''' (hf.mono i2)
        (fun x hx => hff' x <| mem_of_mem_of_subset hx i1) (hg_cont.mono <| image_mono ?_)
        (hg1.mono_set <| image_mono ?_) (hg2.mono_set i2)

Premises used: Set.image_mono, MeasureTheory.IntegrableOn.mono_set, Set.mem_of_mem_of_subset, ContinuousOn.mono, intervalIntegral.integral_deriv_smul_comp'''
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
i2 : [[a, b]] ⊆ Ici a
refine_1 : Ioo (min a b) (max a b) ⊆ Ioi a
refine_2 : [[a, b]] ⊆ Ici a
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (u : ℝ) in f a..f b, g u)

Tactic:
refine
      intervalIntegral.integral_deriv_smul_comp''' (hf.mono i2)
        (fun x hx => hff' x <| mem_of_mem_of_subset hx i1) (hg_cont.mono <| image_mono ?_)
        (hg1.mono_set <| image_mono ?_) (hg2.mono_set i2)

Premises used: Set.image_mono, MeasureTheory.IntegrableOn.mono_set, Set.mem_of_mem_of_subset, ContinuousOn.mono, intervalIntegral.integral_deriv_smul_comp'''
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
i2 : [[a, b]] ⊆ Ici a
⊢ Ioo (min a b) (max a b) ⊆ Ioi a

Tactic:
assumption
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
i2 : [[a, b]] ⊆ Ici a
⊢ [[a, b]] ⊆ Ici a

Tactic:
assumption
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ici a) volume
⊢ ∀ (b : ℝ), 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:
have eq : ∀ b : ℝ, a < b → (∫ x in a..b, f' x • (g ∘ f) x) = ∫ u in f a..f b, g u := fun b hb ↦ by
    have i1 : Ioo (min a b) (max a b) ⊆ Ioi a := by
      rw [min_eq_left hb.le]
      exact Ioo_subset_Ioi_self
    have i2 : [[a, b]] ⊆ Ici a := by rw [uIcc_of_le hb.le]; exact Icc_subset_Ici_self
    refine
      intervalIntegral.integral_deriv_smul_comp''' (hf.mono i2)
        (fun x hx => hff' x <| mem_of_mem_of_subset hx i1) (hg_cont.mono <| image_mono ?_)
        (hg1.mono_set <| image_mono ?_) (hg2.mono_set i2) <;> assumption
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ici a) volume
eq : ∀ (b : ℝ), a < b → Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (u : ℝ) in f a..f b, g u)
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ioi a) volume

Tactic:
rw [integrableOn_Ici_iff_integrableOn_Ioi] at hg2

Premises used: integrableOn_Ici_iff_integrableOn_Ioi
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ici a) volume
eq : ∀ (b : ℝ), a < b → Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (u : ℝ) in f a..f b, g u)
hg2₁ :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ioi a) volume
⊢ ∀ (b : ℝ), 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 [integrableOn_Ici_iff_integrableOn_Ioi] at hg2

Premises used: integrableOn_Ici_iff_integrableOn_Ioi
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ioi a) volume
eq : ∀ (b : ℝ), a < b → Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (u : ℝ) in f a..f b, g u)
⊢ Tendsto.{0, u_1} (β := E) (fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, f' x • (g ∘ f) x) atTop
    (𝓝 (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ f' x • (g ∘ f) x))

Tactic:
have t2 := intervalIntegral_tendsto_integral_Ioi _ hg2 tendsto_id
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ioi a) volume
eq : ∀ (b : ℝ), a < b → Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (u : ℝ) in f a..f b, g u)
t2 :
  Tendsto.{0, u_1} (β := E) (fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, f' x • (g ∘ f) x) atTop
    (𝓝 (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ f' x • (g ∘ f) x))
⊢ Ioi (f a) ⊆ f '' Ici a

Tactic:
have : Ioi (f a) ⊆ f '' Ici a :=
    Ioi_subset_Ici_self.trans <|
      IsPreconnected.intermediate_value_Ici isPreconnected_Ici self_mem_Ici
        (le_principal_iff.mpr <| Ici_mem_atTop _) hf hft
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ioi a) volume
eq : ∀ (b : ℝ), a < b → Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (u : ℝ) in f a..f b, g u)
t2 :
  Tendsto.{0, u_1} (β := E) (fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, f' x • (g ∘ f) x) atTop
    (𝓝 (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ f' x • (g ∘ f) x))
this : Ioi (f a) ⊆ f '' Ici a
⊢ Tendsto.{0, u_1} (β := E) ((fun (i : ℝ) ↦ ∫ (x : ℝ) in f a..id i, g x) ∘ f) atTop
    (𝓝 (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi (f a))) fun (x : ℝ) ↦ g x))

Tactic:
have t1 := (intervalIntegral_tendsto_integral_Ioi _ (hg1.mono_set this) tendsto_id).comp hft
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ioi a) volume
eq : ∀ (b : ℝ), a < b → Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (u : ℝ) in f a..f b, g u)
t2 :
  Tendsto.{0, u_1} (β := E) (fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, f' x • (g ∘ f) x) atTop
    (𝓝 (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ f' x • (g ∘ f) x))
this : Ioi (f a) ⊆ f '' Ici a
t1 :
  Tendsto.{0, u_1} (β := E) ((fun (i : ℝ) ↦ ∫ (x : ℝ) in f a..id i, g x) ∘ f) atTop
    (𝓝 (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi (f a))) fun (x : ℝ) ↦ g x))
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ f' x • (g ∘ f) x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (f a))) fun (u : ℝ) ↦ g u)

Tactic:
tendsto_nhds_unique (Tendsto.congr' (eventuallyEq_of_mem (Ioi_mem_atTop a) eq) t2) t1

Premises used: Filter.eventuallyEq_of_mem, Filter.Ioi_mem_atTop, Filter.Tendsto.congr', tendsto_nhds_unique