awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f f' : 𝕜 → G
s : Set 𝕜
C : ℝ≥0
hs : Convex ℝ s
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C
x : 𝕜
hx : x ∈ s
⊢ nnnorm (E := 𝕜 →L[𝕜] G) (toSpanSingleton 𝕜 (f' x)) ≤ ‖f' x‖₊

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
x y : 𝕜
C : ℝ
hf : DifferentiableOn 𝕜 f s
bound : ∀ x ∈ s, ‖derivWithin 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_hasDerivWithin_le (fun x hx => (hf x hx).hasDerivWithinAt) bound xs
    ys

Premises used: DifferentiableWithinAt.hasDerivWithinAt, Convex.norm_image_sub_le_of_norm_hasDerivWithin_le
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
C : ℝ≥0
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
bound : ∀ x ∈ s, ‖derivWithin f s x‖₊ ≤ C
⊢ LipschitzOnWith C f s

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

Premises used: DifferentiableWithinAt.hasDerivWithinAt, Convex.lipschitzOnWith_of_nnnorm_hasDerivWithin_le
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
x y : 𝕜
C : ℝ
hf : ∀ x ∈ s, DifferentiableAt 𝕜 f x
bound : ∀ x ∈ s, ‖deriv 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_hasDerivWithin_le
    (fun x hx => (hf x hx).hasDerivAt.hasDerivWithinAt) bound xs ys

Premises used: HasDerivAt.hasDerivWithinAt, DifferentiableAt.hasDerivAt, Convex.norm_image_sub_le_of_norm_hasDerivWithin_le
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
C : ℝ≥0
hf : ∀ x ∈ s, DifferentiableAt 𝕜 f x
bound : ∀ x ∈ s, ‖deriv f x‖₊ ≤ C
hs : Convex ℝ s
⊢ LipschitzOnWith C f s

Tactic:
hs.lipschitzOnWith_of_nnnorm_hasDerivWithin_le
    (fun x hx => (hf x hx).hasDerivAt.hasDerivWithinAt) bound

Premises used: HasDerivAt.hasDerivWithinAt, DifferentiableAt.hasDerivAt, Convex.lipschitzOnWith_of_nnnorm_hasDerivWithin_le
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : 𝕜 → G
C : ℝ≥0
hf : Differentiable 𝕜 f
bound : ∀ (x : 𝕜), ‖deriv f x‖₊ ≤ C
⊢ LipschitzWith C f

Tactic:
lipschitzOnWith_univ.1 <|
    convex_univ.lipschitzOnWith_of_nnnorm_deriv_le (fun x _ => hf x) fun x _ => bound x

Premises used: convex_univ, lipschitzOnWith_univ, Iff.mp, Convex.lipschitzOnWith_of_nnnorm_deriv_le
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : 𝕜 → G
hf : Differentiable 𝕜 f
hf' : ∀ (x : 𝕜), deriv f x = 0
x y z : 𝕜
⊢ Eq (α := 𝕜 →L[𝕜] G) (fderiv 𝕜 f z) 0

Tactic:
simp [← toSpanSingleton_deriv, hf']

Premises used: toSpanSingleton_deriv
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (deriv f) 0 s
t : Set G
x : 𝕜
hx : x ∈ s
⊢ Eq (α := 𝕜 →L[𝕜] G) (fderiv 𝕜 f x) (0 x)

Tactic:
simp [← toSpanSingleton_deriv, hf' hx]

Premises used: toSpanSingleton_deriv
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (deriv f) 0 s
x : 𝕜
hx : x ∈ s
h : Eq.{u_4 + 1} (α := G) (((fderiv 𝕜 f x : 𝕜 →L[𝕜] G) : (a : 𝕜) → G) 1 : G) ((0 x : (a : 𝕜) → G) 1 : G)
⊢ Eq (α := 𝕜 →L[𝕜] G) (fderiv 𝕜 f x) (0 x)

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (deriv f) 0 s
x : 𝕜
hx : x ∈ s
⊢ Eq.{u_4 + 1} (α := G) (((fderiv 𝕜 f x : 𝕜 →L[𝕜] G) : (a : 𝕜) → G) 1 : G) ((0 x : (a : 𝕜) → G) 1 : G)

Tactic:
simp [← toSpanSingleton_deriv, hf' hx]

Premises used: toSpanSingleton_deriv
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (deriv f) 0 s
x y : 𝕜
hx : x ∈ s
hy : y ∈ s
a : 𝕜
ha : a ∈ s
h : Eq.{u_4 + 1} (α := G) (((fderiv 𝕜 f a : 𝕜 →L[𝕜] G) : (a : 𝕜) → G) 1 : G) ((0 a : (a : 𝕜) → G) 1 : G)
⊢ Eq (α := 𝕜 →L[𝕜] G) (fderiv 𝕜 f a) (0 a)

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (deriv f) 0 s
x y : 𝕜
hx : x ∈ s
hy : y ∈ s
a : 𝕜
ha : a ∈ s
⊢ Eq.{u_4 + 1} (α := G) (((fderiv 𝕜 f a : 𝕜 →L[𝕜] G) : (a : 𝕜) → G) 1 : G) ((0 a : (a : 𝕜) → G) 1 : G)

Tactic:
simp [← toSpanSingleton_deriv, hf' ha]

Premises used: toSpanSingleton_deriv
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
s : Set 𝕜
f g : 𝕜 → G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (deriv f) (deriv g) s
x : 𝕜
hx : x ∈ s
⊢ Eq (α := 𝕜 →L[𝕜] G) (fderiv 𝕜 f x) (fderiv 𝕜 g x)

Tactic:
simp [← toSpanSingleton_deriv, hf' hx]

Premises used: toSpanSingleton_deriv
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
s : Set 𝕜
x : 𝕜
f g : 𝕜 → G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (deriv f) (deriv g) s
hx : x ∈ s
hfgx : f x = g x
⊢ EqOn f g s

Tactic:
hs.eqOn_of_fderiv_eq hs' hf hg (fun _ hx ↦ ContinuousLinearMap.ext_ring (hf' hx)) hx hfgx

Premises used: ContinuousLinearMap.ext_ring, IsOpen.eqOn_of_fderiv_eq
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
rw :
  ∀ ⦃c : ℝ⦄,
    0 < c →
      ∀ᶠ (x_1 : G × G) in 𝓝 (x, x),
        ‖HSub.hSub (β := H) (f x_1.1 - f x_1.2) ((f' x : (a : G) → H) (x_1.1 - x_1.2) : H)‖ ≤ c * ‖x_1.1 - x_1.2‖
⊢ HasStrictFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' x) x

Tactic:
rw [hasStrictFDerivAt_iff_isLittleO, isLittleO_iff]

Premises used: hasStrictFDerivAt_iff_isLittleO, Asymptotics.isLittleO_iff
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
⊢ ∀ ⦃c : ℝ⦄,
    0 < c →
      ∀ᶠ (x_1 : G × G) in 𝓝 (x, x),
        ‖HSub.hSub (β := H) (f x_1.1 - f x_1.2) ((f' x : (a : G) → H) (x_1.1 - x_1.2) : H)‖ ≤ c * ‖x_1.1 - x_1.2‖

Tactic:
fun c hc => Metric.eventually_nhds_iff_ball.mpr ?_

Premises used: Iff.mpr, setOf, Metric.eventually_nhds_iff_ball
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
refine :
  ∀ (c : ℝ) (hc : 0 < c),
    ∃ ε > 0,
      ∀ y ∈ ball (x, x) ε, ‖HSub.hSub (β := H) (f y.1 - f y.2) ((f' x : (a : G) → H) (y.1 - y.2) : H)‖ ≤ c * ‖y.1 - y.2‖
⊢ ∀ ⦃c : ℝ⦄,
    0 < c →
      ∀ᶠ (x_1 : G × G) in 𝓝 (x, x),
        ‖HSub.hSub (β := H) (f x_1.1 - f x_1.2) ((f' x : (a : G) → H) (x_1.1 - x_1.2) : H)‖ ≤ c * ‖x_1.1 - x_1.2‖

Tactic:
refine fun c hc => Metric.eventually_nhds_iff_ball.mpr ?_

Premises used: Iff.mpr, Metric.eventually_nhds_iff_ball
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
rcases :
  ∀ (ε : ℝ) (ε0 : ε > 0)
    (hε :
      ball x ε ⊆ {x : G | (fun (y : G) ↦ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c),
    ∃ ε > 0,
      ∀ y ∈ ball (x, x) ε, ‖HSub.hSub (β := H) (f y.1 - f y.2) ((f' x : (a : G) → H) (y.1 - y.2) : H)‖ ≤ c * ‖y.1 - y.2‖
⊢ ∃ ε > 0,
    ∀ y ∈ ball (x, x) ε, ‖HSub.hSub (β := H) (f y.1 - f y.2) ((f' x : (a : G) → H) (y.1 - y.2) : H)‖ ≤ c * ‖y.1 - y.2‖

Tactic:
rcases Metric.mem_nhds_iff.mp (inter_mem hder (hcont <| ball_mem_nhds _ hc)) with ⟨ε, ε0, hε⟩

Premises used: Filter.inter_mem, Metric.ball_mem_nhds, Metric.mem_nhds_iff, Iff.mp
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x : G | (fun (y : G) ↦ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
⊢ ∃ ε > 0,
    ∀ y ∈ ball (x, x) ε, ‖HSub.hSub (β := H) (f y.1 - f y.2) ((f' x : (a : G) → H) (y.1 - y.2) : H)‖ ≤ c * ‖y.1 - y.2‖

Tactic:
⟨ε, ε0, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x : G | (fun (y : G) ↦ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
refine :
  ∀ y ∈ ball (x, x) ε, ‖HSub.hSub (β := H) (f y.1 - f y.2) ((f' x : (a : G) → H) (y.1 - y.2) : H)‖ ≤ c * ‖y.1 - y.2‖
⊢ ∃ ε > 0,
    ∀ y ∈ ball (x, x) ε, ‖HSub.hSub (β := H) (f y.1 - f y.2) ((f' x : (a : G) → H) (y.1 - y.2) : H)‖ ≤ c * ‖y.1 - y.2‖

Tactic:
refine ⟨ε, ε0, ?_⟩
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x : G | (fun (y : G) ↦ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
a b : G
h : (a, b) ∈ ball (x, x) ε
⊢ a ∈ ball x ε ∧ b ∈ ball x ε

Tactic:
rw [← ball_prod_same, prodMk_mem_set_prod_eq] at h

Premises used: Set.prodMk_mem_set_prod_eq, ball_prod_same
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x : G | (fun (y : G) ↦ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
a b : G
h : a ∈ ball x ε ∧ b ∈ ball x ε
x' : G
H' : x' ∈ ball x ε
rw : dist (f' x') (f' x) ≤ c
⊢ ‖f' x' - f' x‖ ≤ c

Tactic:
rw [← dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x : G | (fun (y : G) ↦ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
a b : G
h : a ∈ ball x ε ∧ b ∈ ball x ε
x' : G
H' : x' ∈ ball x ε
⊢ dist (f' x') (f' x) ≤ c

Tactic:
le_of_lt (hε H').2

Premises used: le_of_lt, And.right
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x : G | (fun (y : G) ↦ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
a b : G
h : a ∈ ball x ε ∧ b ∈ ball x ε
x' : G
H' : x' ∈ ball x ε
⊢ dist (f' x') (f' x) ≤ c

Tactic:
exact le_of_lt (hε H').2

Premises used: le_of_lt
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x : G | (fun (y : G) ↦ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
a b : G
h : a ∈ ball x ε ∧ b ∈ ball x ε
⊢ ∀ x' ∈ ball x ε, ‖f' x' - f' x‖ ≤ c

Tactic:
have hf' : ∀ x' ∈ ball x ε, ‖f' x' - f' x‖ ≤ c := fun x' H' => by
    rw [← dist_eq_norm]
    exact le_of_lt (hε H').2
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x : G | (fun (y : G) ↦ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
a b : G
h : a ∈ ball x ε ∧ b ∈ ball x ε
hf' : ∀ x' ∈ ball x ε, ‖f' x' - f' x‖ ≤ c
this : NormedSpace ℝ G := NormedSpace.restrictScalars ℝ 𝕜 G
⊢ ‖HSub.hSub (β := H) (f (a, b).1 - f (a, b).2) ((f' x : (a : G) → H) ((a, b).1 - (a, b).2) : H)‖ ≤
    c * ‖(a, b).1 - (a, b).2‖

Tactic:
(convex_ball _ _).norm_image_sub_le_of_norm_hasFDerivWithin_le' ?_ hf' h.2 h.1

Premises used: convex_ball, And.right, And.left, Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le'
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x : G | (fun (y : G) ↦ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
a b : G
h : a ∈ ball x ε ∧ b ∈ ball x ε
hf' : ∀ x' ∈ ball x ε, ‖f' x' - f' x‖ ≤ c
this : NormedSpace ℝ G := NormedSpace.restrictScalars ℝ 𝕜 G
refine : ∀ x_1 ∈ ball x ε, HasFDerivWithinAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' x_1) (ball x ε) x_1
⊢ ‖HSub.hSub (β := H) (f (a, b).1 - f (a, b).2) ((f' x : (a : G) → H) ((a, b).1 - (a, b).2) : H)‖ ≤
    c * ‖(a, b).1 - (a, b).2‖

Tactic:
refine (convex_ball _ _).norm_image_sub_le_of_norm_hasFDerivWithin_le' ?_ hf' h.2 h.1

Premises used: convex_ball, And.right, And.left, Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le'
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x : G | (fun (y : G) ↦ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
a b : G
h : a ∈ ball x ε ∧ b ∈ ball x ε
hf' : ∀ x' ∈ ball x ε, ‖f' x' - f' x‖ ≤ c
this : NormedSpace ℝ G := NormedSpace.restrictScalars ℝ 𝕜 G
⊢ ∀ x_1 ∈ ball x ε, HasFDerivWithinAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' x_1) (ball x ε) x_1

Tactic:
fun y hy => (hε hy).1.hasFDerivWithinAt

Premises used: HasFDerivAt.hasFDerivWithinAt, And.left
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
H : Type u_5
inst_3 : NormedAddCommGroup H
inst_4 : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x : G | (fun (y : G) ↦ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
a b : G
h : a ∈ ball x ε ∧ b ∈ ball x ε
hf' : ∀ x' ∈ ball x ε, ‖f' x' - f' x‖ ≤ c
this : NormedSpace ℝ G := NormedSpace.restrictScalars ℝ 𝕜 G
⊢ ∀ x_1 ∈ ball x ε, HasFDerivWithinAt.{u_3, u_4, u_5} (𝕜 := 𝕜) f (f' x_1) (ball x ε) x_1

Tactic:
exact fun y hy => (hε hy).1.hasFDerivWithinAt

Premises used: HasFDerivAt.hasFDerivWithinAt, And.left
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f f' : 𝕜 → G
x : 𝕜
hder : ∀ᶠ (y : 𝕜) in 𝓝 x, HasDerivAt f (f' y) y
hcont : ContinuousAt f' x
⊢ HasStrictDerivAt f (f' x) x

Tactic:
hasStrictFDerivAt_of_hasFDerivAt_of_continuousAt (hder.mono fun _ hy => hy.hasFDerivAt) <|
    (smulRightL 𝕜 𝕜 G 1).continuous.continuousAt.comp hcont

Premises used: hasStrictFDerivAt_of_hasFDerivAt_of_continuousAt, HasDerivAt.hasFDerivAt, ContinuousLinearMap.smulRightL, Filter.Eventually.mono, Continuous.continuousAt, HasDerivAtFilter, ContinuousLinearMap.continuous, ContinuousAt.comp, OfNat.ofNat, HasStrictDerivAt, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
apply : Tendsto (fun (y : ℝ) ↦ 1 + c * (y - x)) (𝓝 x) (𝓝 (1 + c * (x - x)))
⊢ Tendsto (fun (y : ℝ) ↦ 1 + c * (y - x)) l (𝓝 (1 + c * (x - x)))

Tactic:
apply Tendsto.mono_left _ (hl.trans nhdsWithin_le_nhds)

Premises used: nhdsWithin_le_nhds, Filter.Tendsto.mono_left, LE.le.trans
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
⊢ Tendsto (fun (y : ℝ) ↦ 1 + c * (y - x)) (𝓝 x) (𝓝 (1 + c * (x - x)))

Tactic:
((tendsto_id.sub_const x).const_mul c).const_add 1

Premises used: Filter.tendsto_id, Filter.Tendsto.sub_const, Filter.Tendsto.const_mul, Filter.Tendsto.const_add, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
⊢ Tendsto (fun (y : ℝ) ↦ 1 + c * (y - x)) (𝓝 x) (𝓝 (1 + c * (x - x)))

Tactic:
exact ((tendsto_id.sub_const x).const_mul c).const_add 1

Premises used: Filter.tendsto_id, Filter.Tendsto.sub_const, Filter.Tendsto.const_mul, Filter.Tendsto.const_add, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
⊢ Tendsto (fun (y : ℝ) ↦ 1 + c * (y - x)) l (𝓝 (1 + c * (x - x)))

Tactic:
have : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 (1 + c * (x - x))) := by
      apply Tendsto.mono_left _ (hl.trans nhdsWithin_le_nhds)
      exact ((tendsto_id.sub_const x).const_mul c).const_add 1
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
this : Tendsto (fun (y : ℝ) ↦ 1 + c * (y - x)) l (𝓝 (1 + c * (x - x)))
⊢ Tendsto (β := ℝ) (fun (y : ℝ) ↦ 1 + c * (y - x)) l (𝓝 1)

Tactic:
simp only [_root_.sub_self, add_zero, mul_zero] at this

Premises used: sub_self, MulZeroClass.mul_zero, add_zero
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
this : Tendsto (β := ℝ) (fun (y : ℝ) ↦ 1 + c * (y - x)) l (𝓝 1)
apply : ∀ᶠ (x_1 : ℝ) in 𝓝[≠] x, 1 + c * (x_1 - x) = (x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)
⊢ Tendsto (β := ℝ) (fun (y : ℝ) ↦ (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) l (𝓝 1)

Tactic:
apply Tendsto.congr' (Eventually.filter_mono hl _) this

Premises used: Filter.Eventually.filter_mono, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
this : Tendsto (β := ℝ) (fun (y : ℝ) ↦ 1 + c * (y - x)) l (𝓝 1)
h :
  ∀ (y : ℝ) (hy : Membership.mem (γ := Set ℝ) {x}ᶜ y),
    1 + c * (y - x) = (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[≠] x, 1 + c * (x_1 - x) = (x_1 + c * HPow.hPow (β := ℕ) (x_1 - x) 2 - x) / (x_1 - x)

Tactic:
filter_upwards [self_mem_nhdsWithin] with y hy

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
this : Tendsto (β := ℝ) (fun (y : ℝ) ↦ 1 + c * (y - x)) l (𝓝 1)
y : ℝ
hy : Membership.mem (γ := Set ℝ) {x}ᶜ y
⊢ 1 + c * (y - x) = (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)

Tactic:
field [sub_ne_zero.2 hy]

Premises used: Iff.mpr, sub_ne_zero
-- Module: Mathlib.Analysis.Calculus.Monotone
Goal:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun (y : ℝ) ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun (y : ℝ) ↦ y + c * HPow.hPow (β := ℕ) (y - x) 2) l l
⊢ Tendsto (β := ℝ) (fun (y : ℝ) ↦ (y + c * HPow.hPow (β := ℕ) (y - x) 2 - x) / (y - x)) l (𝓝 1)

Tactic:
have L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1) := by
    have : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 (1 + c * (x - x))) := by
      apply Tendsto.mono_left _ (hl.trans nhdsWithin_le_nhds)
      exact ((tendsto_id.sub_const x).const_mul c).const_add 1
    simp only [_root_.sub_self, add_zero, mul_zero] at this
    apply Tendsto.congr' (Eventually.filter_mono hl _) this
    filter_upwards [self_mem_nhdsWithin] with y hy
    field [sub_ne_zero.2 hy]