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 g : E → G
s : Set E
x : E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : ∀ x ∈ s, Eq (α := E →L[𝕜] G) (fderiv 𝕜 f x) (fderiv 𝕜 g x)
hx : x ∈ s
hfgx : f x = g x
a : G
ha : EqOn f (fun (x : E) ↦ g x + a) s
⊢ EqOn f (fun (x : E) ↦ g x + 0) s

Tactic:
obtain rfl := left_eq_add.mp (hfgx.symm.trans (ha hx))

Premises used: left_eq_add, Iff.mp, Eq.symm, rfl, Eq.trans
-- 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 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : ∀ x ∈ s, Eq (α := E →L[𝕜] G) (fderiv 𝕜 f x) (fderiv 𝕜 g x)
hx : x ∈ s
hfgx : f x = g x
ha : EqOn f (fun (x : E) ↦ g x + 0) s
⊢ EqOn f g s

Tactic:
simpa using ha
-- 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 g : E → G
hf : Differentiable 𝕜 f
hg : Differentiable 𝕜 g
hf' : ∀ (x : E), Eq (α := E →L[𝕜] G) (fderiv 𝕜 f x) (fderiv 𝕜 g x)
x : E
hfgx : f x = g x
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
suffices : EqOn f g univ
⊢ f = g

Tactic:
suffices Set.univ.EqOn f g from funext fun x => this <| mem_univ 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 g : E → G
hf : Differentiable 𝕜 f
hg : Differentiable 𝕜 g
hf' : ∀ (x : E), Eq (α := E →L[𝕜] G) (fderiv 𝕜 f x) (fderiv 𝕜 g x)
x_1 : E
hfgx : f x_1 = g x_1
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 f univ x) (fderivWithin 𝕜 g univ x)

Tactic:
simpa using hf' _
-- 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 g : E → G
hf : Differentiable 𝕜 f
hg : Differentiable 𝕜 g
hf' : ∀ (x : E), Eq (α := E →L[𝕜] G) (fderiv 𝕜 f x) (fderiv 𝕜 g x)
x : E
hfgx : f x = g x
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ EqOn f g univ

Tactic:
exact convex_univ.eqOn_of_fderivWithin_eq hf.differentiableOn hg.differentiableOn
    uniqueDiffOn_univ (fun x _ => by simpa using hf' _) (mem_univ _) hfgx

Premises used: uniqueDiffOn_univ, convex_univ, Set.mem_univ, Differentiable.differentiableOn, Convex.eqOn_of_fderivWithin_eq
-- 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
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf' : IsLittleO (F := ℝ) (𝓝[s] x₀) f' fun (x : E) ↦ ‖x - x₀‖ ^ n
rw :
  ∀ (hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖‖x - x₀‖ ^ n‖) ⦃c : ℝ⦄,
    0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖‖x - x₀‖ ^ (n + 1)‖
⊢ IsLittleO.{u_1, u_4, 0} (E := G) (F := ℝ) (𝓝[s] x₀) (fun (x : E) ↦ f x - f x₀) fun (x : E) ↦ ‖x - x₀‖ ^ (n + 1)

Tactic:
rw [Asymptotics.isLittleO_iff] at hf' ⊢

Premises used: Asymptotics.isLittleO_iff
-- 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
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖‖x - x₀‖ ^ n‖
c : ℝ
hc : 0 < c
simp_rw : ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖‖x - x₀‖ ^ (n + 1)‖

Tactic:
simp_rw [norm_pow, pow_succ, ← mul_assoc, norm_norm]

Premises used: norm_pow, pow_succ, mul_assoc, norm_norm
-- 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
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖‖x - x₀‖ ^ n‖
c : ℝ
hc : 0 < c
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n

Tactic:
simp_rw [norm_pow, norm_norm] at hf'

Premises used: norm_pow, norm_norm
-- 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
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, x ∈ s

Tactic:
have h1 : ∀ᶠ x in 𝓝[s] x₀, x ∈ s := eventually_mem_nhdsWithin
-- 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
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
h1 : ∀ᶠ (x : E) in 𝓝[s] x₀, x ∈ s
h :
  ∀ (x : E) (hxs : x ∈ s) (h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖y - x₀‖ ^ n),
    [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n

Tactic:
filter_upwards [h1, hs.eventually_nhdsWithin_segment hx₀s (hf' hc)] with x hxs h

Premises used: Convex.eventually_nhdsWithin_segment
-- 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
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
h1 : ∀ᶠ (x : E) in 𝓝[s] x₀, x ∈ s
x : E
hxs : x ∈ s
h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖y - x₀‖ ^ n
⊢ [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n

Tactic:
⟨hs.segment_subset hx₀s hxs, fun y hy ↦ (h y hy).trans ?_⟩

Premises used: And.intro, LE.le.trans, Convex.segment_subset
-- 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
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
h1 : ∀ᶠ (x : E) in 𝓝[s] x₀, x ∈ s
x : E
hxs : x ∈ s
h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖y - x₀‖ ^ n
h₁ : ∀ (y : E) (hy : y ∈ [x₀ -[ℝ] x]), c * ‖y - x₀‖ ^ n ≤ c * ‖x - x₀‖ ^ n
⊢ [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n

Tactic:
refine ⟨hs.segment_subset hx₀s hxs, fun y hy ↦ (h y hy).trans ?_⟩
-- 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
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
h1 : ∀ᶠ (x : E) in 𝓝[s] x₀, x ∈ s
x : E
hxs : x ∈ s
h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖y - x₀‖ ^ n
y : E
hy : y ∈ [x₀ -[ℝ] x]
h₁ : ‖y - x₀‖ ≤ ‖x - x₀‖
⊢ c * ‖y - x₀‖ ^ n ≤ c * ‖x - x₀‖ ^ n

Tactic:
gcongr
-- 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
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
h1 : ∀ᶠ (x : E) in 𝓝[s] x₀, x ∈ s
x : E
hxs : x ∈ s
h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖y - x₀‖ ^ n
y : E
hy : y ∈ [x₀ -[ℝ] x]
⊢ ‖y - x₀‖ ≤ ‖x - x₀‖

Tactic:
norm_sub_le_of_mem_segment hy

Premises used: norm_sub_le_of_mem_segment
-- 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
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
h1 : ∀ᶠ (x : E) in 𝓝[s] x₀, x ∈ s
x : E
hxs : x ∈ s
h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖y - x₀‖ ^ n
y : E
hy : y ∈ [x₀ -[ℝ] x]
⊢ ‖y - x₀‖ ≤ ‖x - x₀‖

Tactic:
exact norm_sub_le_of_mem_segment hy

Premises used: norm_sub_le_of_mem_segment
-- 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
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n

Tactic:
have : ∀ᶠ x in 𝓝[s] x₀, segment ℝ x₀ x ⊆ s ∧ ∀ y ∈ segment ℝ x₀ x, ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n := by
    have h1 : ∀ᶠ x in 𝓝[s] x₀, x ∈ s := eventually_mem_nhdsWithin
    filter_upwards [h1, hs.eventually_nhdsWithin_segment hx₀s (hf' hc)] with x hxs h
    refine ⟨hs.segment_subset hx₀s hxs, fun y hy ↦ (h y hy).trans ?_⟩
    gcongr
    exact norm_sub_le_of_mem_segment 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
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
this : ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
x : E
h :
  ∀ (h_segment : [x₀ -[ℝ] x] ⊆ s) (h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n),
    ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖
⊢ ([x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n) → ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖

Tactic:
⟨h_segment, h⟩
-- 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
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
this : ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
h :
  ∀ (x : E) (h_segment : [x₀ -[ℝ] x] ⊆ s) (h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n),
    ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖

Tactic:
filter_upwards [this] with x ⟨h_segment, h⟩
-- 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
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
this : ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
x : E
h_segment : [x₀ -[ℝ] x] ⊆ s
h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
⊢ ‖HSub.hSub (α := G) ((fun (x : E) ↦ f x - f x₀) x) ((fun (x : E) ↦ f x - f x₀) x₀)‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖

Tactic:
(convex_segment x₀ x).norm_image_sub_le_of_norm_hasFDerivWithin_le (f := fun x ↦ f x - f x₀)
      (y := x) (x := x₀) (s := segment ℝ x₀ x) ?_ h
      (left_mem_segment ℝ x₀ x)
      (right_mem_segment ℝ x₀ x)

Premises used: Real, left_mem_segment, Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le, right_mem_segment, convex_segment
-- 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
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
this : ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
x : E
h_segment : [x₀ -[ℝ] x] ⊆ s
h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
h₁ : ‖f x - f x₀‖ = ‖f x - f x₀ - (f x₀ - f x₀)‖
h₂ : ∀ x_1 ∈ [x₀ -[ℝ] x], HasFDerivWithinAt (fun (x : E) ↦ f x - f x₀) (f' x_1) [x₀ -[ℝ] x] x_1
⊢ ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖

Tactic:
convert!
    (convex_segment x₀ x).norm_image_sub_le_of_norm_hasFDerivWithin_le (f := fun x ↦ f x - f x₀)
      (y := x) (x := x₀) (s := segment ℝ x₀ x) ?_ h
      (left_mem_segment ℝ x₀ x)
      (right_mem_segment ℝ x₀ x) using 1

Premises used: Real, left_mem_segment, Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le, right_mem_segment, convex_segment
-- 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
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
this : ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
x : E
h_segment : [x₀ -[ℝ] x] ⊆ s
h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
⊢ ‖f x - f x₀‖ = ‖f x - f x₀ - (f x₀ - f x₀)‖

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
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
this : ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
x : E
h_segment : [x₀ -[ℝ] x] ⊆ s
h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
h₁ : ∀ x_1 ∈ [x₀ -[ℝ] x], HasFDerivWithinAt f (f' x_1) [x₀ -[ℝ] x] x_1
⊢ ∀ x_1 ∈ [x₀ -[ℝ] x], HasFDerivWithinAt (fun (x : E) ↦ f x - f x₀) (f' x_1) [x₀ -[ℝ] x] x_1

Tactic:
simp only [hasFDerivWithinAt_sub_const_iff]

Premises used: hasFDerivWithinAt_sub_const_iff
-- 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
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
this : ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
x : E
h_segment : [x₀ -[ℝ] x] ⊆ s
h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
⊢ ∀ x_1 ∈ [x₀ -[ℝ] x], HasFDerivWithinAt f (f' x_1) [x₀ -[ℝ] x] x_1

Tactic:
fun x hx ↦ (hff' x (h_segment hx)).mono h_segment

Premises used: 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
f : E → G
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
this : ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
x : E
h_segment : [x₀ -[ℝ] x] ⊆ s
h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
⊢ ∀ x_1 ∈ [x₀ -[ℝ] x], HasFDerivWithinAt f (f' x_1) [x₀ -[ℝ] x] x_1

Tactic:
exact fun x hx ↦ (hff' x (h_segment hx)).mono h_segment

Premises used: HasFDerivWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf' : IsLittleO (F := ℝ) (𝓝[s] x₀) f' fun (x : ℝ) ↦ (x - x₀) ^ n
refine_2 :
  ∀ (h : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - f x₀) fun (x : ℝ) ↦ ‖x - x₀‖ ^ (n + 1)),
    IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - f x₀) fun (x : ℝ) ↦ (x - x₀) ^ (n + 1)
refine_1 :
  IsLittleO.{0, u_1, 0} (E := ℝ →L[ℝ] E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ toSpanSingleton ℝ (f' x)) fun (x : ℝ) ↦
    ‖x - x₀‖ ^ n
⊢ IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - f x₀) fun (x : ℝ) ↦ (x - x₀) ^ (n + 1)

Tactic:
have h := hs.isLittleO_pow_succ hx₀s hff' ?_ (n := n)
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf' : IsLittleO (F := ℝ) (𝓝[s] x₀) f' fun (x : ℝ) ↦ (x - x₀) ^ n
h : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - f x₀) fun (x : ℝ) ↦ ‖x - x₀‖ ^ (n + 1)
refine_2 :
  ∀ (h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖‖x - x₀‖ ^ (n + 1)‖) ⦃c : ℝ⦄,
    0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖(x - x₀) ^ (n + 1)‖
⊢ IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - f x₀) fun (x : ℝ) ↦ (x - x₀) ^ (n + 1)

Tactic:
rw [Asymptotics.isLittleO_iff] at h ⊢

Premises used: Asymptotics.isLittleO_iff
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf' : IsLittleO (F := ℝ) (𝓝[s] x₀) f' fun (x : ℝ) ↦ (x - x₀) ^ n
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖‖x - x₀‖ ^ (n + 1)‖
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖(x - x₀) ^ (n + 1)‖

Tactic:
simpa using h
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf' : IsLittleO (F := ℝ) (𝓝[s] x₀) f' fun (x : ℝ) ↦ (x - x₀) ^ n
refine_1 :
  ∀ (hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖(x - x₀) ^ n‖) ⦃c : ℝ⦄,
    0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, norm (E := ℝ →L[ℝ] E) (toSpanSingleton ℝ (f' x)) ≤ c * ‖‖x - x₀‖ ^ n‖
⊢ IsLittleO.{0, u_1, 0} (E := ℝ →L[ℝ] E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ toSpanSingleton ℝ (f' x)) fun (x : ℝ) ↦
    ‖x - x₀‖ ^ n

Tactic:
rw [Asymptotics.isLittleO_iff] at hf' ⊢

Premises used: Asymptotics.isLittleO_iff
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖(x - x₀) ^ n‖
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖(x - x₀) ^ n‖

Tactic:
hf'
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖(x - x₀) ^ n‖
h :
  ∀ (c : ℝ) (hc : 0 < c) (x : ℝ),
    norm (E := ℝ →L[ℝ] E) (toSpanSingleton ℝ (f' x)) ≤ c * ‖‖x - x₀‖ ^ n‖ ↔ ‖f' x‖ ≤ c * ‖(x - x₀) ^ n‖
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, norm (E := ℝ →L[ℝ] E) (toSpanSingleton ℝ (f' x)) ≤ c * ‖‖x - x₀‖ ^ n‖

Tactic:
convert! hf' using 4 with c hc x
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖(x - x₀) ^ n‖
c : ℝ
hc : 0 < c
x : ℝ
⊢ norm (E := ℝ →L[ℝ] E) (toSpanSingleton ℝ (f' x)) ≤ c * ‖‖x - x₀‖ ^ n‖ ↔ ‖f' x‖ ≤ c * ‖(x - x₀) ^ n‖

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 f' : 𝕜 → G
s : Set 𝕜
x_1 y : 𝕜
C : ℝ
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x_1 ∈ s
ys : y ∈ s
x : 𝕜
hx : x ∈ s
⊢ norm (E := 𝕜 →L[𝕜] G) (toSpanSingleton 𝕜 (f' x)) ≤ ‖f' x‖

Tactic:
simp