awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
𝕜 : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
f f' : 𝕜 → E
z₀ z₁ : 𝕜
hcont : ContinuousOn.{0, u_3} (Y := E) (fun (t : ℝ) ↦ f' (z₀ + t • z₁)) (Icc 0 1)
hderiv : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)
γ : (t : ℝ) → 𝕜 := fun (t : ℝ) ↦ z₀ + t • z₁
hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1
hderiv' : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) [[0, 1]] t), HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t
h : Eq.{u_3 + 1} (α := E) (∫ (x : ℝ) in 0..1, z₁ • f' (z₀ + x • z₁)) (∫ (y : ℝ) in 0..1, z₁ • (f' ∘ γ) y)
h₁ : Eq.{u_3 + 1} (α := E) (∫ (x : ℝ) in 0..1, z₁ • f' (z₀ + x • z₁)) (∫ (y : ℝ) in 0..1, z₁ • f' (γ y))
⊢ HSMul.hSMul (β := E) z₁ (∫ (t : ℝ) in 0..1, f' (z₀ + t • z₁)) = ∫ (y : ℝ) in 0..1, z₁ • (f' ∘ γ) y

Tactic:
simp_rw [← integral_smul, Function.comp_apply, γ]

Premises used: intervalIntegral.integral_smul, Function.comp_apply
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
𝕜 : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
f f' : 𝕜 → E
z₀ z₁ : 𝕜
hcont : ContinuousOn.{0, u_3} (Y := E) (fun (t : ℝ) ↦ f' (z₀ + t • z₁)) (Icc 0 1)
hderiv : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)
γ : (t : ℝ) → 𝕜 := fun (t : ℝ) ↦ z₀ + t • z₁
hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1
hderiv' : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) [[0, 1]] t), HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t
⊢ f (z₀ + z₁) - f z₀ = (f ∘ γ) 1 - (f ∘ γ) 0

Tactic:
simp only [γ, Function.comp_apply, one_smul, zero_smul, add_zero]

Premises used: one_smul, zero_smul, Function.comp_apply, add_zero
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
pos : ∀ (hab : a < b), IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioc a b) volume
neg : ∀ (hab : ¬a < b), IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioc a b) volume
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioc a b) volume

Tactic:
by_cases hab : a < b
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : ¬a < b
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioc a b) volume

Tactic:
simp [Ioc_eq_empty hab]

Premises used: Set.Ioc_eq_empty
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
pos : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioo a b) volume
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioc a b) volume

Tactic:
rw [integrableOn_Ioc_iff_integrableOn_Ioo]

Premises used: integrableOn_Ioc_iff_integrableOn_Ioo
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
apply : (fun (x : ℝ) ↦ derivWithin g (Ioi x) x) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo a b))] g'
⊢ AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))

Tactic:
apply (aemeasurable_derivWithin_Ioi g _).congr

Premises used: AEMeasurable.congr, aemeasurable_derivWithin_Ioi
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
⊢ (fun (x : ℝ) ↦ derivWithin g (Ioi x) x) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo a b))] g'

Tactic:
(ae_restrict_mem measurableSet_Ioo).mono fun x hx => ?_

Premises used: MeasureTheory.ae_restrict_mem, Filter.EventuallyEq, Filter.Eventually.mono, measurableSet_Ioo
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
refine : ∀ (x : ℝ) (hx : x ∈ Ioo a b), (fun (x : ℝ) ↦ derivWithin g (Ioi x) x) x = g' x
⊢ (fun (x : ℝ) ↦ derivWithin g (Ioi x) x) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo a b))] g'

Tactic:
refine (ae_restrict_mem measurableSet_Ioo).mono fun x hx => ?_

Premises used: MeasureTheory.ae_restrict_mem, Filter.Eventually.mono, measurableSet_Ioo
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
x : ℝ
hx : x ∈ Ioo a b
⊢ (fun (x : ℝ) ↦ derivWithin g (Ioi x) x) x = g' x

Tactic:
(hderiv x hx).derivWithin (uniqueDiffWithinAt_Ioi _)

Premises used: HasDerivWithinAt.derivWithin, uniqueDiffWithinAt_Ioi
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
x : ℝ
hx : x ∈ Ioo a b
⊢ (fun (x : ℝ) ↦ derivWithin g (Ioi x) x) x = g' x

Tactic:
exact (hderiv x hx).derivWithin (uniqueDiffWithinAt_Ioi _)

Premises used: HasDerivWithinAt.derivWithin, uniqueDiffWithinAt_Ioi
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
⊢ AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))

Tactic:
have meas_g' : AEMeasurable g' (volume.restrict (Ioo a b)) := by
    apply (aemeasurable_derivWithin_Ioi g _).congr
    refine (ae_restrict_mem measurableSet_Ioo).mono fun x hx => ?_
    exact (hderiv x hx).derivWithin (uniqueDiffWithinAt_Ioi _)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
pos : ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞) ≤ ENNReal.ofReal (g b - g a)
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioo a b) volume

Tactic:
suffices H : (∫⁻ x in Ioo a b, ‖g' x‖₊) ≤ ENNReal.ofReal (g b - g a) from
    ⟨meas_g'.aestronglyMeasurable, H.trans_lt ENNReal.ofReal_lt_top⟩
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
pos : ∀ (H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)), False
⊢ ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞) ≤ ENNReal.ofReal (g b - g a)

Tactic:
by_contra! H
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)
⊢ ∃ (f : SimpleFunc ℝ ℝ≥0),
    (∀ (x : ℝ), (f : (a : ℝ) → ℝ≥0) x ≤ ‖g' x‖₊) ∧
      ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) < ∞ ∧
        ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞)

Tactic:
exists_lt_lintegral_simpleFunc_of_lt_lintegral H

Premises used: MeasureTheory.exists_lt_lintegral_simpleFunc_of_lt_lintegral
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)
pos :
  ∀ (f : SimpleFunc ℝ ℝ≥0) (fle : ∀ (x : ℝ), (f : (a : ℝ) → ℝ≥0) x ≤ ‖g' x‖₊)
    (fint : ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) < ∞)
    (hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞)), False
⊢ False

Tactic:
obtain ⟨f, fle, fint, hf⟩ :
    ∃ f : SimpleFunc ℝ ℝ≥0,
      (∀ x, f x ≤ ‖g' x‖₊) ∧
        (∫⁻ x : ℝ in Ioo a b, f x) < ∞ ∧ ENNReal.ofReal (g b - g a) < ∫⁻ x : ℝ in Ioo a b, f x :=
    exists_lt_lintegral_simpleFunc_of_lt_lintegral H

Premises used: Real, ENNReal.ofReal, HSub.hSub, MeasureTheory.SimpleFunc, NNReal, MeasureTheory.exists_lt_lintegral_simpleFunc_of_lt_lintegral, Set.Ioo
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), (f : (a : ℝ) → ℝ≥0) x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) < ∞
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞)
F : ℝ → ℝ := NNReal.toReal ∘ (⇑f : (a : ℝ) → ℝ≥0)
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Ioo a b) volume

Tactic:
⟨f.measurable.coe_nnreal_real.aestronglyMeasurable, ?_⟩

Premises used: Measurable.aestronglyMeasurable, MeasureTheory.SimpleFunc.measurable, MeasureTheory.Integrable, MeasureTheory.IntegrableOn, Measurable.coe_nnreal_real, And.intro
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), (f : (a : ℝ) → ℝ≥0) x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) < ∞
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞)
F : ℝ → ℝ := NNReal.toReal ∘ (⇑f : (a : ℝ) → ℝ≥0)
refine : @HasFiniteIntegral _ _ _ MeasureSpace.toMeasurableSpace F (Measure.restrict volume (Ioo a b))
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Ioo a b) volume

Tactic:
refine ⟨f.measurable.coe_nnreal_real.aestronglyMeasurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), (f : (a : ℝ) → ℝ≥0) x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) < ∞
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞)
F : ℝ → ℝ := NNReal.toReal ∘ (⇑f : (a : ℝ) → ℝ≥0)
⊢ @HasFiniteIntegral _ _ _ MeasureSpace.toMeasurableSpace F (Measure.restrict volume (Ioo a b))

Tactic:
simpa only [F, hasFiniteIntegral_iff_enorm, comp_apply, NNReal.enorm_eq] using fint

Premises used: NNReal.enorm_eq, Function.comp_apply, MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), (f : (a : ℝ) → ℝ≥0) x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) < ∞
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞)
F : ℝ → ℝ := NNReal.toReal ∘ (⇑f : (a : ℝ) → ℝ≥0)
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Ioo a b) volume

Tactic:
have intF : IntegrableOn F (Ioo a b) := by
    refine ⟨f.measurable.coe_nnreal_real.aestronglyMeasurable, ?_⟩
    simpa only [F, hasFiniteIntegral_iff_enorm, comp_apply, NNReal.enorm_eq] using fint
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), (f : (a : ℝ) → ℝ≥0) x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) < ∞
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞)
F : ℝ → ℝ := NNReal.toReal ∘ (⇑f : (a : ℝ) → ℝ≥0)
intF : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Ioo a b) volume
⊢ ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)

Tactic:
have A : ∫⁻ x : ℝ in Ioo a b, f x = ENNReal.ofReal (∫ x in Ioo a b, F x) :=
    lintegral_coe_eq_integral _ intF
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), (f : (a : ℝ) → ℝ≥0) x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) < ∞
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞)
F : ℝ → ℝ := NNReal.toReal ∘ (⇑f : (a : ℝ) → ℝ≥0)
intF : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Ioo a b) volume
A :
  ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
⊢ ENNReal.ofReal (g b - g a) <
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)

Tactic:
rw [A] at hf
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), (f : (a : ℝ) → ℝ≥0) x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) < ∞
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞)
F : ℝ → ℝ := NNReal.toReal ∘ (⇑f : (a : ℝ) → ℝ≥0)
intF : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Ioo a b) volume
A :
  ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
hf₁ :
  ENNReal.ofReal (g b - g a) <
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Ioo a b) volume

Tactic:
rw [A] at hf
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), (f : (a : ℝ) → ℝ≥0) x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) < ∞
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞)
F : ℝ → ℝ := NNReal.toReal ∘ (⇑f : (a : ℝ) → ℝ≥0)
intF : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Ioo a b) volume
A :
  ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
hf₁ :
  ENNReal.ofReal (g b - g a) <
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
intF₁ : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Ioo a b) volume
⊢ ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)

Tactic:
rw [A] at hf
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), (f : (a : ℝ) → ℝ≥0) x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) < ∞
F : ℝ → ℝ := NNReal.toReal ∘ (⇑f : (a : ℝ) → ℝ≥0)
hf :
  ENNReal.ofReal (g b - g a) <
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
intF : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Ioo a b) volume
A :
  ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
rw : ∫ (x : ℝ) in a..b, F x ≤ g b - g a
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x) ≤ g b - g a

Tactic:
rw [← integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le hab.le]

Premises used: LT.lt.le, MeasureTheory.integral_Ioc_eq_integral_Ioo, intervalIntegral.integral_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), (f : (a : ℝ) → ℝ≥0) x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) < ∞
F : ℝ → ℝ := NNReal.toReal ∘ (⇑f : (a : ℝ) → ℝ≥0)
hf :
  ENNReal.ofReal (g b - g a) <
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
intF : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Ioo a b) volume
A :
  ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
⊢ ∫ (x : ℝ) in a..b, F x ≤ g b - g a

Tactic:
integral_le_sub_of_hasDeriv_right_of_le hab.le hcont hderiv ?_ fun x hx => ?_

Premises used: LT.lt.le, intervalIntegral.integral_le_sub_of_hasDeriv_right_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), (f : (a : ℝ) → ℝ≥0) x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) < ∞
F : ℝ → ℝ := NNReal.toReal ∘ (⇑f : (a : ℝ) → ℝ≥0)
hf :
  ENNReal.ofReal (g b - g a) <
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
intF : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Ioo a b) volume
A :
  ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
refine_1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Icc a b) volume
refine_2 : ∀ (x : ℝ) (hx : x ∈ Ioo a b), F x ≤ g' x
⊢ ∫ (x : ℝ) in a..b, F x ≤ g b - g a

Tactic:
refine integral_le_sub_of_hasDeriv_right_of_le hab.le hcont hderiv ?_ fun x hx => ?_

Premises used: LT.lt.le, intervalIntegral.integral_le_sub_of_hasDeriv_right_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), (f : (a : ℝ) → ℝ≥0) x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) < ∞
F : ℝ → ℝ := NNReal.toReal ∘ (⇑f : (a : ℝ) → ℝ≥0)
hf :
  ENNReal.ofReal (g b - g a) <
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
intF : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Ioo a b) volume
A :
  ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
refine_1 refine_1₁ refine_1₂ refine_1₃ : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Ioo a b) volume
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Icc a b) volume

Tactic:
rwa [integrableOn_Icc_iff_integrableOn_Ioo]

Premises used: integrableOn_Icc_iff_integrableOn_Ioo