awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hf : DifferentiableOn 𝕜 f s
bound : ∀ x ∈ s, norm (E := E →L[𝕜] G) (fderivWithin 𝕜 f s x) ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖

Tactic:
hs.norm_image_sub_le_of_norm_hasFDerivWithin_le (fun x hx => (hf x hx).hasFDerivWithinAt) bound
    xs ys

Premises used: Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le, DifferentiableWithinAt.hasFDerivWithinAt
-- 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
C : ℝ≥0
hf : DifferentiableOn 𝕜 f s
bound : ∀ x ∈ s, nnnorm (E := E →L[𝕜] G) (fderivWithin 𝕜 f s x) ≤ C
hs : Convex ℝ s
⊢ LipschitzOnWith C f s

Tactic:
hs.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le (fun x hx => (hf x hx).hasFDerivWithinAt) bound

Premises used: Convex.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le, DifferentiableWithinAt.hasFDerivWithinAt
-- 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
hf : ∀ x ∈ s, DifferentiableAt 𝕜 f x
bound : ∀ x ∈ s, norm (E := E →L[𝕜] G) (fderiv 𝕜 f x) ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖

Tactic:
hs.norm_image_sub_le_of_norm_hasFDerivWithin_le
    (fun x hx => (hf x hx).hasFDerivAt.hasFDerivWithinAt) bound xs ys

Premises used: HasFDerivAt.hasFDerivWithinAt, Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le, DifferentiableAt.hasFDerivAt
-- 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
C : ℝ≥0
hf : ∀ x ∈ s, DifferentiableAt 𝕜 f x
bound : ∀ x ∈ s, nnnorm (E := E →L[𝕜] G) (fderiv 𝕜 f x) ≤ C
hs : Convex ℝ s
⊢ LipschitzOnWith C f s

Tactic:
hs.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le
    (fun x hx => (hf x hx).hasFDerivAt.hasFDerivWithinAt) bound

Premises used: HasFDerivAt.hasFDerivWithinAt, Convex.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le, DifferentiableAt.hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace 𝕜 G
E : Type u_5
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
f : E → G
C : ℝ≥0
hf : Differentiable 𝕜 f
bound : ∀ (x : E), nnnorm (E := E →L[𝕜] G) (fderiv 𝕜 f x) ≤ C
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
rw : LipschitzOnWith C f univ
⊢ LipschitzWith C f

Tactic:
rw [← lipschitzOnWith_univ]

Premises used: lipschitzOnWith_univ
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace 𝕜 G
E : Type u_5
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
f : E → G
C : ℝ≥0
hf : Differentiable 𝕜 f
bound : ∀ (x : E), nnnorm (E := E →L[𝕜] G) (fderiv 𝕜 f x) ≤ C
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ LipschitzOnWith C f univ

Tactic:
lipschitzOnWith_of_nnnorm_fderiv_le (fun x _ ↦ hf x) (fun x _ ↦ bound x) convex_univ

Premises used: Convex.lipschitzOnWith_of_nnnorm_fderiv_le, convex_univ
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace 𝕜 G
E : Type u_5
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
f : E → G
C : ℝ≥0
hf : Differentiable 𝕜 f
bound : ∀ (x : E), nnnorm (E := E →L[𝕜] G) (fderiv 𝕜 f x) ≤ C
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ LipschitzOnWith C f univ

Tactic:
exact lipschitzOnWith_of_nnnorm_fderiv_le (fun x _ ↦ hf x) (fun x _ ↦ bound x) convex_univ

Premises used: Convex.lipschitzOnWith_of_nnnorm_fderiv_le, convex_univ
-- 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
φ : 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
g : (y : E) → G := fun (y : E) ↦ HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G)
⊢ ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x

Tactic:
have hg : ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x := fun x xs =>
    (hf x xs).sub φ.hasFDerivWithinAt
-- 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
φ : 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
g : (y : E) → G := fun (y : E) ↦ HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G)
hg : ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x
⊢ ‖HSub.hSub (β := G) (f y - f x) ((φ : (a : E) → G) (y - x) : G)‖ =
    ‖f y - f x - HSub.hSub (α := G) (β := G) ((φ : (a : E) → G) y : G) ((φ : (a : E) → G) x : G)‖

Tactic:
simp
-- 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
φ : 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
g : (y : E) → G := fun (y : E) ↦ HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G)
hg : ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x
e_a :
  f y - f x - HSub.hSub (α := G) (β := G) ((φ : (a : E) → G) y : G) ((φ : (a : E) → G) x : G) =
    HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G) - HSub.hSub (β := G) (f x) ((φ : (a : E) → G) x : G)
⊢ ‖f y - f x - HSub.hSub (α := G) (β := G) ((φ : (a : E) → G) y : G) ((φ : (a : E) → G) x : G)‖ =
    ‖HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G) - HSub.hSub (β := G) (f x) ((φ : (a : E) → G) x : G)‖

Tactic:
congr 1
-- 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
φ : 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
g : (y : E) → G := fun (y : E) ↦ HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G)
hg : ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x
⊢ f y - f x - HSub.hSub (α := G) (β := G) ((φ : (a : E) → G) y : G) ((φ : (a : E) → G) x : G) =
    HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G) - HSub.hSub (β := G) (f x) ((φ : (a : E) → G) x : G)

Tactic:
abel
-- 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
φ : 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
g : (y : E) → G := fun (y : E) ↦ HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G)
hg : ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x
⊢ ‖HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G) - HSub.hSub (β := G) (f x) ((φ : (a : E) → G) x : G)‖ =
    ‖g y - g x‖

Tactic:
simp [g]
-- 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
φ : 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
g : (y : E) → G := fun (y : E) ↦ HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G)
hg : ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x
⊢ ‖g y - g x‖ ≤ C * ‖y - x‖

Tactic:
Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le hg bound hs xs ys

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
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
φ : 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
g : (y : E) → G := fun (y : E) ↦ HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G)
hg : ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x
y₁ :
  ‖HSub.hSub (β := G) (f y - f x) ((φ : (a : E) → G) (y - x) : G)‖ =
    ‖f y - f x - HSub.hSub (α := G) (β := G) ((φ : (a : E) → G) y : G) ((φ : (a : E) → G) x : G)‖
y₂ :
  ‖f y - f x - HSub.hSub (α := G) (β := G) ((φ : (a : E) → G) y : G) ((φ : (a : E) → G) x : G)‖ =
    ‖HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G) - HSub.hSub (β := G) (f x) ((φ : (a : E) → G) x : G)‖
y₃ :
  ‖HSub.hSub (β := G) (f y) ((φ : (a : E) → G) y : G) - HSub.hSub (β := G) (f x) ((φ : (a : E) → G) x : G)‖ =
    ‖g y - g x‖
⊢ ‖HSub.hSub (β := G) (f y - f x) ((φ : (a : E) → G) (y - x) : G)‖ ≤ C * ‖y - x‖

Tactic:
calc
    ‖f y - f x - φ (y - x)‖ = ‖f y - f x - (φ y - φ x)‖ := by simp
    _ = ‖f y - φ y - (f x - φ x)‖ := by congr 1; abel
    _ = ‖g y - g x‖ := by simp [g]
    _ ≤ C * ‖y - x‖ := Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le hg bound hs xs ys

Premises used: Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le, HSub.hSub, DFunLike.coe
-- 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
φ : E →L[𝕜] G
hf : DifferentiableOn 𝕜 f s
bound : ∀ x ∈ s, ‖fderivWithin 𝕜 f s x - φ‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
⊢ ‖HSub.hSub (β := G) (f y - f x) ((φ : (a : E) → G) (y - x) : G)‖ ≤ C * ‖y - x‖

Tactic:
hs.norm_image_sub_le_of_norm_hasFDerivWithin_le' (fun x hx => (hf x hx).hasFDerivWithinAt) bound
    xs ys

Premises used: Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le', DifferentiableWithinAt.hasFDerivWithinAt
-- 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
φ : E →L[𝕜] G
hf : ∀ x ∈ s, DifferentiableAt 𝕜 f x
bound : ∀ x ∈ s, ‖fderiv 𝕜 f x - φ‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
⊢ ‖HSub.hSub (β := G) (f y - f x) ((φ : (a : E) → G) (y - x) : G)‖ ≤ C * ‖y - x‖

Tactic:
hs.norm_image_sub_le_of_norm_hasFDerivWithin_le'
    (fun x hx => (hf x hx).hasFDerivAt.hasFDerivWithinAt) bound xs ys

Premises used: HasFDerivAt.hasFDerivWithinAt, DifferentiableAt.hasFDerivAt, 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
x_1 y : E
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hf' : ∀ x ∈ s, Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 f s x) 0
hx_1 : x_1 ∈ s
hy : y ∈ s
x : E
hx : x ∈ s
⊢ norm (E := E →L[𝕜] G) (fderivWithin 𝕜 f s x) ≤ 0

Tactic:
simp only [hf' x hx, norm_zero, le_rfl]

Premises used: le_rfl, norm_zero
-- 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
x y : E
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hf' : ∀ x ∈ s, Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 f s x) 0
hx : x ∈ s
hy : y ∈ s
⊢ ∀ x ∈ s, norm (E := E →L[𝕜] G) (fderivWithin 𝕜 f s x) ≤ 0

Tactic:
have bound : ∀ x ∈ s, ‖fderivWithin 𝕜 f s x‖ ≤ 0 := fun x hx => by
    simp only [hf' x hx, norm_zero, le_rfl]
-- 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
x y : E
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hf' : ∀ x ∈ s, Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 f s x) 0
hx : x ∈ s
hy : y ∈ s
bound : ∀ x ∈ s, norm (E := E →L[𝕜] G) (fderivWithin 𝕜 f s x) ≤ 0
⊢ f x = f y

Tactic:
simpa only [(dist_eq_norm _ _).symm, zero_mul, dist_le_zero, eq_comm] using
    hs.norm_image_sub_le_of_norm_fderivWithin_le hf bound hx hy

Premises used: dist_eq_norm, MulZeroClass.zero_mul, dist_le_zero, Convex.norm_image_sub_le_of_norm_fderivWithin_le, eq_comm, Eq.symm
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace 𝕜 G
E : Type u_5
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
f : E → G
hf : Differentiable 𝕜 f
hf' : ∀ (x : E), Eq (α := E →L[𝕜] G) (fderiv 𝕜 f x) 0
x_1 y : E
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
rw : Eq (α := E →L[𝕜] G) (fderiv 𝕜 f x) 0
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 f univ x) 0

Tactic:
rw [fderivWithin_univ]

Premises used: fderivWithin_univ
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace 𝕜 G
E : Type u_5
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
f : E → G
hf : Differentiable 𝕜 f
hf' : ∀ (x : E), Eq (α := E →L[𝕜] G) (fderiv 𝕜 f x) 0
x_1 y : E
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
⊢ Eq (α := E →L[𝕜] G) (fderiv 𝕜 f x) 0

Tactic:
hf' x
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace 𝕜 G
E : Type u_5
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
f : E → G
hf : Differentiable 𝕜 f
hf' : ∀ (x : E), Eq (α := E →L[𝕜] G) (fderiv 𝕜 f x) 0
x_1 y : E
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
⊢ Eq (α := E →L[𝕜] G) (fderiv 𝕜 f x) 0

Tactic:
exact hf' x
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace 𝕜 G
E : Type u_5
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
f : E → G
hf : Differentiable 𝕜 f
hf' : ∀ (x : E), Eq (α := E →L[𝕜] G) (fderiv 𝕜 f x) 0
x y : E
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ f x = f y

Tactic:
exact convex_univ.is_const_of_fderivWithin_eq_zero hf.differentiableOn
    (fun x _ => by rw [fderivWithin_univ]; exact hf' x) trivial trivial

Premises used: trivial, convex_univ, Convex.is_const_of_fderivWithin_eq_zero, Differentiable.differentiableOn
-- 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 g : E → G
s : Set E
x : E
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs' : UniqueDiffOn 𝕜 s
hf' : EqOn (β := E →L[𝕜] G) (fderivWithin 𝕜 f s) (fderivWithin 𝕜 g s) s
hx : x ∈ s
hfgx : f x = g x
y : E
hy : y ∈ s
suffices : f x - g x = f y - g y
⊢ f y = g y

Tactic:
suffices f x - g x = f y - g y by rwa [hfgx, sub_self, eq_comm, sub_eq_zero] at this
-- 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 g : E → G
s : Set E
x : E
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs' : UniqueDiffOn 𝕜 s
hf' : EqOn (β := E →L[𝕜] G) (fderivWithin 𝕜 f s) (fderivWithin 𝕜 g s) s
hx : x ∈ s
hfgx : f x = g x
y : E
hy : y ∈ s
⊢ f x - g x = f y - g y

Tactic:
hs.is_const_of_fderivWithin_eq_zero (hf.sub hg) (fun z hz => ?_) hx hy

Premises used: DifferentiableOn.sub, Convex.is_const_of_fderivWithin_eq_zero
-- 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 g : E → G
s : Set E
x : E
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs' : UniqueDiffOn 𝕜 s
hf' : EqOn (β := E →L[𝕜] G) (fderivWithin 𝕜 f s) (fderivWithin 𝕜 g s) s
hx : x ∈ s
hfgx : f x = g x
y : E
hy : y ∈ s
refine : ∀ (z : E) (hz : z ∈ s), Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f - g) s z) 0
⊢ f x - g x = f y - g y

Tactic:
refine hs.is_const_of_fderivWithin_eq_zero (hf.sub hg) (fun z hz => ?_) hx hy

Premises used: DifferentiableOn.sub, Convex.is_const_of_fderivWithin_eq_zero
-- 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 g : E → G
s : Set E
x : E
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs' : UniqueDiffOn 𝕜 s
hf' : EqOn (β := E →L[𝕜] G) (fderivWithin 𝕜 f s) (fderivWithin 𝕜 g s) s
hx : x ∈ s
hfgx : f x = g x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
rw : HSub.hSub (α := E →L[𝕜] G) (fderivWithin 𝕜 f s z) (fderivWithin 𝕜 g s z) = 0
rw₁ : Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 f s z) (fderivWithin 𝕜 g s z)
rw₂ rw₃ : Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 g s z) (fderivWithin 𝕜 g s z)
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f - g) s z) 0

Tactic:
rw [fderivWithin_sub (hs' _ hz) (hf _ hz) (hg _ hz), sub_eq_zero, hf' hz]

Premises used: sub_eq_zero, fderivWithin_sub
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
t : Set G
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' t)

Tactic:
Metric.isOpen_iff.mpr fun y ⟨hy, hy'⟩ ↦ ?_

Premises used: _private.0.IsOpen.isOpen_inter_preimage_of_fderiv_eq_zero.match_1, Iff.mpr, Exists, Metric.ball, HasSubset.Subset, Inter.inter, GT.gt, And, Metric.isOpen_iff, Set.preimage, OfNat.ofNat
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
t : Set G
refine : ∀ y ∈ s ∩ f ⁻¹' t, ∀ (hy : y ∈ s) (hy' : y ∈ f ⁻¹' t), ∃ ε > 0, ball y ε ⊆ s ∩ f ⁻¹' t
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' t)

Tactic:
refine Metric.isOpen_iff.mpr fun y ⟨hy, hy'⟩ ↦ ?_
-- 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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
t : Set G
y : E
h : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
obtain : ∀ (r : ℝ) (hr : r > 0) (h : ball y r ⊆ s), ∃ ε > 0, ball y ε ⊆ s ∩ f ⁻¹' t
⊢ ∃ ε > 0, ball y ε ⊆ s ∩ f ⁻¹' t

Tactic:
obtain ⟨r, hr, h⟩ := Metric.isOpen_iff.mp hs y hy

Premises used: Metric.isOpen_iff, 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
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
t : Set G
y : E
h_1 : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
r : ℝ
hr : r > 0
h : ball y r ⊆ s
⊢ ∃ ε > 0, ball y ε ⊆ s ∩ f ⁻¹' t

Tactic:
⟨r, hr, Set.subset_inter h fun x hx ↦ ?_⟩

Premises used: Set.subset_inter, 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
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
t : Set G
y : E
h_1 : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
r : ℝ
hr : r > 0
h : ball y r ⊆ s
refine : ∀ (x : E) (hx : x ∈ ball y r), x ∈ f ⁻¹' t
⊢ ∃ ε > 0, ball y ε ⊆ s ∩ f ⁻¹' t

Tactic:
refine ⟨r, hr, Set.subset_inter h fun x hx ↦ ?_⟩