awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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 : HSMul.hSMul (β := E) z₁ (∫ (t : ℝ) in 0..1, f' (z₀ + t • z₁)) = ∫ (y : ℝ) in 0..1, z₁ • (f' ∘ γ) y
⊢ HSMul.hSMul (β := E) z₁ (∫ (t : ℝ) in 0..1, f' (z₀ + t • z₁)) = f (z₀ + z₁) - f z₀
have h₁ : f (z₀ + z₁) - f z₀ = (f ∘ γ) 1 - (f ∘ γ) 0
Tactic: convert! (integral_eq_sub_of_hasDerivAt hderiv' hint) using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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
⊢ HSMul.hSMul (β := E) z₁ (∫ (t : ℝ) in 0..1, f' (z₀ + t • z₁)) = ∫ (y : ℝ) in 0..1, z₁ • (f' ∘ γ) y
have h : Eq.{u_3 + 1} (α := E) (∫ (x : ℝ) in 0..1, z₁ • f' (z₀ + x • z₁)) (∫ (y : ℝ) in 0..1, z₁ • (f' ∘ γ) y)
Tactic: simp_rw [← integral_smul, Function.comp_apply, γ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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)
⊢ HSMul.hSMul (β := E) z₁ (∫ (t : ℝ) in 0..1, f' (z₀ + t • z₁)) = ∫ (y : ℝ) in 0..1, z₁ • (f' ∘ γ) y
have h₁ : Eq.{u_3 + 1} (α := E) (∫ (x : ℝ) in 0..1, z₁ • f' (z₀ + x • z₁)) (∫ (y : ℝ) in 0..1, z₁ • f' (γ y))
Tactic: simp_rw [← integral_smul, Function.comp_apply, γ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioc a b) volume
have pos : ∀ (hab : a < b), IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioc a b) volume
Tactic: by_cases hab : a < b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioc a b) volume
have neg : ∀ (hab : ¬a < b), IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioc a b) volume
Tactic: by_cases hab : a < b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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
have pos : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioo a b) volume
Tactic: rw [integrableOn_Ioc_iff_integrableOn_Ioo]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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))
have apply : (fun (x : ℝ) ↦ derivWithin g (Ioi x) x) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo a b))] g'
Tactic: apply (aemeasurable_derivWithin_Ioi g _).congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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'
have refine : ∀ (x : ℝ) (hx : x ∈ Ioo a b), (fun (x : ℝ) ↦ derivWithin g (Ioi x) x) x = g' x
Tactic: refine (ae_restrict_mem measurableSet_Ioo).mono fun x hx => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
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' (Ioo a b) volume
have meas_g' : 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 _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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))
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioo a b) volume
have pos : ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞) ≤ ENNReal.ofReal (g b - g a)
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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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))
⊢ ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞) ≤ ENNReal.ofReal (g b - g a)
have pos : ∀ (H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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∞)
⊢ False
have 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
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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
have refine : @HasFiniteIntegral _ _ _ MeasureSpace.toMeasurableSpace F (Measure.restrict volume (Ioo a b))
Tactic: refine ⟨f.measurable.coe_nnreal_real.aestronglyMeasurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
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)
⊢ False
have intF : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
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
⊢ False
have 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)
Tactic: have A : ∫⁻ x : ℝ in Ioo a b, f x = ENNReal.ofReal (∫ x in Ioo a b, F x) :=
    lintegral_coe_eq_integral _ intF
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
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)
⊢ False
have hf₁ : 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
Cleared hypotheses: hf, intF, A
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x) ≤ g b - g a
have rw : ∫ (x : ℝ) in a..b, F x ≤ g b - g a
Tactic: rw [← integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le hab.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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
have refine_1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Icc a b) volume
Tactic: refine integral_le_sub_of_hasDeriv_right_of_le hab.le hcont hderiv ?_ fun x hx => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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
⊢ ∫ (x : ℝ) in a..b, F x ≤ g b - g a
have refine_2 : ∀ (x : ℝ) (hx : x ∈ Ioo a b), F x ≤ g' x
Tactic: refine integral_le_sub_of_hasDeriv_right_of_le hab.le hcont hderiv ?_ fun x hx => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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 : ℝ
hx : x ∈ Ioo a b
⊢ F x ≤ g' x
have h : g' x = (↑‖g' x‖₊ : ℝ)
Tactic: convert! NNReal.coe_le_coe.2 (fle x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
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)
⊢ False
have B : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x) ≤ g b - g a
Tactic: have B : (∫ x : ℝ in Ioo a b, F x) ≤ g b - g a := by
    rw [← integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le hab.le]
    refine integral_le_sub_of_hasDeriv_right_of_le hab.le hcont hderiv ?_ fun x hx => ?_
    · rwa [integrableOn_Icc_iff_integrableOn_Ioo]
    · convert! NNReal.coe_le_coe.2 (fle x)
      simp only [Real.norm_of_nonneg (g'pos x hx), coe_nnnorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g [[a, b]]
hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ g' x
⊢ IntervalIntegrable g' volume a b
have inl : ∀ (hab : a ≤ b), IntervalIntegrable g' volume a b
Tactic: rcases le_total a b with hab | hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g [[a, b]]
hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ g' x
inl : ∀ (hab : a ≤ b), IntervalIntegrable g' volume a b
⊢ IntervalIntegrable g' volume a b
have inr : ∀ (hab : b ≤ a), IntervalIntegrable g' volume a b
Tactic: rcases le_total a b with hab | hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g [[a, b]]
hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ g' x
hab : a ≤ b
⊢ IntervalIntegrable g' volume a b
have inl : ∀ (hcont : ContinuousOn g (Icc a b)) (hderiv : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x) (hpos : ∀ x ∈ Ioo a b, 0 ≤ g' x),
  IntegrableOn (mα := Real.measurableSpace) g' (Ioc a b) volume
Tactic: simp only [uIcc_of_le, min_eq_left, max_eq_right, IntervalIntegrable, hab,
      Ioc_eq_empty_of_le, integrableOn_empty, and_true] at hcont hderiv hpos ⊢
Cleared hypotheses: hcont, hderiv, hpos
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g [[a, b]]
hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ g' x
hab : b ≤ a
⊢ IntervalIntegrable g' volume a b
have inr : ∀ (hcont : ContinuousOn g (Icc b a)) (hderiv : ∀ x ∈ Ioo b a, HasDerivAt g (g' x) x) (hpos : ∀ x ∈ Ioo b a, 0 ≤ g' x),
  IntegrableOn (mα := Real.measurableSpace) g' (Ioc b a) volume
Tactic: simp only [uIcc_of_ge, min_eq_right, max_eq_left, hab, IntervalIntegrable, Ioc_eq_empty_of_le,
      integrableOn_empty, true_and] at hcont hderiv hpos ⊢
Cleared hypotheses: hcont, hderiv, hpos
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
Goal:
a b : ℝ
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
u v u' v' : ℝ → A
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
⊢ ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a
have apply : IntervalIntegrable.{u_1} (ε := A) (fun (x : ℝ) ↦ u' x * v x + u x * v' x) volume a b
Tactic: apply integral_eq_sub_of_hasDeriv_right (hu.mul hv) fun x hx ↦ (huu' x hx).mul (hvv' x hx)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
Goal:
a b : ℝ
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
u v u' v' : ℝ → A
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
⊢ ∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x
have rw : Eq.{u_1 + 1} (α := A) (∫ (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: rw [← integral_deriv_mul_eq_sub_of_hasDeriv_right hu hv huu' hvv' hu' hv', ← integral_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
Goal:
a b : ℝ
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
u v u' v' : ℝ → A
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_1 + 1} (α := A) (∫ (x : ℝ) in a..b, u x * v' x) (∫ (x : ℝ) in a..b, u' x * v x + u x * v' x - u' x * v x)
⊢ ∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x
have hf : IntervalIntegrable.{u_1} (ε := A) (fun (x : ℝ) ↦ u' x * v x + u x * v' x) volume a b
Tactic: rw [← integral_deriv_mul_eq_sub_of_hasDeriv_right hu hv huu' hvv' hu' hv', ← integral_sub]