awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
x : ℝ
hx : x ∈ Ioo a b
⊢ HasDerivAt f (deriv f x) x
have inr : DifferentiableAt ℝ f x
Tactic: apply DifferentiableAt.hasDerivAt
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
x : ℝ
hx : x ∈ Ioo a b
⊢ DifferentiableAt ℝ f x
have inr : Icc a b ∈ 𝓝 x
Tactic: apply ((h x ⟨hx.1.le, hx.2.le⟩).differentiableWithinAt one_ne_zero).differentiableAt
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
⊢ IntervalIntegrable (deriv f) volume a b
have this : ContinuousOn (derivWithin f (Icc a b)) (Icc a b)
Tactic: have := (h.derivWithin (m := 0) (uniqueDiffOn_Icc h'ab) (by simp)).continuousOn
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
this : ContinuousOn (derivWithin f (Icc a b)) (Icc a b)
⊢ IntervalIntegrable (deriv f) volume a b
have inr : derivWithin f (Icc a b) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ι a b))] deriv f
Tactic: apply (this.intervalIntegrable_of_Icc (μ := volume) hab).congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
this : ContinuousOn (derivWithin f (Icc a b)) (Icc a b)
⊢ derivWithin f (Icc a b) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ι a b))] deriv f
have inr : derivWithin f (Icc a b) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] deriv f
Tactic: simp only [hab, uIoc_of_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
this : ContinuousOn (derivWithin f (Icc a b)) (Icc a b)
⊢ derivWithin f (Icc a b) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] deriv f
have inr : derivWithin f (Icc a b) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo a b))] deriv f
Tactic: rw [← restrict_Ioo_eq_restrict_Ioc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
this : ContinuousOn (derivWithin f (Icc a b)) (Icc a b)
⊢ derivWithin f (Icc a b) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo a b))] deriv f
have h₁ : ∀ (x : ℝ) (hx : x ∈ Ioo a b), derivWithin f (Icc a b) x = deriv f x
Tactic: filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, derivWithin f (Icc a b) x = f b - f a
have rw : Eq.{u_3 + 1} (α := E) (∫ (x : ℝ) in a..b, derivWithin f (Icc a b) x) (∫ (x : ℝ) in a..b, deriv f x)
Tactic: rw [← integral_deriv_of_contDiffOn_Icc h hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : ℝ) in a..b, derivWithin f (Icc a b) x) (∫ (x : ℝ) in a..b, deriv f x)
have rw : Eq.{u_3 + 1} (α := E)
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ derivWithin f (Icc a b) x)
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ deriv f x)
Tactic: rw [integral_of_le hab, integral_of_le hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ derivWithin f (Icc a b) x)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ deriv f x)
have h₁ : derivWithin f (Icc a b) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] deriv f
Tactic: apply MeasureTheory.integral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ derivWithin f (Icc a b) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] deriv f
have h₁ : derivWithin f (Icc a b) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo a b))] deriv f
Tactic: rw [← restrict_Ioo_eq_restrict_Ioc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ derivWithin f (Icc a b) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo a b))] deriv f
have h₁ : ∀ (x : ℝ) (hx : x ∈ Ioo a b), derivWithin f (Icc a b) x = deriv f x
Tactic: filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f [[a, b]]
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a
have inl : ∀ (hab : a ≤ b), ∫ (x : ℝ) in a..b, deriv f x = f b - f a
Tactic: rcases le_or_gt a b with hab | hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f [[a, b]]
inl : ∀ (hab : a ≤ b), ∫ (x : ℝ) in a..b, deriv f x = f b - f a
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a
have inr : ∀ (hab : b < a), ∫ (x : ℝ) in a..b, deriv f x = f b - f a
Tactic: rcases le_or_gt a b with hab | hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f [[a, b]]
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a
have h₁ : ContDiffOn ℝ 1 f (Icc a b)
Tactic: simp only [uIcc_of_le hab] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f [[a, b]]
hab : b < a
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a
have h₁ : ContDiffOn ℝ 1 f (Icc b a)
Tactic: simp only [uIcc_of_ge hab.le] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
hab : b < a
h : ContDiffOn ℝ 1 f (Icc b a)
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a
have inr : -(f a - f b) = f b - f a
Tactic: rw [integral_symm, integral_deriv_of_contDiffOn_Icc h hab.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f [[a, b]]
⊢ ∫ (x : ℝ) in a..b, derivWithin f [[a, b]] x = f b - f a
have inl : ∀ (hab : a ≤ b), ∫ (x : ℝ) in a..b, derivWithin f [[a, b]] x = f b - f a
Tactic: rcases le_or_gt a b with hab | hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f [[a, b]]
inl : ∀ (hab : a ≤ b), ∫ (x : ℝ) in a..b, derivWithin f [[a, b]] x = f b - f a
⊢ ∫ (x : ℝ) in a..b, derivWithin f [[a, b]] x = f b - f a
have inr : ∀ (hab : b < a), ∫ (x : ℝ) in a..b, derivWithin f [[a, b]] x = f b - f a
Tactic: rcases le_or_gt a b with hab | hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f [[a, b]]
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, derivWithin f [[a, b]] x = f b - f a
have inl : ∀ (h : ContDiffOn ℝ 1 f (Icc a b)), ∫ (x : ℝ) in a..b, derivWithin f (Icc a b) x = f b - f a
Tactic: simp only [uIcc_of_le hab] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f [[a, b]]
hab : b < a
⊢ ∫ (x : ℝ) in a..b, derivWithin f [[a, b]] x = f b - f a
have inr : ∀ (h : ContDiffOn ℝ 1 f (Icc b a)), ∫ (x : ℝ) in a..b, derivWithin f (Icc b a) x = f b - f a
Tactic: simp only [uIcc_of_ge hab.le] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
hab : b < a
h : ContDiffOn ℝ 1 f (Icc b a)
⊢ ∫ (x : ℝ) in a..b, derivWithin f (Icc b a) x = f b - f a
have inr : -(f a - f b) = f b - f a
Tactic: rw [integral_symm, integral_derivWithin_Icc_of_contDiffOn_Icc h hab.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
⊢ ‖HSub.hSub (α := UniformSpace.Completion E) (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) b)
        (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a)‖ₑ =
    ‖f b - f a‖ₑ
have rw : edist (α := UniformSpace.Completion E) (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) b)
    (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a) =
  ‖f b - f a‖ₑ
Tactic: rw [← edist_eq_enorm_sub, Function.comp_def, g.isometry.edist_eq, edist_eq_enorm_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
rw :
  edist (α := UniformSpace.Completion E) (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) b)
      (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a) =
    ‖f b - f a‖ₑ
⊢ ‖HSub.hSub (α := UniformSpace.Completion E) (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) b)
        (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a)‖ₑ =
    ‖f b - f a‖ₑ
have rw₁ : edist.{u_3} (α := UniformSpace.Completion E)
    ((fun (x : ℝ) ↦ ((g : (a : E) → UniformSpace.Completion E) (f x) : UniformSpace.Completion E)) b)
    ((fun (x : ℝ) ↦ ((g : (a : E) → UniformSpace.Completion E) (f x) : UniformSpace.Completion E)) a) =
  ‖f b - f a‖ₑ
Tactic: rw [← edist_eq_enorm_sub, Function.comp_def, g.isometry.edist_eq, edist_eq_enorm_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
rw :
  edist (α := UniformSpace.Completion E) (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) b)
      (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a) =
    ‖f b - f a‖ₑ
rw₁ :
  edist.{u_3} (α := UniformSpace.Completion E)
      ((fun (x : ℝ) ↦ ((g : (a : E) → UniformSpace.Completion E) (f x) : UniformSpace.Completion E)) b)
      ((fun (x : ℝ) ↦ ((g : (a : E) → UniformSpace.Completion E) (f x) : UniformSpace.Completion E)) a) =
    ‖f b - f a‖ₑ
⊢ ‖HSub.hSub (α := UniformSpace.Completion E) (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) b)
        (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a)‖ₑ =
    ‖f b - f a‖ₑ
have rw₂ : edist (f b) (f a) = ‖f b - f a‖ₑ
Tactic: rw [← edist_eq_enorm_sub, Function.comp_def, g.isometry.edist_eq, edist_eq_enorm_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
rw :
  edist (α := UniformSpace.Completion E) (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) b)
      (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a) =
    ‖f b - f a‖ₑ
rw₁ :
  edist.{u_3} (α := UniformSpace.Completion E)
      ((fun (x : ℝ) ↦ ((g : (a : E) → UniformSpace.Completion E) (f x) : UniformSpace.Completion E)) b)
      ((fun (x : ℝ) ↦ ((g : (a : E) → UniformSpace.Completion E) (f x) : UniformSpace.Completion E)) a) =
    ‖f b - f a‖ₑ
rw₂ : edist (f b) (f a) = ‖f b - f a‖ₑ
⊢ ‖HSub.hSub (α := UniformSpace.Completion E) (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) b)
        (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a)‖ₑ =
    ‖f b - f a‖ₑ
have rw₃ : ‖f b - f a‖ₑ = ‖f b - f a‖ₑ
Tactic: rw [← edist_eq_enorm_sub, Function.comp_def, g.isometry.edist_eq, edist_eq_enorm_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
⊢ ‖f b - f a‖ₑ ≤ ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ
have this : ‖HSub.hSub (α := UniformSpace.Completion E) (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) b)
      (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a)‖ₑ =
  ‖f b - f a‖ₑ
Tactic: have : ‖(g ∘ f) b - (g ∘ f) a‖ₑ = ‖f b - f a‖ₑ := by
    rw [← edist_eq_enorm_sub, Function.comp_def, g.isometry.edist_eq, edist_eq_enorm_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this :
  ‖HSub.hSub (α := UniformSpace.Completion E) (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) b)
        (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a)‖ₑ =
    ‖f b - f a‖ₑ
⊢ ‖f b - f a‖ₑ ≤ ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ
have rw : enorm.{u_3} (E := UniformSpace.Completion E)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
      deriv ((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) x) ≤
  ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ
Tactic: rw [← this, ← integral_deriv_of_contDiffOn_Icc (g.contDiff.comp_contDiffOn h) hab,
    integral_of_le hab, restrict_Ioc_eq_restrict_Icc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this :
  ‖HSub.hSub (α := UniformSpace.Completion E) (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) b)
        (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a)‖ₑ =
    ‖f b - f a‖ₑ
⊢ enorm.{u_3} (E := UniformSpace.Completion E)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
        deriv ((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) x) ≤
    ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ
have apply : ∫⁻ (a : ℝ) in Icc a b,
    enorm (E := UniformSpace.Completion E) (deriv ((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a) ∂volume ≤
  ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ
Tactic: apply (enorm_integral_le_lintegral_enorm _).trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this :
  ‖HSub.hSub (α := UniformSpace.Completion E) (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) b)
        (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a)‖ₑ =
    ‖f b - f a‖ₑ
⊢ ∫⁻ (a : ℝ) in Icc a b,
      enorm (E := UniformSpace.Completion E) (deriv ((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a) ∂volume ≤
    ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ
have h₁ : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Icc a b),
  enorm (E := UniformSpace.Completion E) (deriv ((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a) ≤ ‖deriv f a‖ₑ
Tactic: apply lintegral_mono_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this :
  ‖HSub.hSub (α := UniformSpace.Completion E) (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) b)
        (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a)‖ₑ =
    ‖f b - f a‖ₑ
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Icc a b),
    enorm (E := UniformSpace.Completion E) (deriv ((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a) ≤ ‖deriv f a‖ₑ
have h₁ : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioo a b),
  enorm (E := UniformSpace.Completion E) (deriv ((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a) ≤ ‖deriv f a‖ₑ
Tactic: rw [← restrict_Ioo_eq_restrict_Icc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this :
  ‖HSub.hSub (α := UniformSpace.Completion E) (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) b)
        (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a)‖ₑ =
    ‖f b - f a‖ₑ
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioo a b),
    enorm (E := UniformSpace.Completion E) (deriv ((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a) ≤ ‖deriv f a‖ₑ
have h₁ : ∀ (x : ℝ) (hx : x ∈ Ioo a b),
  enorm (E := UniformSpace.Completion E) (deriv ((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) x) ≤ ‖deriv f x‖ₑ
Tactic: filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this :
  ‖HSub.hSub (α := UniformSpace.Completion E) (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) b)
        (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a)‖ₑ =
    ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ enorm (E := UniformSpace.Completion E) (deriv ((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) x) ≤ ‖deriv f x‖ₑ
have h₁ : enorm (E := UniformSpace.Completion E)
    ((fderiv ℝ (⇑g : (a : E) → UniformSpace.Completion E) (f x) : (a : E) → UniformSpace.Completion E) (deriv f x) :
      UniformSpace.Completion E) ≤
  ‖deriv f x‖ₑ
Tactic: rw [fderiv_comp_deriv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this :
  ‖HSub.hSub (α := UniformSpace.Completion E) (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) b)
        (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a)‖ₑ =
    ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
h₁ :
  enorm (E := UniformSpace.Completion E)
      ((fderiv ℝ (⇑g : (a : E) → UniformSpace.Completion E) (f x) : (a : E) → UniformSpace.Completion E) (deriv f x) :
        UniformSpace.Completion E) ≤
    ‖deriv f x‖ₑ
⊢ enorm (E := UniformSpace.Completion E) (deriv ((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) x) ≤ ‖deriv f x‖ₑ
have h₂ : DifferentiableAt ℝ (F := UniformSpace.Completion E) (⇑g : (a : E) → UniformSpace.Completion E) (f x)
Tactic: rw [fderiv_comp_deriv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this :
  ‖HSub.hSub (α := UniformSpace.Completion E) (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) b)
        (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a)‖ₑ =
    ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
h₁ :
  enorm (E := UniformSpace.Completion E)
      ((fderiv ℝ (⇑g : (a : E) → UniformSpace.Completion E) (f x) : (a : E) → UniformSpace.Completion E) (deriv f x) :
        UniformSpace.Completion E) ≤
    ‖deriv f x‖ₑ
h₂ : DifferentiableAt ℝ (F := UniformSpace.Completion E) (⇑g : (a : E) → UniformSpace.Completion E) (f x)
⊢ enorm (E := UniformSpace.Completion E) (deriv ((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) x) ≤ ‖deriv f x‖ₑ
have h₃ : DifferentiableAt ℝ f x
Tactic: rw [fderiv_comp_deriv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this :
  ‖HSub.hSub (α := UniformSpace.Completion E) (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) b)
        (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a)‖ₑ =
    ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ enorm (E := UniformSpace.Completion E)
      ((fderiv ℝ (⇑g : (a : E) → UniformSpace.Completion E) (f x) : (a : E) → UniformSpace.Completion E) (deriv f x) :
        UniformSpace.Completion E) ≤
    ‖deriv f x‖ₑ
have this₁ : fderiv ℝ (⇑g : (a : E) → UniformSpace.Completion E) (f x) = g.toContinuousLinearMap
Tactic: have : fderiv ℝ g (f x) = g.toContinuousLinearMap := g.toContinuousLinearMap.fderiv
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ ‖f b - f a‖ₑ ≤ ∫⁻ (x : ℝ) in Icc a b, ‖derivWithin f (Icc a b) x‖ₑ
have apply : ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ = ∫⁻ (x : ℝ) in Icc a b, ‖derivWithin f (Icc a b) x‖ₑ
Tactic: apply (enorm_sub_le_lintegral_deriv_of_contDiffOn_Icc h hab).trans_eq