awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx_1 : x ∈ Ici a
hx : a < x
⊢ ContinuousWithinAt g (Ici a) x

Tactic:
(hderiv x hx).continuousAt.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, HasDerivAt.continuousAt
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx_1 : x ∈ Ici a
hx : a < x
⊢ ContinuousWithinAt g (Ici a) x

Tactic:
exact (hderiv x hx).continuousAt.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, HasDerivAt.continuousAt
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ ContinuousOn g (Ici a)

Tactic:
have hcont : ContinuousOn g (Ici a) := by
    intro x hx
    rcases hx.out.eq_or_lt with rfl | hx
    · exact hcont
    · exact (hderiv x hx).continuousAt.continuousWithinAt
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioi a) volume

Tactic:
integrableOn_Ioi_of_intervalIntegral_norm_tendsto (l - g a) a (fun x => ?_) tendsto_id ?_

Premises used: Filter.tendsto_id, HSub.hSub, MeasureTheory.integrableOn_Ioi_of_intervalIntegral_norm_tendsto
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
refine_1 : ∀ (x : ℝ), IntegrableOn (mα := measurableSpace) g' (Ioc a (id x)) volume
refine_2 : Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, ‖g' x‖) atTop (𝓝 (l - g a))
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioi a) volume

Tactic:
refine integrableOn_Ioi_of_intervalIntegral_norm_tendsto (l - g a) a (fun x => ?_) tendsto_id ?_

Premises used: Filter.tendsto_id, HSub.hSub, MeasureTheory.integrableOn_Ioi_of_intervalIntegral_norm_tendsto
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
⊢ IntegrableOn (mα := measurableSpace) g' (Ioc a (id x)) volume

Tactic:
intervalIntegral.integrableOn_deriv_of_nonneg (hcont.mono Icc_subset_Ici_self)
      (fun y hy => hderiv y hy.1) fun y hy => g'pos y hy.1

Premises used: intervalIntegral.integrableOn_deriv_of_nonneg, And.left, ContinuousOn.mono, Set.Icc_subset_Ici_self
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
⊢ IntegrableOn (mα := measurableSpace) g' (Ioc a (id x)) volume

Tactic:
exact intervalIntegral.integrableOn_deriv_of_nonneg (hcont.mono Icc_subset_Ici_self)
      (fun y hy => hderiv y hy.1) fun y hy => g'pos y hy.1

Premises used: intervalIntegral.integrableOn_deriv_of_nonneg, And.left, ContinuousOn.mono, Set.Icc_subset_Ici_self
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
apply : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ g x - g a) fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, ‖g' x‖
⊢ Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, ‖g' x‖) atTop (𝓝 (l - g a))

Tactic:
apply Tendsto.congr' _ (hg.sub_const _)

Premises used: Filter.Tendsto.sub_const, Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
h : ∀ (x : ℝ) (hx : x ∈ Ioi a), g x - g a = ∫ (x : ℝ) in a..id x, ‖g' x‖
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ g x - g a) fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, ‖g' x‖

Tactic:
filter_upwards [Ioi_mem_atTop a] with x hx

Premises used: Filter.Ioi_mem_atTop
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
⊢ a ≤ id x

Tactic:
have h'x : a ≤ id x := le_of_lt hx
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
symm : ∫ (y : ℝ) in a..id x, g' y = g x - g a
⊢ g x - g a = ∫ (y : ℝ) in a..id x, g' y

Tactic:
symm
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
apply : IntervalIntegrable g' volume a (id x)
⊢ ∫ (y : ℝ) in a..id x, g' y = g x - g a

Tactic:
apply intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le h'x
        (hcont.mono Icc_subset_Ici_self) fun y hy => hderiv y hy.1

Premises used: intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le, And.left, ContinuousOn.mono, Set.Icc_subset_Ici_self
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
rw : IntegrableOn (mα := measurableSpace) g' (Ioc a (id x)) volume
⊢ IntervalIntegrable g' volume a (id x)

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le h'x]

Premises used: intervalIntegrable_iff_integrableOn_Ioc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ IntegrableOn (mα := measurableSpace) g' (Ioc a (id x)) volume

Tactic:
intervalIntegral.integrableOn_deriv_of_nonneg (hcont.mono Icc_subset_Ici_self)
        (fun y hy => hderiv y hy.1) fun y hy => g'pos y hy.1

Premises used: intervalIntegral.integrableOn_deriv_of_nonneg, And.left, ContinuousOn.mono, Set.Icc_subset_Ici_self
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ IntegrableOn (mα := measurableSpace) g' (Ioc a (id x)) volume

Tactic:
exact intervalIntegral.integrableOn_deriv_of_nonneg (hcont.mono Icc_subset_Ici_self)
        (fun y hy => hderiv y hy.1) fun y hy => g'pos y hy.1

Premises used: intervalIntegral.integrableOn_deriv_of_nonneg, And.left, ContinuousOn.mono, Set.Icc_subset_Ici_self
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
simp_rw :
  Eq (α := ℝ) (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc a (id x))) fun (y : ℝ) ↦ g' y)
    (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc a (id x))) fun (y : ℝ) ↦ ‖g' y‖)
⊢ Eq (α := ℝ) (∫ (y : ℝ) in a..id x, g' y) (∫ (y : ℝ) in a..id x, ‖g' y‖)

Tactic:
simp_rw [intervalIntegral.integral_of_le h'x]

Premises used: intervalIntegral.integral_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ Eq (α := ℝ) (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc a (id x))) fun (y : ℝ) ↦ g' y)
    (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc a (id x))) fun (y : ℝ) ↦ ‖g' y‖)

Tactic:
setIntegral_congr_fun measurableSet_Ioc fun y hy => ?_

Premises used: MeasureTheory.setIntegral_congr_fun, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
refine : ∀ (y : ℝ) (hy : y ∈ Ioc a (id x)), g' y = ‖g' y‖
⊢ Eq (α := ℝ) (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc a (id x))) fun (y : ℝ) ↦ g' y)
    (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc a (id x))) fun (y : ℝ) ↦ ‖g' y‖)

Tactic:
refine setIntegral_congr_fun measurableSet_Ioc fun y hy => ?_

Premises used: MeasureTheory.setIntegral_congr_fun, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
y : ℝ
hy : y ∈ Ioc a (id x)
rw : 0 ≤ g' y
⊢ g' y = |g' y|

Tactic:
rw [abs_of_nonneg]

Premises used: abs_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
y : ℝ
hy : y ∈ Ioc a (id x)
⊢ 0 ≤ g' y

Tactic:
g'pos _ hy.1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
y : ℝ
hy : y ∈ Ioc a (id x)
⊢ 0 ≤ g' y

Tactic:
exact g'pos _ hy.1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
g₁ : g x - g a = ∫ (y : ℝ) in a..id x, g' y
g₂ : Eq (α := ℝ) (∫ (y : ℝ) in a..id x, g' y) (∫ (y : ℝ) in a..id x, ‖g' y‖)
⊢ g x - g a = ∫ (x : ℝ) in a..id x, ‖g' x‖

Tactic:
calc
    g x - g a = ∫ y in a..id x, g' y := by
      symm
      apply intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le h'x
        (hcont.mono Icc_subset_Ici_self) fun y hy => hderiv y hy.1
      rw [intervalIntegrable_iff_integrableOn_Ioc_of_le h'x]
      exact intervalIntegral.integrableOn_deriv_of_nonneg (hcont.mono Icc_subset_Ici_self)
        (fun y hy => hderiv y hy.1) fun y hy => g'pos y hy.1
    _ = ∫ y in a..id x, ‖g' y‖ := by
      simp_rw [intervalIntegral.integral_of_le h'x]
      refine setIntegral_congr_fun measurableSet_Ioc fun y hy => ?_
      dsimp
      rw [abs_of_nonneg]
      exact g'pos _ hy.1

Premises used: id
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioi a) volume

Tactic:
integrableOn_Ioi_deriv_of_nonneg ?_ (fun x hx => hderiv x hx.out.le) g'pos hg

Premises used: MeasureTheory.integrableOn_Ioi_deriv_of_nonneg, Membership.mem.out, LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
refine : ContinuousWithinAt g (Ici a) a
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioi a) volume

Tactic:
refine integrableOn_Ioi_deriv_of_nonneg ?_ (fun x hx => hderiv x hx.out.le) g'pos hg

Premises used: MeasureTheory.integrableOn_Ioi_deriv_of_nonneg, Membership.mem.out, LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ ContinuousWithinAt g (Ici a) a

Tactic:
(hderiv a self_mem_Ici).continuousAt.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, HasDerivAt.continuousAt, Set.self_mem_Ici
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ ContinuousWithinAt g (Ici a) a

Tactic:
exact (hderiv a self_mem_Ici).continuousAt.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, HasDerivAt.continuousAt, Set.self_mem_Ici
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ g' x) = l - g a

Tactic:
integral_Ioi_of_hasDerivAt_of_tendsto hcont hderiv
    (integrableOn_Ioi_deriv_of_nonneg hcont hderiv g'pos hg) hg

Premises used: MeasureTheory.integrableOn_Ioi_deriv_of_nonneg, MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ g' x) = l - g a

Tactic:
integral_Ioi_of_hasDerivAt_of_tendsto' hderiv (integrableOn_Ioi_deriv_of_nonneg' hderiv g'pos hg)
    hg

Premises used: MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto', MeasureTheory.integrableOn_Ioi_deriv_of_nonneg'
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'neg : ∀ x ∈ Ioi a, g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
apply : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (-g') (Measure.restrict volume (Ioi a))
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioi a) volume

Tactic:
apply integrable_neg_iff.1

Premises used: Iff.mp, MeasureTheory.integrable_neg_iff
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'neg : ∀ x ∈ Ioi a, g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (-g') (Measure.restrict volume (Ioi a))

Tactic:
integrableOn_Ioi_deriv_of_nonneg hcont.neg (fun x hx => (hderiv x hx).neg)
    (fun x hx => neg_nonneg_of_nonpos (g'neg x hx)) hg.neg

Premises used: Filter.Tendsto.neg, MeasureTheory.integrableOn_Ioi_deriv_of_nonneg, HasDerivAt.neg, MeasureTheory.IntegrableOn, neg_nonneg_of_nonpos, ContinuousWithinAt.neg
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'neg : ∀ x ∈ Ioi a, g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (-g') (Measure.restrict volume (Ioi a))

Tactic:
exact integrableOn_Ioi_deriv_of_nonneg hcont.neg (fun x hx => (hderiv x hx).neg)
    (fun x hx => neg_nonneg_of_nonpos (g'neg x hx)) hg.neg

Premises used: Filter.Tendsto.neg, MeasureTheory.integrableOn_Ioi_deriv_of_nonneg, HasDerivAt.neg, neg_nonneg_of_nonpos, ContinuousWithinAt.neg
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x
g'neg : ∀ x ∈ Ioi a, g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioi a) volume

Tactic:
integrableOn_Ioi_deriv_of_nonpos ?_ (fun x hx ↦ hderiv x hx.out.le) g'neg hg

Premises used: Membership.mem.out, LT.lt.le, MeasureTheory.integrableOn_Ioi_deriv_of_nonpos
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x
g'neg : ∀ x ∈ Ioi a, g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
refine : ContinuousWithinAt g (Ici a) a
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioi a) volume

Tactic:
refine integrableOn_Ioi_deriv_of_nonpos ?_ (fun x hx ↦ hderiv x hx.out.le) g'neg hg

Premises used: Membership.mem.out, LT.lt.le, MeasureTheory.integrableOn_Ioi_deriv_of_nonpos
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x
g'neg : ∀ x ∈ Ioi a, g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ ContinuousWithinAt g (Ici a) a

Tactic:
(hderiv a self_mem_Ici).continuousAt.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, HasDerivAt.continuousAt, Set.self_mem_Ici
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x
g'neg : ∀ x ∈ Ioi a, g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ ContinuousWithinAt g (Ici a) a

Tactic:
exact (hderiv a self_mem_Ici).continuousAt.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, HasDerivAt.continuousAt, Set.self_mem_Ici
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'neg : ∀ x ∈ Ioi a, g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ g' x) = l - g a

Tactic:
integral_Ioi_of_hasDerivAt_of_tendsto hcont hderiv
    (integrableOn_Ioi_deriv_of_nonpos hcont hderiv g'neg hg) hg

Premises used: MeasureTheory.integrableOn_Ioi_deriv_of_nonpos, MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
g g' : ℝ → ℝ
a l : ℝ
hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x
g'neg : ∀ x ∈ Ioi a, g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ g' x) = l - g a

Tactic:
integral_Ioi_of_hasDerivAt_of_tendsto' hderiv (integrableOn_Ioi_deriv_of_nonpos' hderiv g'neg hg)
    hg

Premises used: MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto', MeasureTheory.integrableOn_Ioi_deriv_of_nonpos'
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
suffices : ∃ (a : E), Tendsto f atBot (𝓝 a)
⊢ Tendsto f atBot (𝓝 (limUnder atBot f))

Tactic:
suffices ∃ a, Tendsto f atBot (𝓝 a) from tendsto_nhds_limUnder this
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
g : ℝ → E := f ∘ fun (x : ℝ) ↦ -x
x : ℝ
hx : x ∈ Ioi (-a)
⊢ -x ∈ Iic a

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
g : ℝ → E := f ∘ fun (x : ℝ) ↦ -x
x : ℝ
hx : x ∈ Ioi (-a)
⊢ -x ∈ Iic a

Tactic:
have : -x ∈ Iic a := by grind
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
g : ℝ → E := f ∘ fun (x : ℝ) ↦ -x
x : ℝ
hx : x ∈ Ioi (-a)
this : -x ∈ Iic a
⊢ HasDerivAt g (-f' (-x)) x

Tactic:
simpa using HasDerivAt.scomp x (hderiv (-x) this) (hasDerivAt_neg' x)

Premises used: hasDerivAt_neg', HasDerivAt.scomp, Neg.neg
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
g : ℝ → E := f ∘ fun (x : ℝ) ↦ -x
⊢ ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x

Tactic:
have hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x := by
    intro x hx
    have : -x ∈ Iic a := by grind
    simpa using HasDerivAt.scomp x (hderiv (-x) this) (hasDerivAt_neg' x)
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
g : ℝ → E := f ∘ fun (x : ℝ) ↦ -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
apply : IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' (-x)) (Ioi (-a)) volume
⊢ Tendsto g atTop (𝓝 (limUnder atTop g))

Tactic:
apply tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi hdg

Premises used: MeasureTheory.tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
g : ℝ → E := f ∘ fun (x : ℝ) ↦ -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
⊢ Ioi (-a) ⊆ Neg.neg ⁻¹' Iic a

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
g : ℝ → E := f ∘ fun (x : ℝ) ↦ -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' (-x)) (Ioi (-a)) volume

Tactic:
exact ((MeasurePreserving.integrableOn_comp_preimage (Measure.measurePreserving_neg _)
      (Homeomorph.neg ℝ).measurableEmbedding).2 f'int.neg).mono_set (by simp)

Premises used: Iff.mpr, MeasureTheory.Measure.measurePreserving_neg, MeasureTheory.MeasurePreserving.integrableOn_comp_preimage, Real, Homeomorph.measurableEmbedding, Homeomorph.neg, MeasureTheory.IntegrableOn.mono_set, MeasureTheory.IntegrableOn.neg