awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C
hmem_s :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → Membership.mem (α := E) s ((lineMap a b : (a : ℝ) → E) t : E)
⊢ 0 ≤ C

Tactic:
have hC₀ : 0 ≤ C := (norm_nonneg _).trans <| hC _ <| hmem_s (1 / 2) (by norm_num)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C
hmem_s :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → Membership.mem (α := E) s ((lineMap a b : (a : ℝ) → E) t : E)
hC₀ : 0 ≤ C
⊢ ContinuousOn f (segment ℝ a b)

Tactic:
have hfc : ContinuousOn f (segment ℝ a b) :=
    hf.continuousOn.mono <| segment_subset_closure_openSegment.trans <| closure_mono hab
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C
hmem_s :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → Membership.mem (α := E) s ((lineMap a b : (a : ℝ) → E) t : E)
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
⊢ ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)

Tactic:
have hfd : ∀ t ∈ Ioo (0 : ℝ) 1, LineDifferentiableAt ℝ f (lineMap a b t) (b - a) := fun t ht ↦
    (hf.differentiableAt hs <| hmem_s t ht).lineDifferentiableAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C
hmem_s :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → Membership.mem (α := E) s ((lineMap a b : (a : ℝ) → E) t : E)
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t
rw : norm.{u_2} (E := F) ((fderiv ℝ f ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a) : F) ≤ C * ‖b - a‖
rw₁ : DifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t)
⊢ ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C * ‖b - a‖

Tactic:
rw [DifferentiableAt.lineDeriv_eq_fderiv]

Premises used: DifferentiableAt.lineDeriv_eq_fderiv
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C
hmem_s :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → Membership.mem (α := E) s ((lineMap a b : (a : ℝ) → E) t : E)
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t
⊢ norm.{u_2} (E := F) ((fderiv ℝ f ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a) : F) ≤ C * ‖b - a‖

Tactic:
ContinuousLinearMap.le_of_opNorm_le _ (hC _ <| hmem_s t ht) _

Premises used: ContinuousLinearMap.le_of_opNorm_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C
hmem_s :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → Membership.mem (α := E) s ((lineMap a b : (a : ℝ) → E) t : E)
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t
⊢ norm.{u_2} (E := F) ((fderiv ℝ f ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a) : F) ≤ C * ‖b - a‖

Tactic:
exact ContinuousLinearMap.le_of_opNorm_le _ (hC _ <| hmem_s t ht) _

Premises used: ContinuousLinearMap.le_of_opNorm_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C
hmem_s :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → Membership.mem (α := E) s ((lineMap a b : (a : ℝ) → E) t : E)
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t
⊢ DifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t)

Tactic:
hf.differentiableAt hs <| hmem_s t ht

Premises used: DiffContOnCl.differentiableAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C
hmem_s :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → Membership.mem (α := E) s ((lineMap a b : (a : ℝ) → E) t : E)
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t
⊢ DifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t)

Tactic:
exact hf.differentiableAt hs <| hmem_s t ht

Premises used: DiffContOnCl.differentiableAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C
hmem_s :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → Membership.mem (α := E) s ((lineMap a b : (a : ℝ) → E) t : E)
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
⊢ ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C * ‖b - a‖

Tactic:
have hfC : ∀ t ∈ Ioo (0 : ℝ) 1, ‖lineDeriv ℝ f (lineMap a b t) (b - a)‖ ≤ C * ‖b - a‖ := by
    intro t ht
    rw [DifferentiableAt.lineDeriv_eq_fderiv]
    · exact ContinuousLinearMap.le_of_opNorm_le _ (hC _ <| hmem_s t ht) _
    · exact hf.differentiableAt hs <| hmem_s t ht
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C
hmem_s :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → Membership.mem (α := E) s ((lineMap a b : (a : ℝ) → E) t : E)
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hfC :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C * ‖b - a‖
⊢ ‖f b - f a‖ ≤
    C * ‖b - a‖ *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ |
          Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ Ne (α := E →L[ℝ] F) (fderiv ℝ f ((lineMap a b : (a : ℝ) → E) t)) 0}

Tactic:
norm_sub_le_mul_volume_of_norm_lineDeriv_le hfc hfd (.of_forall hfC) |>.trans ?_

Premises used: norm_sub_le_mul_volume_of_norm_lineDeriv_le, Filter.Eventually.of_forall, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C
hmem_s :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → Membership.mem (α := E) s ((lineMap a b : (a : ℝ) → E) t : E)
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hfC :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C * ‖b - a‖
refine :
  C * ‖b - a‖ *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a) ≠ 0} ≤
    C * ‖b - a‖ *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ |
          Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ Ne (α := E →L[ℝ] F) (fderiv ℝ f ((lineMap a b : (a : ℝ) → E) t)) 0}
⊢ ‖f b - f a‖ ≤
    C * ‖b - a‖ *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ |
          Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ Ne (α := E →L[ℝ] F) (fderiv ℝ f ((lineMap a b : (a : ℝ) → E) t)) 0}

Tactic:
refine norm_sub_le_mul_volume_of_norm_lineDeriv_le hfc hfd (.of_forall hfC) |>.trans ?_

Premises used: norm_sub_le_mul_volume_of_norm_lineDeriv_le, Filter.Eventually.of_forall, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C
hmem_s :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → Membership.mem (α := E) s ((lineMap a b : (a : ℝ) → E) t : E)
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hfC :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C * ‖b - a‖
hbc :
  autoParam
    (Ne (α := ENNReal)
      ((volume : (a : Set ℝ) → ENNReal)
          {t : ℝ |
            Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧
              Ne (α := E →L[ℝ] F) (fderiv ℝ f ((lineMap a b : (a : ℝ) → E) t)) 0} :
        ENNReal)
      (⊤ : ENNReal))
    measureReal_mono._auto_1
hbc₁ :
  ∀ (a_1 : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) a_1 →
      Eq (α := E →L[ℝ] F) (fderiv ℝ f ((lineMap a b : (a : ℝ) → E) a_1)) 0 →
        lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) a_1) (b - a) = 0
⊢ C * ‖b - a‖ *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a) ≠ 0} ≤
    C * ‖b - a‖ *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ |
          Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ Ne (α := E →L[ℝ] F) (fderiv ℝ f ((lineMap a b : (a : ℝ) → E) t)) 0}

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C
hmem_s :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → Membership.mem (α := E) s ((lineMap a b : (a : ℝ) → E) t : E)
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hfC :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C * ‖b - a‖
⊢ autoParam
    (Ne (α := ENNReal)
      ((volume : (a : Set ℝ) → ENNReal)
          {t : ℝ |
            Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧
              Ne (α := E →L[ℝ] F) (fderiv ℝ f ((lineMap a b : (a : ℝ) → E) t)) 0} :
        ENNReal)
      (⊤ : ENNReal))
    measureReal_mono._auto_1

Tactic:
ne_top_of_le_ne_top ?_ (measure_mono inter_subset_left)

Premises used: Set.inter_subset_left, ne_top_of_le_ne_top, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C
hmem_s :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → Membership.mem (α := E) s ((lineMap a b : (a : ℝ) → E) t : E)
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hfC :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C * ‖b - a‖
hbc : Ne (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo 0 1) : ENNReal) (⊤ : ENNReal)
⊢ autoParam
    (Ne (α := ENNReal)
      ((volume : (a : Set ℝ) → ENNReal)
          {t : ℝ |
            Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧
              Ne (α := E →L[ℝ] F) (fderiv ℝ f ((lineMap a b : (a : ℝ) → E) t)) 0} :
        ENNReal)
      (⊤ : ENNReal))
    measureReal_mono._auto_1

Tactic:
refine ne_top_of_le_ne_top ?_ (measure_mono inter_subset_left)

Premises used: Set.inter_subset_left, ne_top_of_le_ne_top, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C
hmem_s :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → Membership.mem (α := E) s ((lineMap a b : (a : ℝ) → E) t : E)
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hfC :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C * ‖b - a‖
⊢ Ne (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo 0 1) : ENNReal) (⊤ : ENNReal)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C
hmem_s :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → Membership.mem (α := E) s ((lineMap a b : (a : ℝ) → E) t : E)
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hfC :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C * ‖b - a‖
a_1 : ℝ
h : Membership.mem (γ := Set ℝ) (Ioo 0 1) a_1
⊢ Eq (α := E →L[ℝ] F) (fderiv ℝ f ((lineMap a b : (a : ℝ) → E) a_1)) 0 →
    lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) a_1) (b - a) = 0

Tactic:
simp +contextual [(hf.differentiableAt hs <| hmem_s _ ‹_›).lineDeriv_eq_fderiv]

Premises used: DiffContOnCl.differentiableAt, DifferentiableAt.lineDeriv_eq_fderiv
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
rcases :
  ∀ (C : ℝ) (hC₀ : C > 0)
    (hC : Asymptotics.IsBigOWith (E := E →L[ℝ] F) (F := ℝ) C (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r),
    Asymptotics.IsBigO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 a) (fun (x : E) ↦ f x - f a) fun (x : E) ↦ ‖x - a‖ ^ (r + 1)
⊢ Asymptotics.IsBigO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 a) (fun (x : E) ↦ f x - f a) fun (x : E) ↦ ‖x - a‖ ^ (r + 1)

Tactic:
rcases hderiv.exists_pos with ⟨C, hC₀, hC⟩

Premises used: Asymptotics.IsBigO.exists_pos
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : Asymptotics.IsBigOWith (E := E →L[ℝ] F) (F := ℝ) C (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
⊢ ∀ᶠ (x : E) in 𝓝 a, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖‖x - a‖ ^ r‖

Tactic:
rw [Asymptotics.IsBigOWith_def] at hC

Premises used: Asymptotics.IsBigOWith_def
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖‖x - a‖ ^ r‖
rcases :
  ∀ (ε : ℝ) (hε₀ : ε > 0)
    (hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ norm (E := E →L[ℝ] F) (fderiv ℝ f y) ≤ C * ‖‖y - a‖ ^ r‖),
    Asymptotics.IsBigO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 a) (fun (x : E) ↦ f x - f a) fun (x : E) ↦ ‖x - a‖ ^ (r + 1)
⊢ Asymptotics.IsBigO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 a) (fun (x : E) ↦ f x - f a) fun (x : E) ↦ ‖x - a‖ ^ (r + 1)

Tactic:
rcases eventually_nhds_iff_ball.mp (hdf.and hC) with ⟨ε, hε₀, hε⟩

Premises used: Filter.Eventually.and, Iff.mp, Metric.eventually_nhds_iff_ball
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ norm (E := E →L[ℝ] F) (fderiv ℝ f y) ≤ C * ‖‖y - a‖ ^ r‖
⊢ Asymptotics.IsBigO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 a) (fun (x : E) ↦ f x - f a) fun (x : E) ↦ ‖x - a‖ ^ (r + 1)

Tactic:
.of_bound C ?_

Premises used: Asymptotics.IsBigO.of_bound
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ norm (E := E →L[ℝ] F) (fderiv ℝ f y) ≤ C * ‖‖y - a‖ ^ r‖
refine : ∀ᶠ (x : E) in 𝓝 a, ‖f x - f a‖ ≤ C * ‖‖x - a‖ ^ (r + 1)‖
⊢ Asymptotics.IsBigO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 a) (fun (x : E) ↦ f x - f a) fun (x : E) ↦ ‖x - a‖ ^ (r + 1)

Tactic:
refine .of_bound C ?_
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ norm (E := E →L[ℝ] F) (fderiv ℝ f y) ≤ C * ‖‖y - a‖ ^ r‖
rw : ∃ ε > 0, ∀ y ∈ ball a ε, ‖f y - f a‖ ≤ C * ‖‖y - a‖ ^ (r + 1)‖
⊢ ∀ᶠ (x : E) in 𝓝 a, ‖f x - f a‖ ≤ C * ‖‖x - a‖ ^ (r + 1)‖

Tactic:
rw [eventually_nhds_iff_ball]

Premises used: Metric.eventually_nhds_iff_ball
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ norm (E := E →L[ℝ] F) (fderiv ℝ f y) ≤ C * ‖‖y - a‖ ^ r‖
⊢ ∃ ε > 0, ∀ y ∈ ball a ε, ‖f y - f a‖ ≤ C * ‖‖y - a‖ ^ (r + 1)‖

Tactic:
⟨ε, hε₀, fun y hy ↦ ?_⟩

Premises used: And.intro, Exists.intro