awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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
⊢ ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C * ‖b - a‖
have rw : norm.{u_2} (E := F) ((fderiv ℝ f ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a) : F) ≤ C * ‖b - a‖
Tactic: rw [DifferentiableAt.lineDeriv_eq_fderiv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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‖
⊢ ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C * ‖b - a‖
have rw₁ : DifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t)
Tactic: rw [DifferentiableAt.lineDeriv_eq_fderiv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (hypothesis)
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)
⊢ ‖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}
have hfC : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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}
have 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}
Tactic: refine norm_sub_le_mul_volume_of_norm_lineDeriv_le hfc hfd (.of_forall hfC) |>.trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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‖
⊢ 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}
have 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
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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
⊢ 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}
have 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
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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
have hbc : Ne (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo 0 1) : ENNReal) (⊤ : ENNReal)
Tactic: refine ne_top_of_le_ne_top ?_ (measure_mono inter_subset_left)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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
⊢ 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)
have 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)
Tactic: rcases hderiv.exists_pos with ⟨C, hC₀, hC⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (hypothesis)
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
⊢ 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)
have hC₁ : ∀ᶠ (x : E) in 𝓝 a, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖‖x - a‖ ^ r‖
Tactic: rw [Asymptotics.IsBigOWith_def] at hC
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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‖
⊢ 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)
have 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)
Tactic: rcases eventually_nhds_iff_ball.mp (hdf.and hC) with ⟨ε, hε₀, hε⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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)
have refine : ∀ᶠ (x : E) in 𝓝 a, ‖f x - f a‖ ≤ C * ‖‖x - a‖ ^ (r + 1)‖
Tactic: refine .of_bound C ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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‖
⊢ ∀ᶠ (x : E) in 𝓝 a, ‖f x - f a‖ ≤ C * ‖‖x - a‖ ^ (r + 1)‖
have rw : ∃ ε > 0, ∀ y ∈ ball a ε, ‖f y - f a‖ ≤ C * ‖‖y - a‖ ^ (r + 1)‖
Tactic: rw [eventually_nhds_iff_ball]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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)‖
have refine : ∀ (y : E) (hy : y ∈ ball a ε), ‖f y - f a‖ ≤ C * ‖‖y - a‖ ^ (r + 1)‖
Tactic: refine ⟨ε, hε₀, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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‖
y : E
hy : y ∈ ball a ε
⊢ ‖f y - f a‖ ≤ C * ‖‖y - a‖ ^ (r + 1)‖
have rw : ‖f y - f a‖ ≤ C * ‖y - a‖ ^ r * ‖y - a‖
Tactic: rw [Real.norm_of_nonneg (by positivity), Real.rpow_add_one' (by positivity) (by positivity),
    ← mul_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (hypothesis)
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‖
y : E
hy : y ∈ ball a ε
⊢ ‖f y - f a‖ ≤ C * ‖y - a‖ ^ r * ‖y - a‖
have hsub : closedBall a ‖y - a‖ ⊆ ball a ε
Tactic: have hsub : closedBall a ‖y - a‖ ⊆ ball a ε :=
    closedBall_subset_ball (mem_ball_iff_norm.mp hy)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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‖
y : E
hy : y ∈ ball a ε
hsub : closedBall a ‖y - a‖ ⊆ ball a ε
⊢ ‖f y - f a‖ ≤ C * ‖y - a‖ ^ r * ‖y - a‖
have hf : ∀ x ∈ closedBall a ‖y - a‖, DifferentiableAt ℝ f x
Tactic: apply (convex_closedBall a ‖y - a‖).norm_image_sub_le_of_norm_fderiv_le (𝕜 := ℝ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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‖
y : E
hy : y ∈ ball a ε
hsub : closedBall a ‖y - a‖ ⊆ ball a ε
hf : ∀ x ∈ closedBall a ‖y - a‖, DifferentiableAt ℝ f x
⊢ ‖f y - f a‖ ≤ C * ‖y - a‖ ^ r * ‖y - a‖
have bound : ∀ x ∈ closedBall a ‖y - a‖, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖y - a‖ ^ r
Tactic: apply (convex_closedBall a ‖y - a‖).norm_image_sub_le_of_norm_fderiv_le (𝕜 := ℝ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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‖
y : E
hy : y ∈ ball a ε
hsub : closedBall a ‖y - a‖ ⊆ ball a ε
hf : ∀ x ∈ closedBall a ‖y - a‖, DifferentiableAt ℝ f x
bound : ∀ x ∈ closedBall a ‖y - a‖, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖y - a‖ ^ r
⊢ ‖f y - f a‖ ≤ C * ‖y - a‖ ^ r * ‖y - a‖
have xs : a ∈ closedBall a ‖y - a‖
Tactic: apply (convex_closedBall a ‖y - a‖).norm_image_sub_le_of_norm_fderiv_le (𝕜 := ℝ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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‖
y : E
hy : y ∈ ball a ε
hsub : closedBall a ‖y - a‖ ⊆ ball a ε
hf : ∀ x ∈ closedBall a ‖y - a‖, DifferentiableAt ℝ f x
bound : ∀ x ∈ closedBall a ‖y - a‖, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖y - a‖ ^ r
xs : a ∈ closedBall a ‖y - a‖
⊢ ‖f y - f a‖ ≤ C * ‖y - a‖ ^ r * ‖y - a‖
have ys : y ∈ closedBall a ‖y - a‖
Tactic: apply (convex_closedBall a ‖y - a‖).norm_image_sub_le_of_norm_fderiv_le (𝕜 := ℝ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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‖
y : E
hy : y ∈ ball a ε
hsub : closedBall a ‖y - a‖ ⊆ ball a ε
z : E
hz : z ∈ closedBall a ‖y - a‖
⊢ norm (E := E →L[ℝ] F) (fderiv ℝ f z) ≤ C * ‖y - a‖ ^ r
have bound : C * ‖‖z - a‖ ^ r‖ ≤ C * ‖y - a‖ ^ r
Tactic: grw [(hε z <| hsub hz).2, Real.norm_of_nonneg (by positivity), mem_closedBall_iff_norm.mp hz]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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‖
y : E
hy : y ∈ ball a ε
hsub : closedBall a ‖y - a‖ ⊆ ball a ε
z : E
hz : z ∈ closedBall a ‖y - a‖
bound : C * ‖‖z - a‖ ^ r‖ ≤ C * ‖y - a‖ ^ r
⊢ norm (E := E →L[ℝ] F) (fderiv ℝ f z) ≤ C * ‖y - a‖ ^ r
have bound₁ : C * ‖z - a‖ ^ r ≤ C * ‖y - a‖ ^ r
Tactic: grw [(hε z <| hsub hz).2, Real.norm_of_nonneg (by positivity), mem_closedBall_iff_norm.mp hz]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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‖
y : E
hy : y ∈ ball a ε
hsub : closedBall a ‖y - a‖ ⊆ ball a ε
z : E
hz : z ∈ closedBall a ‖y - a‖
bound : C * ‖‖z - a‖ ^ r‖ ≤ C * ‖y - a‖ ^ r
bound₁ : C * ‖z - a‖ ^ r ≤ C * ‖y - a‖ ^ r
⊢ norm (E := E →L[ℝ] F) (fderiv ℝ f z) ≤ C * ‖y - a‖ ^ r
have bound₂ : C * ‖y - a‖ ^ r ≤ C * ‖y - a‖ ^ r
Tactic: grw [(hε z <| hsub hz).2, Real.norm_of_nonneg (by positivity), mem_closedBall_iff_norm.mp hz]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : ℝ
⊢ FTCFilter a (𝓝[{a}] a) ⊥
have rw : FTCFilter a (Pure.pure a) ⊥
Tactic: rw [nhdsWithin, principal_singleton, inf_eq_right.2 (pure_le_nhds a)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : ℝ
⊢ FTCFilter a (𝓝[univ] a) (𝓝 a)
have rw : FTCFilter a (𝓝 a) (𝓝 a)
Tactic: rw [nhdsWithin_univ]