awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ℝ → E} (hfc : ContinuousOn f (Icc a b))
    (hfd : DifferentiableOn ℝ f (Ioo a b)) (hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) (hE : CompleteSpace E),
    ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
hE : ¬CompleteSpace E
g : ℝ → UniformSpace.Completion E := UniformSpace.Completion.coe' ∘ f
hg : g = UniformSpace.Completion.coe' ∘ f
hgc : ContinuousOn g (Icc a b)
hgd : DifferentiableOn ℝ g (Ioo a b)
t : ℝ
ht : t ∈ Ioo a b
⊢ deriv g t = (↑(deriv f t) : UniformSpace.Completion E)
have this₁ : HasFDerivAt (𝕜 := ℝ) UniformSpace.Completion.coe' UniformSpace.Completion.toComplL (f t)
Tactic: have : HasFDerivAt (𝕜 := ℝ) (↑) UniformSpace.Completion.toComplL (f t) := by
        rw [← UniformSpace.Completion.coe_toComplL (𝕜 := ℝ)]
        exact (UniformSpace.Completion.toComplL (E := E) (𝕜 := ℝ)).hasFDerivAt
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
this_1 :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ℝ → E} (hfc : ContinuousOn f (Icc a b))
    (hfd : DifferentiableOn ℝ f (Ioo a b)) (hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) (hE : CompleteSpace E),
    ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
hE : ¬CompleteSpace E
g : ℝ → UniformSpace.Completion E := UniformSpace.Completion.coe' ∘ f
hg : g = UniformSpace.Completion.coe' ∘ f
hgc : ContinuousOn g (Icc a b)
hgd : DifferentiableOn ℝ g (Ioo a b)
t : ℝ
ht : t ∈ Ioo a b
this : HasFDerivAt (𝕜 := ℝ) UniformSpace.Completion.coe' UniformSpace.Completion.toComplL (f t)
⊢ deriv g t = (↑(deriv f t) : UniformSpace.Completion E)
have hdft : HasDerivAt f (deriv f t) t
Tactic: have hdft : HasDerivAt f (deriv f t) t := hfd.hasDerivAt <| Ioo_mem_nhds ht.1 ht.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
this_1 :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ℝ → E} (hfc : ContinuousOn f (Icc a b))
    (hfd : DifferentiableOn ℝ f (Ioo a b)) (hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) (hE : CompleteSpace E),
    ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
hE : ¬CompleteSpace E
g : ℝ → UniformSpace.Completion E := UniformSpace.Completion.coe' ∘ f
hg : g = UniformSpace.Completion.coe' ∘ f
hgc : ContinuousOn g (Icc a b)
hgd : DifferentiableOn ℝ g (Ioo a b)
t : ℝ
ht : t ∈ Ioo a b
this : HasFDerivAt (𝕜 := ℝ) UniformSpace.Completion.coe' UniformSpace.Completion.toComplL (f t)
hdft : HasDerivAt f (deriv f t) t
rw :
  Eq (α := UniformSpace.Completion E) (deriv (UniformSpace.Completion.coe' ∘ f) t)
    (↑(deriv f t) : UniformSpace.Completion E)
⊢ deriv g t = (↑(deriv f t) : UniformSpace.Completion E)
have rw₁ : Eq (α := UniformSpace.Completion E)
  ((UniformSpace.Completion.toComplL : (a : E) → UniformSpace.Completion E) (deriv f t) : UniformSpace.Completion E)
  ((↑(deriv f t) : UniformSpace.Completion E) : UniformSpace.Completion E)
Tactic: rw [hg, (this.comp_hasDerivAt t hdft).deriv, UniformSpace.Completion.coe_toComplL]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
this_1 :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ℝ → E} (hfc : ContinuousOn f (Icc a b))
    (hfd : DifferentiableOn ℝ f (Ioo a b)) (hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) (hE : CompleteSpace E),
    ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
hE : ¬CompleteSpace E
g : ℝ → UniformSpace.Completion E := UniformSpace.Completion.coe' ∘ f
hg : g = UniformSpace.Completion.coe' ∘ f
hgc : ContinuousOn g (Icc a b)
hgd : DifferentiableOn ℝ g (Ioo a b)
t : ℝ
ht : t ∈ Ioo a b
this : HasFDerivAt (𝕜 := ℝ) UniformSpace.Completion.coe' UniformSpace.Completion.toComplL (f t)
hdft : HasDerivAt f (deriv f t) t
rw :
  Eq (α := UniformSpace.Completion E) (deriv (UniformSpace.Completion.coe' ∘ f) t)
    (↑(deriv f t) : UniformSpace.Completion E)
rw₁ :
  Eq (α := UniformSpace.Completion E)
    ((UniformSpace.Completion.toComplL : (a : E) → UniformSpace.Completion E) (deriv f t) : UniformSpace.Completion E)
    ((↑(deriv f t) : UniformSpace.Completion E) : UniformSpace.Completion E)
⊢ deriv g t = (↑(deriv f t) : UniformSpace.Completion E)
have rw₂ : Eq (α := UniformSpace.Completion E) (↑(deriv f t) : UniformSpace.Completion E)
  (↑(deriv f t) : UniformSpace.Completion E)
Tactic: rw [hg, (this.comp_hasDerivAt t hdft).deriv, UniformSpace.Completion.coe_toComplL]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ℝ → E} (hfc : ContinuousOn f (Icc a b))
    (hfd : DifferentiableOn ℝ f (Ioo a b)) (hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) (hE : CompleteSpace E),
    ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
hE : ¬CompleteSpace E
g : ℝ → UniformSpace.Completion E := UniformSpace.Completion.coe' ∘ f
hg : g = UniformSpace.Completion.coe' ∘ f
hgc : ContinuousOn g (Icc a b)
hgd : DifferentiableOn ℝ g (Ioo a b)
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
have hdg : ∀ (t : ℝ) (ht : t ∈ Ioo a b), deriv g t = (↑(deriv f t) : UniformSpace.Completion E)
Tactic: have hdg t (ht : t ∈ Ioo a b) : deriv g t = deriv f t := by
      have : HasFDerivAt (𝕜 := ℝ) (↑) UniformSpace.Completion.toComplL (f t) := by
        rw [← UniformSpace.Completion.coe_toComplL (𝕜 := ℝ)]
        exact (UniformSpace.Completion.toComplL (E := E) (𝕜 := ℝ)).hasFDerivAt
      have hdft : HasDerivAt f (deriv f t) t := hfd.hasDerivAt <| Ioo_mem_nhds ht.1 ht.2
      rw [hg, (this.comp_hasDerivAt t hdft).deriv, UniformSpace.Completion.coe_toComplL]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ℝ → E} (hfc : ContinuousOn f (Icc a b))
    (hfd : DifferentiableOn ℝ f (Ioo a b)) (hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) (hE : CompleteSpace E),
    ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
hE : ¬CompleteSpace E
g : ℝ → UniformSpace.Completion E := UniformSpace.Completion.coe' ∘ f
hg : g = UniformSpace.Completion.coe' ∘ f
hgc : ContinuousOn g (Icc a b)
hgd : DifferentiableOn ℝ g (Ioo a b)
hdg : ∀ (t : ℝ) (ht : t ∈ Ioo a b), deriv g t = (↑(deriv f t) : UniformSpace.Completion E)
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
have hgn : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv g t‖ ≤ B t
Tactic: have hgn : ∀ᵐ t, t ∈ Ioo a b → ‖deriv g t‖ ≤ B t :=
      hfB.mono fun t htB ht ↦ by
        simpa only [hdg t ht, UniformSpace.Completion.norm_coe] using htB ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
⊢ (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
have rwa : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] B
Tactic: rwa [uIoc_of_le hab, ← Measure.restrict_congr_set Ioo_ae_eq_Ioc, EventuallyLE,
        ae_restrict_iff' measurableSet_Ioo]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
rwa : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] B
⊢ (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
have rwa₁ : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo a b))] B
Tactic: rwa [uIoc_of_le hab, ← Measure.restrict_congr_set Ioo_ae_eq_Ioc, EventuallyLE,
        ae_restrict_iff' measurableSet_Ioo]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
rwa : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] B
rwa₁ : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo a b))] B
⊢ (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
have rwa₂ : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioo a b), ‖deriv f x‖ ≤ B x
Tactic: rwa [uIoc_of_le hab, ← Measure.restrict_congr_set Ioo_ae_eq_Ioc, EventuallyLE,
        ae_restrict_iff' measurableSet_Ioo]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (hypothesis)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
have hfB' : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
Tactic: have hfB' : (‖deriv f ·‖) ≤ᵐ[volume.restrict (uIoc a b)] B := by
    rwa [uIoc_of_le hab, ← Measure.restrict_congr_set Ioo_ae_eq_Ioc, EventuallyLE,
        ae_restrict_iff' measurableSet_Ioo]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
have rw : norm.{u_1} (E := E) (∫ (y : ℝ) in a..b, deriv f y) ≤ ∫ (t : ℝ) in a..b, B t
Tactic: rw [← intervalIntegral.integral_eq_sub_of_hasDeriv_right (f' := deriv f)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
rw : norm.{u_1} (E := E) (∫ (y : ℝ) in a..b, deriv f y) ≤ ∫ (t : ℝ) in a..b, B t
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
have hcont : ContinuousOn f (uIcc a b)
Tactic: rw [← intervalIntegral.integral_eq_sub_of_hasDeriv_right (f' := deriv f)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
rw : norm.{u_1} (E := E) (∫ (y : ℝ) in a..b, deriv f y) ≤ ∫ (t : ℝ) in a..b, B t
hcont : ContinuousOn f (uIcc a b)
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
have hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (deriv f x) (Ioi x) x
Tactic: rw [← intervalIntegral.integral_eq_sub_of_hasDeriv_right (f' := deriv f)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
rw : norm.{u_1} (E := E) (∫ (y : ℝ) in a..b, deriv f y) ≤ ∫ (t : ℝ) in a..b, B t
hcont : ContinuousOn f (uIcc a b)
hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (deriv f x) (Ioi x) x
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
have hint : IntervalIntegrable (deriv f) volume a b
Tactic: rw [← intervalIntegral.integral_eq_sub_of_hasDeriv_right (f' := deriv f)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
⊢ norm.{u_1} (E := E) (∫ (y : ℝ) in a..b, deriv f y) ≤ ∫ (t : ℝ) in a..b, B t
have apply : ∀ᵐ (t : ℝ), t ∈ Ioc a b → ‖deriv f t‖ ≤ B t
Tactic: apply intervalIntegral.norm_integral_le_of_norm_le hab _ hBi
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
⊢ ∀ᵐ (t : ℝ), t ∈ Ioc a b → ‖deriv f t‖ ≤ B t
have rwa : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioc a b), ‖deriv f x‖ ≤ B x
Tactic: rwa [← ae_restrict_iff' measurableSet_Ioc, ← uIoc_of_le hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
rwa : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioc a b), ‖deriv f x‖ ≤ B x
⊢ ∀ᵐ (t : ℝ), t ∈ Ioc a b → ‖deriv f t‖ ≤ B t
have rwa₁ : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (uIoc a b), ‖deriv f x‖ ≤ B x
Tactic: rwa [← ae_restrict_iff' measurableSet_Ioc, ← uIoc_of_le hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
⊢ ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (deriv f x) (Ioi x) x
have hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (deriv f x) (Ioi x) x
Tactic: rw [min_eq_left hab, max_eq_right hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
⊢ IntervalIntegrable (deriv f) volume a b
have hint : (ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))).EventuallyLE (β := ℝ) (fun (x : ℝ) ↦ ‖deriv f x‖)
  fun (x : ℝ) ↦ ‖B x‖
Tactic: apply hBi.mono_fun (aestronglyMeasurable_deriv _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
⊢ ‖f b - f a‖ ≤
    C * Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume {x : ℝ | x ∈ Ioo a b ∧ deriv f x ≠ 0}
have hsm : MeasurableSet s
Tactic: have hsm : MeasurableSet s := by measurability
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, s.indicator (fun (x : ℝ) ↦ C) t
have hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ s.indicator (fun (x : ℝ) ↦ C) t
Tactic: apply norm_sub_le_integral_of_norm_deriv_le_of_le hab hfc hfd
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ s.indicator (fun (x : ℝ) ↦ C) t
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, s.indicator (fun (x : ℝ) ↦ C) t
have hBi : IntervalIntegrable (ε := ℝ) (s.indicator fun (x : ℝ) ↦ C) volume a b
Tactic: apply norm_sub_le_integral_of_norm_deriv_le_of_le hab hfc hfd
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
⊢ ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ s.indicator (fun (x : ℝ) ↦ C) t
have hfB : ∀ (t : ℝ) (ht : t ∈ Ioo a b → ‖deriv f t‖ ≤ C) (ht_mem : t ∈ Ioo a b), ‖deriv f t‖ ≤ s.indicator (fun (x : ℝ) ↦ C) t
Tactic: refine hnorm.mono fun t ht ht_mem ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
t : ℝ
ht : t ∈ Ioo a b → ‖deriv f t‖ ≤ C
ht_mem : t ∈ Ioo a b
⊢ ‖deriv f t‖ ≤ s.indicator (fun (x : ℝ) ↦ C) t
have hfB : t ∈ s → ‖deriv f t‖ ≤ C
Tactic: apply le_indicator_apply
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
t : ℝ
ht : t ∈ Ioo a b → ‖deriv f t‖ ≤ C
ht_mem : t ∈ Ioo a b
hfB : t ∈ s → ‖deriv f t‖ ≤ C
⊢ ‖deriv f t‖ ≤ s.indicator (fun (x : ℝ) ↦ C) t
have hfB₁ : t ∉ s → ‖deriv f t‖ ≤ 0
Tactic: apply le_indicator_apply
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
t : ℝ
ht : t ∈ Ioo a b → ‖deriv f t‖ ≤ C
ht_mem : t ∈ Ioo a b
⊢ t ∉ s → ‖deriv f t‖ ≤ 0
have hfB : t ∉ toMeasurable volume {x : ℝ | deriv f x ≠ 0} → deriv f t = 0
Tactic: simp only [s, norm_le_zero_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
⊢ IntervalIntegrable (ε := ℝ) (s.indicator fun (x : ℝ) ↦ C) volume a b
have hBi : IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (s.indicator fun (x : ℝ) ↦ C) (Ioo a b) volume
Tactic: rw [intervalIntegrable_iff_integrableOn_Ioo_of_le hab]