awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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)
inr : derivWithin f (Icc a b) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ι a b))] deriv f
⊢ IntervalIntegrable (deriv f) volume a b

Tactic:
apply (this.intervalIntegrable_of_Icc (μ := volume) hab).congr_ae

Premises used: ContinuousOn.intervalIntegrable_of_Icc, IntervalIntegrable.congr_ae
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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)
inr : derivWithin f (Icc a b) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] deriv f
⊢ derivWithin f (Icc a b) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ι a b))] deriv f

Tactic:
simp only [hab, uIoc_of_le]

Premises used: Set.uIoc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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)
inr : derivWithin f (Icc a b) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo a b))] deriv f
⊢ derivWithin f (Icc a b) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] deriv f

Tactic:
rw [← restrict_Ioo_eq_restrict_Ioc]

Premises used: MeasureTheory.restrict_Ioo_eq_restrict_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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)
h₁ : ∀ (x : ℝ) (hx : x ∈ Ioo a b), derivWithin f (Icc a b) x = deriv f x
⊢ derivWithin f (Icc a b) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo a b))] deriv f

Tactic:
filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx

Premises used: measurableSet_Ioo, MeasureTheory.self_mem_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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)
x : ℝ
hx : x ∈ Ioo a b
⊢ derivWithin f (Icc a b) x = deriv f x

Tactic:
derivWithin_of_mem_nhds (Icc_mem_nhds hx.1 hx.2)

Premises used: And.right, And.left, derivWithin_of_mem_nhds, Icc_mem_nhds
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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)
x : ℝ
hx : x ∈ Ioo a b
⊢ derivWithin f (Icc a b) x = deriv f x

Tactic:
exact derivWithin_of_mem_nhds (Icc_mem_nhds hx.1 hx.2)

Premises used: And.right, And.left, derivWithin_of_mem_nhds, Icc_mem_nhds
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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
rw : Eq.{u_3 + 1} (α := E) (∫ (x : ℝ) in a..b, derivWithin f (Icc a b) x) (∫ (x : ℝ) in a..b, deriv f x)
⊢ ∫ (x : ℝ) in a..b, derivWithin f (Icc a b) x = f b - f a

Tactic:
rw [← integral_deriv_of_contDiffOn_Icc h hab]

Premises used: intervalIntegral.integral_deriv_of_contDiffOn_Icc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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
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)
⊢ 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_of_le hab, integral_of_le hab]

Premises used: intervalIntegral.integral_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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₁ : derivWithin f (Icc a b) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] deriv f
⊢ 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:
apply MeasureTheory.integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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₁ : derivWithin f (Icc a b) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo a b))] deriv f
⊢ derivWithin f (Icc a b) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] deriv f

Tactic:
rw [← restrict_Ioo_eq_restrict_Ioc]

Premises used: MeasureTheory.restrict_Ioo_eq_restrict_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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₁ : ∀ (x : ℝ) (hx : x ∈ Ioo a b), derivWithin f (Icc a b) x = deriv f x
⊢ derivWithin f (Icc a b) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo a b))] deriv f

Tactic:
filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx

Premises used: measurableSet_Ioo, MeasureTheory.self_mem_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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 : ℝ
hx : x ∈ Ioo a b
⊢ derivWithin f (Icc a b) x = deriv f x

Tactic:
derivWithin_of_mem_nhds (Icc_mem_nhds hx.1 hx.2)

Premises used: And.right, And.left, derivWithin_of_mem_nhds, Icc_mem_nhds
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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 : ℝ
hx : x ∈ Ioo a b
⊢ derivWithin f (Icc a b) x = deriv f x

Tactic:
exact derivWithin_of_mem_nhds (Icc_mem_nhds hx.1 hx.2)

Premises used: And.right, And.left, derivWithin_of_mem_nhds, Icc_mem_nhds
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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
inr : ∀ (hab : b < a), ∫ (x : ℝ) in a..b, deriv f x = f b - f a
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a

Tactic:
rcases le_or_gt a b with hab | hab

Premises used: le_or_gt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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
⊢ ContDiffOn ℝ 1 f (Icc a b)

Tactic:
simp only [uIcc_of_le hab] at h

Premises used: Set.uIcc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
hab : a ≤ b
h : ContDiffOn ℝ 1 f (Icc a b)
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a

Tactic:
integral_deriv_of_contDiffOn_Icc h hab

Premises used: intervalIntegral.integral_deriv_of_contDiffOn_Icc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
hab : a ≤ b
h : ContDiffOn ℝ 1 f (Icc a b)
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a

Tactic:
exact integral_deriv_of_contDiffOn_Icc h hab

Premises used: intervalIntegral.integral_deriv_of_contDiffOn_Icc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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
⊢ ContDiffOn ℝ 1 f (Icc b a)

Tactic:
simp only [uIcc_of_ge hab.le] at h

Premises used: Set.uIcc_of_ge, LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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)
inr : -(f a - f b) = f b - f a
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a

Tactic:
rw [integral_symm, integral_deriv_of_contDiffOn_Icc h hab.le]

Premises used: LT.lt.le, intervalIntegral.integral_symm, intervalIntegral.integral_deriv_of_contDiffOn_Icc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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)
⊢ -(f a - f b) = f b - f a

Tactic:
abel
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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
inr : ∀ (hab : b < a), ∫ (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

Tactic:
rcases le_or_gt a b with hab | hab

Premises used: le_or_gt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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
inl : ∀ (h : ContDiffOn ℝ 1 f (Icc a b)), ∫ (x : ℝ) in a..b, derivWithin f (Icc a b) x = f b - f a
⊢ ∫ (x : ℝ) in a..b, derivWithin f [[a, b]] x = f b - f a

Tactic:
simp only [uIcc_of_le hab] at h ⊢

Premises used: Set.uIcc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
hab : a ≤ b
h : ContDiffOn ℝ 1 f (Icc a b)
⊢ ∫ (x : ℝ) in a..b, derivWithin f (Icc a b) x = f b - f a

Tactic:
integral_derivWithin_Icc_of_contDiffOn_Icc h hab

Premises used: intervalIntegral.integral_derivWithin_Icc_of_contDiffOn_Icc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
hab : a ≤ b
h : ContDiffOn ℝ 1 f (Icc a b)
⊢ ∫ (x : ℝ) in a..b, derivWithin f (Icc a b) x = f b - f a

Tactic:
exact integral_derivWithin_Icc_of_contDiffOn_Icc h hab

Premises used: intervalIntegral.integral_derivWithin_Icc_of_contDiffOn_Icc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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
inr : ∀ (h : ContDiffOn ℝ 1 f (Icc b a)), ∫ (x : ℝ) in a..b, derivWithin f (Icc b a) x = f b - f a
⊢ ∫ (x : ℝ) in a..b, derivWithin f [[a, b]] x = f b - f a

Tactic:
simp only [uIcc_of_ge hab.le] at h ⊢

Premises used: Set.uIcc_of_ge, LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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)
inr : -(f a - f b) = f b - f a
⊢ ∫ (x : ℝ) in a..b, derivWithin f (Icc b a) x = f b - f a

Tactic:
rw [integral_symm, integral_derivWithin_Icc_of_contDiffOn_Icc h hab.le]

Premises used: LT.lt.le, intervalIntegral.integral_symm, intervalIntegral.integral_derivWithin_Icc_of_contDiffOn_Icc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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‖ₑ
rw₃ rw₄ : ‖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‖ₑ

Tactic:
rw [← edist_eq_enorm_sub, Function.comp_def, g.isometry.edist_eq, edist_eq_enorm_sub]

Premises used: edist_eq_enorm_sub, Isometry.edist_eq, Function.comp_def, LinearIsometry.isometry
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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‖ₑ

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]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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‖ₑ
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‖ₑ
⊢ ‖f b - f a‖ₑ ≤ ∫⁻ (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]

Premises used: ContDiff.comp_contDiffOn, intervalIntegral.integral_of_le, LinearIsometry.contDiff, MeasureTheory.restrict_Ioc_eq_restrict_Icc, intervalIntegral.integral_deriv_of_contDiffOn_Icc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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‖ₑ
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‖ₑ
⊢ 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:
apply (enorm_integral_le_lintegral_enorm _).trans

Premises used: MeasureTheory.enorm_integral_le_lintegral_enorm, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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‖ₑ
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‖ₑ
⊢ ∫⁻ (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 lintegral_mono_ae

Premises used: MeasureTheory.lintegral_mono_ae
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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‖ₑ
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‖ₑ
⊢ ∀ᵐ (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:
rw [← restrict_Ioo_eq_restrict_Icc]

Premises used: MeasureTheory.restrict_Ioo_eq_restrict_Icc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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‖ₑ
h₁ :
  ∀ (x : ℝ) (hx : x ∈ Ioo a b),
    enorm (E := UniformSpace.Completion E) (deriv ((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) x) ≤ ‖deriv f x‖ₑ
⊢ ∀ᵐ (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:
filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx

Premises used: measurableSet_Ioo, MeasureTheory.self_mem_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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)
h₃ : DifferentiableAt ℝ f x
⊢ enorm (E := UniformSpace.Completion E) (deriv ((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) x) ≤ ‖deriv f x‖ₑ

Tactic:
rw [fderiv_comp_deriv]

Premises used: fderiv_comp_deriv
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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
⊢ DifferentiableAt ℝ (F := UniformSpace.Completion E) (⇑g : (a : E) → UniformSpace.Completion E) (f x)

Tactic:
(g.contDiff.differentiable one_ne_zero).differentiableAt

Premises used: Differentiable.differentiableAt, LinearIsometry.contDiff, ContDiff.differentiable, one_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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
⊢ DifferentiableAt ℝ (F := UniformSpace.Completion E) (⇑g : (a : E) → UniformSpace.Completion E) (f x)

Tactic:
exact (g.contDiff.differentiable one_ne_zero).differentiableAt

Premises used: Differentiable.differentiableAt, LinearIsometry.contDiff, ContDiff.differentiable, one_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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
⊢ DifferentiableAt ℝ f x

Tactic:
(h x ⟨hx.1.le, hx.2.le⟩).contDiffAt (Icc_mem_nhds hx.1 hx.2)
      |>.differentiableAt one_ne_zero

Premises used: ContDiffAt.differentiableAt, LT.lt.le, ContDiffWithinAt.contDiffAt, And.right, And.left, And.intro, one_ne_zero, Icc_mem_nhds
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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
⊢ DifferentiableAt ℝ f x

Tactic:
exact (h x ⟨hx.1.le, hx.2.le⟩).contDiffAt (Icc_mem_nhds hx.1 hx.2)
      |>.differentiableAt one_ne_zero

Premises used: ContDiffAt.differentiableAt, LT.lt.le, ContDiffWithinAt.contDiffAt, And.right, And.left, And.intro, one_ne_zero, Icc_mem_nhds
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
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
⊢ fderiv ℝ (⇑g : (a : E) → UniformSpace.Completion E) (f x) = g.toContinuousLinearMap

Tactic:
have : fderiv ℝ g (f x) = g.toContinuousLinearMap := g.toContinuousLinearMap.fderiv