awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
x : ℝ
hx : x ∈ Ico a b
⊢ HasDerivWithinAt f (f' x) (Ici x) x

Tactic:
exact (hf x <| Ico_subset_Icc_self hx).mono_of_mem_nhdsWithin (Icc_mem_nhdsGE_of_mem hx)

Premises used: Set.Ico_subset_Icc_self, Icc_mem_nhdsGE_of_mem, HasDerivWithinAt.mono_of_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hf : DifferentiableOn ℝ f (Icc a b)
bound : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ C
⊢ ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)

Tactic:
norm_image_sub_le_of_norm_deriv_le_segment' ?_ bound

Premises used: norm_image_sub_le_of_norm_deriv_le_segment'
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hf : DifferentiableOn ℝ f (Icc a b)
bound : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ C
refine : ∀ x ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) x) (Icc a b) x
⊢ ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)

Tactic:
refine norm_image_sub_le_of_norm_deriv_le_segment' ?_ bound

Premises used: norm_image_sub_le_of_norm_deriv_le_segment'
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hf : DifferentiableOn ℝ f (Icc a b)
bound : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ C
⊢ ∀ x ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) x) (Icc a b) x

Tactic:
fun x hx => (hf x hx).hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hf : DifferentiableOn ℝ f (Icc a b)
bound : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ C
⊢ ∀ x ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) x) (Icc a b) x

Tactic:
exact fun x hx => (hf x hx).hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → E
C : ℝ
hf : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) x → HasDerivWithinAt f (f' x) (Icc 0 1) x
bound : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ico 0 1) x → ‖f' x‖ ≤ C
⊢ ‖f 1 - f 0‖ ≤ C

Tactic:
simpa only [sub_zero, mul_one] using
    norm_image_sub_le_of_norm_deriv_le_segment' hf bound 1 (right_mem_Icc.2 zero_le_one)

Premises used: Iff.mpr, Set.right_mem_Icc, sub_zero, zero_le_one, mul_one, OfNat.ofNat, norm_image_sub_le_of_norm_deriv_le_segment'
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
C : ℝ
hf : DifferentiableOn ℝ f (Icc 0 1)
bound : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ico 0 1) x → ‖derivWithin f (Icc 0 1) x‖ ≤ C
⊢ ‖f 1 - f 0‖ ≤ C

Tactic:
simpa only [sub_zero, mul_one] using
    norm_image_sub_le_of_norm_deriv_le_segment hf bound 1 (right_mem_Icc.2 zero_le_one)

Premises used: Iff.mpr, Set.right_mem_Icc, sub_zero, norm_image_sub_le_of_norm_deriv_le_segment, zero_le_one, mul_one, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt f 0 (Ici x) x
⊢ ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ 0 * (x - a)

Tactic:
have : ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ 0 * (x - a) := fun x hx =>
    norm_image_sub_le_of_norm_deriv_right_le_segment hcont hderiv (fun _ _ => norm_zero.le) x hx
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt f 0 (Ici x) x
this : ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ 0 * (x - a)
⊢ ∀ x ∈ Icc a b, f x = f a

Tactic:
simpa only [zero_mul, norm_le_zero_iff, sub_eq_zero] using this

Premises used: sub_eq_zero, MulZeroClass.zero_mul, norm_le_zero_iff
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hdiff : DifferentiableOn ℝ f (Icc a b)
hderiv : ∀ x ∈ Ico a b, derivWithin f (Icc a b) x = 0
⊢ ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ 0

Tactic:
simpa only [norm_le_zero_iff] using fun x hx => hderiv x hx

Premises used: norm_le_zero_iff
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hdiff : DifferentiableOn ℝ f (Icc a b)
hderiv : ∀ x ∈ Ico a b, derivWithin f (Icc a b) x = 0
⊢ ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ 0

Tactic:
have H : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ 0 := by
    simpa only [norm_le_zero_iff] using fun x hx => hderiv x hx
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hdiff : DifferentiableOn ℝ f (Icc a b)
hderiv : ∀ x ∈ Ico a b, derivWithin f (Icc a b) x = 0
H : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ 0
⊢ ∀ x ∈ Icc a b, f x = f a

Tactic:
simpa only [zero_mul, norm_le_zero_iff, sub_eq_zero] using fun x hx =>
    norm_image_sub_le_of_norm_deriv_le_segment hdiff H x hx

Premises used: sub_eq_zero, MulZeroClass.zero_mul, norm_image_sub_le_of_norm_deriv_le_segment, norm_le_zero_iff
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' g : ℝ → E
derivf : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
derivg : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x
fcont : ContinuousOn f (Icc a b)
gcont : ContinuousOn g (Icc a b)
hi : f a = g a
simp : ∀ (hi : f a - g a = 0), ∀ y ∈ Icc a b, f y - g y = 0
⊢ ∀ y ∈ Icc a b, f y = g y

Tactic:
simp only [← @sub_eq_zero _ _ (f _)] at hi ⊢

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' g : ℝ → E
derivf : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
derivg : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x
fcont : ContinuousOn f (Icc a b)
gcont : ContinuousOn g (Icc a b)
hi : f a - g a = 0
y : ℝ
hy : y ∈ Ico a b
⊢ HasDerivWithinAt.{0, u_1} (F := E) (fun (y : ℝ) ↦ f y - g y) 0 (Ici y) y

Tactic:
simpa only [sub_self] using (derivf y hy).sub (derivg y hy)

Premises used: HasDerivWithinAt.sub, sub_self
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' g : ℝ → E
derivf : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
derivg : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x
fcont : ContinuousOn f (Icc a b)
gcont : ContinuousOn g (Icc a b)
hi : f a - g a = 0
⊢ ∀ y ∈ Icc a b, f y - g y = 0

Tactic:
exact hi ▸ constant_of_has_deriv_right_zero (fcont.sub gcont) fun y hy => by
    simpa only [sub_self] using (derivf y hy).sub (derivg y hy)
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
g : ℝ → E
fdiff : DifferentiableOn ℝ f (Icc a b)
gdiff : DifferentiableOn ℝ g (Icc a b)
hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)
hi : f a = g a
⊢ ∀ y ∈ Ico a b, HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y

Tactic:
have A : ∀ y ∈ Ico a b, HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y := fun y hy =>
    (fdiff y (mem_Icc_of_Ico hy)).hasDerivWithinAt.mono_of_mem_nhdsWithin
    (Icc_mem_nhdsGE_of_mem hy)
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
g : ℝ → E
fdiff : DifferentiableOn ℝ f (Icc a b)
gdiff : DifferentiableOn ℝ g (Icc a b)
hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)
hi : f a = g a
A : ∀ y ∈ Ico a b, HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y
⊢ ∀ y ∈ Ico a b, HasDerivWithinAt g (derivWithin g (Icc a b) y) (Ici y) y

Tactic:
have B : ∀ y ∈ Ico a b, HasDerivWithinAt g (derivWithin g (Icc a b) y) (Ici y) y := fun y hy =>
    (gdiff y (mem_Icc_of_Ico hy)).hasDerivWithinAt.mono_of_mem_nhdsWithin
    (Icc_mem_nhdsGE_of_mem hy)
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
g : ℝ → E
fdiff : DifferentiableOn ℝ f (Icc a b)
gdiff : DifferentiableOn ℝ g (Icc a b)
hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)
hi : f a = g a
A : ∀ y ∈ Ico a b, HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y
B : ∀ y ∈ Ico a b, HasDerivWithinAt g (derivWithin g (Icc a b) y) (Ici y) y
⊢ ∀ y ∈ Icc a b, f y = g y

Tactic:
eq_of_has_deriv_right_eq A (fun y hy => (hderiv hy).symm ▸ B y hy) fdiff.continuousOn
    gdiff.continuousOn hi

Premises used: DifferentiableOn.continuousOn, Eq.rec, eq_of_has_deriv_right_eq, Eq.symm
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
g : ℝ → E
fdiff : DifferentiableOn ℝ f (Icc a b)
gdiff : DifferentiableOn ℝ g (Icc a b)
hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)
hi : f a = g a
A : ∀ y ∈ Ico a b, HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y
B : ∀ y ∈ Ico a b, HasDerivWithinAt g (derivWithin g (Icc a b) y) (Ici y) y
⊢ ∀ y ∈ Icc a b, f y = g y

Tactic:
exact eq_of_has_deriv_right_eq A (fun y hy => (hderiv hy).symm ▸ B y hy) fdiff.continuousOn
    gdiff.continuousOn hi

Premises used: DifferentiableOn.continuousOn, eq_of_has_deriv_right_eq
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
𝕜 : Type u_3
G : Type u_4
inst_4 : NontriviallyNormedField 𝕜
inst_5 : IsRCLikeNormedField 𝕜
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
f g : E → G
C : ℝ
s : Set E
x y : E
f' g' : E → E →L[𝕜] G
φ : E →L[𝕜] G
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ PathConnectedSpace 𝕜

Tactic:
infer_instance
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := NormedSpace.restrictScalars ℝ 𝕜 G
g : (a : ℝ) → E := (⇑(AffineMap.lineMap x y) : (a : ℝ) → E)
⊢ MapsTo g (Icc 0 1) s

Tactic:
have segm : MapsTo g (Icc 0 1 : Set ℝ) s := hs.mapsTo_lineMap xs ys
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := NormedSpace.restrictScalars ℝ 𝕜 G
g : (a : ℝ) → E := (⇑(AffineMap.lineMap x y) : (a : ℝ) → E)
segm : MapsTo g (Icc 0 1) s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
⊢ HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → G) (y - x)) (Icc 0 1) t

Tactic:
simpa using ((hf (g t) (segm ht)).restrictScalars ℝ).comp_hasDerivWithinAt _
      AffineMap.hasDerivWithinAt_lineMap segm

Premises used: Real, AffineMap.hasDerivWithinAt_lineMap, HasFDerivWithinAt.restrictScalars, HasFDerivWithinAt.comp_hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := NormedSpace.restrictScalars ℝ 𝕜 G
g : (a : ℝ) → E := (⇑(AffineMap.lineMap x y) : (a : ℝ) → E)
segm : MapsTo g (Icc 0 1) s
⊢ ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → G) (y - x)) (Icc 0 1) t

Tactic:
have hD : ∀ t ∈ Icc (0 : ℝ) 1,
      HasDerivWithinAt (f ∘ g) (f' (g t) (y - x)) (Icc 0 1) t := fun t ht => by
    simpa using ((hf (g t) (segm ht)).restrictScalars ℝ).comp_hasDerivWithinAt _
      AffineMap.hasDerivWithinAt_lineMap segm
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := NormedSpace.restrictScalars ℝ 𝕜 G
g : (a : ℝ) → E := (⇑(AffineMap.lineMap x y) : (a : ℝ) → E)
segm : MapsTo g (Icc 0 1) s
hD :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → G) (y - x)) (Icc 0 1) t
⊢ ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ico 0 1) t → norm.{u_4} (E := G) ((f' (g t) : (a : E) → G) (y - x) : G) ≤ C * ‖y - x‖

Tactic:
have bound : ∀ t ∈ Ico (0 : ℝ) 1, ‖f' (g t) (y - x)‖ ≤ C * ‖y - x‖ := fun t ht =>
    le_of_opNorm_le _ (bound _ <| segm <| Ico_subset_Icc_self ht) _
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound_1 : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := NormedSpace.restrictScalars ℝ 𝕜 G
g : (a : ℝ) → E := (⇑(AffineMap.lineMap x y) : (a : ℝ) → E)
segm : MapsTo g (Icc 0 1) s
hD :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → G) (y - x)) (Icc 0 1) t
bound :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ico 0 1) t → norm.{u_4} (E := G) ((f' (g t) : (a : E) → G) (y - x) : G) ≤ C * ‖y - x‖
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖

Tactic:
simpa [g] using norm_image_sub_le_of_norm_deriv_le_segment_01' hD bound

Premises used: norm_image_sub_le_of_norm_deriv_le_segment_01'
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
C : ℝ≥0
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C
hs : Convex ℝ s
rw : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ (↑C : ℝ) * ‖x - y‖
⊢ LipschitzOnWith C f s

Tactic:
rw [lipschitzOnWith_iff_norm_sub_le]

Premises used: lipschitzOnWith_iff_norm_sub_le
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
C : ℝ≥0
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C
hs : Convex ℝ s
x : E
x_in : x ∈ s
y : E
y_in : y ∈ s
⊢ ‖f x - f y‖ ≤ (↑C : ℝ) * ‖x - y‖

Tactic:
hs.norm_image_sub_le_of_norm_hasFDerivWithin_le hf bound y_in x_in

Premises used: Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
C : ℝ≥0
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C
hs : Convex ℝ s
x : E
x_in : x ∈ s
y : E
y_in : y ∈ s
⊢ ‖f x - f y‖ ≤ (↑C : ℝ) * ‖x - y‖

Tactic:
exact hs.norm_image_sub_le_of_norm_hasFDerivWithin_le hf bound y_in x_in

Premises used: Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x : E
f' : E → E →L[𝕜] G
hs : Convex ℝ s
f : E → G
hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
K : ℝ≥0
hK : ‖f' x‖₊ < K
⊢ ∃ ε > 0, ball x ε ∩ s ⊆ {y : E | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K}

Tactic:
mem_nhdsWithin_iff.1 (hder.and <| hcont.nnnorm.eventually (gt_mem_nhds hK))

Premises used: gt_mem_nhds, Metric.mem_nhdsWithin_iff, ContinuousWithinAt.nnnorm, Filter.Eventually.and, Filter.Tendsto.eventually, Iff.mp
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x : E
f' : E → E →L[𝕜] G
hs : Convex ℝ s
f : E → G
hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
K : ℝ≥0
hK : ‖f' x‖₊ < K
obtain :
  ∀ (ε : ℝ) (ε0 : ε > 0) (hε : ball x ε ∩ s ⊆ {y : E | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K}),
    ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
⊢ ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
obtain ⟨ε, ε0, hε⟩ : ∃ ε > 0,
      ball x ε ∩ s ⊆ { y | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K } :=
    mem_nhdsWithin_iff.1 (hder.and <| hcont.nnnorm.eventually (gt_mem_nhds hK))

Premises used: gt_mem_nhds, Metric.mem_nhdsWithin_iff, ContinuousWithinAt.nnnorm, Filter.Eventually.and, Filter.Tendsto.eventually, Iff.mp
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x : E
f' : E → E →L[𝕜] G
hs : Convex ℝ s
f : E → G
hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
K : ℝ≥0
hK : ‖f' x‖₊ < K
ε : ℝ
ε0 : ε > 0
hε : ball x ε ∩ s ⊆ {y : E | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K}
⊢ s ∩ ball x ε ⊆ {y : E | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K}

Tactic:
rw [inter_comm] at hε

Premises used: Set.inter_comm
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x : E
f' : E → E →L[𝕜] G
hs : Convex ℝ s
f : E → G
hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
K : ℝ≥0
hK : ‖f' x‖₊ < K
ε : ℝ
ε0 : ε > 0
hε : s ∩ ball x ε ⊆ {y : E | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K}
⊢ ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
⟨s ∩ ball x ε, inter_mem_nhdsWithin _ (ball_mem_nhds _ ε0), ?_⟩

Premises used: inter_mem_nhdsWithin, Metric.ball, Inter.inter, Metric.ball_mem_nhds, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x : E
f' : E → E →L[𝕜] G
hs : Convex ℝ s
f : E → G
hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
K : ℝ≥0
hK : ‖f' x‖₊ < K
ε : ℝ
ε0 : ε > 0
hε : s ∩ ball x ε ⊆ {y : E | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K}
refine : LipschitzOnWith K f (s ∩ ball x ε)
⊢ ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
refine ⟨s ∩ ball x ε, inter_mem_nhdsWithin _ (ball_mem_nhds _ ε0), ?_⟩
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x : E
f' : E → E →L[𝕜] G
hs : Convex ℝ s
f : E → G
hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
K : ℝ≥0
hK : ‖f' x‖₊ < K
ε : ℝ
ε0 : ε > 0
hε : s ∩ ball x ε ⊆ {y : E | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K}
⊢ LipschitzOnWith K f (s ∩ ball x ε)

Tactic:
(hs.inter (convex_ball _ _)).lipschitzOnWith_of_nnnorm_hasFDerivWithin_le
      (fun y hy => (hε hy).1.mono inter_subset_left) fun y hy => (hε hy).2.le

Premises used: LT.lt.le, Set.inter_subset_left, Convex.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le, Convex.inter, convex_ball, And.right, And.left, HasFDerivWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x : E
f' : E → E →L[𝕜] G
hs : Convex ℝ s
f : E → G
hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
K : ℝ≥0
hK : ‖f' x‖₊ < K
ε : ℝ
ε0 : ε > 0
hε : s ∩ ball x ε ⊆ {y : E | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K}
⊢ LipschitzOnWith K f (s ∩ ball x ε)

Tactic:
exact
    (hs.inter (convex_ball _ _)).lipschitzOnWith_of_nnnorm_hasFDerivWithin_le
      (fun y hy => (hε hy).1.mono inter_subset_left) fun y hy => (hε hy).2.le

Premises used: LT.lt.le, Set.inter_subset_left, Convex.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le, Convex.inter, convex_ball, And.right, And.left, HasFDerivWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x : E
f' : E → E →L[𝕜] G
hs : Convex ℝ s
f : E → G
hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
(exists_gt _).imp <|
    hs.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt hder hcont

Premises used: NoMaxOrder.exists_gt, Exists.imp, Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt