awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ y ∈ Ico a x,
    ‖((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
t : ℝ
ht : t ∈ Icc a x
I : Icc a x ⊆ Icc a b
⊢ HasDerivWithinAt (fun (y : ℝ) ↦ taylorWithinEval f n (Icc a b) y x)
    (((↑n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t

Tactic:
(hasDerivWithinAt_taylorWithinEval_at_Icc x h (I ht) hf.of_succ hf').mono I

Premises used: hasDerivWithinAt_taylorWithinEval_at_Icc, HasDerivWithinAt.mono, ContDiffOn.of_succ
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ y ∈ Ico a x,
    ‖((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
t : ℝ
ht : t ∈ Icc a x
I : Icc a x ⊆ Icc a b
⊢ HasDerivWithinAt (fun (y : ℝ) ↦ taylorWithinEval f n (Icc a b) y x)
    (((↑n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t

Tactic:
exact (hasDerivWithinAt_taylorWithinEval_at_Icc x h (I ht) hf.of_succ hf').mono I

Premises used: hasDerivWithinAt_taylorWithinEval_at_Icc, HasDerivWithinAt.mono, ContDiffOn.of_succ
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ y ∈ Ico a x,
    ‖((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
⊢ ∀ t ∈ Icc a x,
    HasDerivWithinAt (fun (y : ℝ) ↦ taylorWithinEval f n (Icc a b) y x)
      (((↑n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t

Tactic:
have A : ∀ t ∈ Icc a x, HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
      (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t := by
    intro t ht
    have I : Icc a x ⊆ Icc a b := Icc_subset_Icc_right hx.2
    exact (hasDerivWithinAt_taylorWithinEval_at_Icc x h (I ht) hf.of_succ hf').mono I
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ y ∈ Ico a x,
    ‖((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
A :
  ∀ t ∈ Icc a x,
    HasDerivWithinAt (fun (y : ℝ) ↦ taylorWithinEval f n (Icc a b) y x)
      (((↑n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
⊢ ‖taylorWithinEval f n (Icc a b) x x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C * (x - a)

Tactic:
have := norm_image_sub_le_of_norm_deriv_le_segment' A h' x (right_mem_Icc.2 hx.1)
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ y ∈ Ico a x,
    ‖((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
A :
  ∀ t ∈ Icc a x,
    HasDerivWithinAt (fun (y : ℝ) ↦ taylorWithinEval f n (Icc a b) y x)
      (((↑n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
this :
  ‖taylorWithinEval f n (Icc a b) x x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C * (x - a)
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C * (x - a)

Tactic:
simp only [taylorWithinEval_self] at this

Premises used: taylorWithinEval_self
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ y ∈ Ico a x,
    ‖((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
A :
  ∀ t ∈ Icc a x,
    HasDerivWithinAt (fun (y : ℝ) ↦ taylorWithinEval f n (Icc a b) y x)
      (((↑n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
this : ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C * (x - a)
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / (↑n ! : ℝ)

Tactic:
this.trans_eq ?_

Premises used: LE.le.trans_eq
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ y ∈ Ico a x,
    ‖((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
A :
  ∀ t ∈ Icc a x,
    HasDerivWithinAt (fun (y : ℝ) ↦ taylorWithinEval f n (Icc a b) y x)
      (((↑n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
this : ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C * (x - a)
inr : (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C * (x - a) = C * (x - a) ^ (n + 1) / (↑n ! : ℝ)
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / (↑n ! : ℝ)

Tactic:
refine this.trans_eq ?_

Premises used: LE.le.trans_eq
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ y ∈ Ico a x,
    ‖((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
A :
  ∀ t ∈ Icc a x,
    HasDerivWithinAt (fun (y : ℝ) ↦ taylorWithinEval f n (Icc a b) y x)
      (((↑n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
this : ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C * (x - a)
inr : (↑n ! : ℝ)⁻¹ * (x - a) ^ n * C * (x - a) = C * (x - a) ^ (n + 1) / (↑n ! : ℝ)
⊢ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C * (x - a) = C * (x - a) ^ (n + 1) / (↑n ! : ℝ)

Tactic:
rw [abs_of_nonneg (sub_nonneg.mpr hx.1)]

Premises used: Iff.mpr, And.left, abs_of_nonneg, sub_nonneg
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ y ∈ Ico a x,
    ‖((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
A :
  ∀ t ∈ Icc a x,
    HasDerivWithinAt (fun (y : ℝ) ↦ taylorWithinEval f n (Icc a b) y x)
      (((↑n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
this : ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C * (x - a)
⊢ (↑n ! : ℝ)⁻¹ * (x - a) ^ n * C * (x - a) = C * (x - a) ^ (n + 1) / (↑n ! : ℝ)

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
inl :
  ∀ (hab : a ≤ a) (hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a a)),
    ∃ (C : ℝ), ∀ x ∈ Icc a a, ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ C * (x - a) ^ (n + 1)
inr : ∀ (h : a < b), ∃ (C : ℝ), ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1)
⊢ ∃ (C : ℝ), ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1)

Tactic:
rcases eq_or_lt_of_le hab with (rfl | h)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a a)
⊢ ∃ (C : ℝ), ∀ x ∈ Icc a a, ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ C * (x - a) ^ (n + 1)

Tactic:
⟨0, fun x hx => ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a a)
inl : ∀ (x : ℝ) (hx : x ∈ Icc a a), ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ 0 * (x - a) ^ (n + 1)
⊢ ∃ (C : ℝ), ∀ x ∈ Icc a a, ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ C * (x - a) ^ (n + 1)

Tactic:
refine ⟨0, fun x hx => ?_⟩
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a a)
x : ℝ
hx : x ∈ Icc a a
⊢ x = a

Tactic:
simpa [← le_antisymm_iff] using hx

Premises used: le_antisymm_iff
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a a)
x : ℝ
hx : x ∈ Icc a a
⊢ x = a

Tactic:
have : x = a := by simpa [← le_antisymm_iff] using hx
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a a)
x : ℝ
hx : x ∈ Icc a a
this : x = a
⊢ ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ 0 * (x - a) ^ (n + 1)

Tactic:
simp [← this]
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun (y : ℝ) ↦ ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
h₁ : ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ sSup (g '' Icc a b) / (↑n ! : ℝ) * (x - a) ^ (n + 1)
⊢ ∃ (C : ℝ), ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1)

Tactic:
use SupSet.sSup (g '' Icc a b) / (n !)

Premises used: Set.Icc, Nat.factorial, Set.image, SupSet.sSup
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun (y : ℝ) ↦ ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
x : ℝ
hx : x ∈ Icc a b
h₁ : ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ sSup (g '' Icc a b) * (x - a) ^ (n + 1) / (↑n ! : ℝ)
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ sSup (g '' Icc a b) / (↑n ! : ℝ) * (x - a) ^ (n + 1)

Tactic:
rw [div_mul_eq_mul_div₀]

Premises used: div_mul_eq_mul_div₀
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun (y : ℝ) ↦ ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
x : ℝ
hx : x ∈ Icc a b
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ sSup (g '' Icc a b) * (x - a) ^ (n + 1) / (↑n ! : ℝ)

Tactic:
taylor_mean_remainder_bound hab hf hx fun y => ?_

Premises used: taylor_mean_remainder_bound
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun (y : ℝ) ↦ ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
x : ℝ
hx : x ∈ Icc a b
h₁ : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ sSup (g '' Icc a b)
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ sSup (g '' Icc a b) * (x - a) ^ (n + 1) / (↑n ! : ℝ)

Tactic:
refine taylor_mean_remainder_bound hab hf hx fun y => ?_

Premises used: taylor_mean_remainder_bound
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun (y : ℝ) ↦ ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
x : ℝ
hx : x ∈ Icc a b
y : ℝ
⊢ y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ sSup (g '' Icc a b)

Tactic:
(hf.continuousOn_iteratedDerivWithin rfl.le <| uniqueDiffOn_Icc h).norm.le_sSup_image_Icc

Premises used: uniqueDiffOn_Icc, ContinuousOn.le_sSup_image_Icc, Set.Mem, ContDiffOn.continuousOn_iteratedDerivWithin, Eq.le, ContinuousOn.norm, rfl
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun (y : ℝ) ↦ ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
x : ℝ
hx : x ∈ Icc a b
y : ℝ
⊢ y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ sSup (g '' Icc a b)

Tactic:
exact (hf.continuousOn_iteratedDerivWithin rfl.le <| uniqueDiffOn_Icc h).norm.le_sSup_image_Icc

Premises used: uniqueDiffOn_Icc, ContinuousOn.le_sSup_image_Icc, ContDiffOn.continuousOn_iteratedDerivWithin, Eq.le, ContinuousOn.norm, rfl
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf :
  ∀ k ≤ n,
    let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
    let v : (t : ℝ) → F := fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
inl :
  ∀
    (hf :
      ∀ k ≤ n,
        let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x₀ - t) ^ k / (↑k ! : ℝ);
        let v : (t : ℝ) → F := fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x₀]] t;
        ∫ (t : ℝ) in x₀..x₀, u t • deriv v t = u x₀ • v x₀ - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x₀, deriv u t • v t),
    f x₀ - taylorWithinEval f n [[x₀, x₀]] x₀ x₀ =
      ∫ (t : ℝ) in x₀..x₀, ((x₀ - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x₀]] t
inr :
  ∀ (this : x₀ ≠ x),
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t

Tactic:
rcases eq_or_ne x₀ x with rfl | this

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x₀ : ℝ
n : ℕ
hf :
  ∀ k ≤ n,
    let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x₀ - t) ^ k / (↑k ! : ℝ);
    let v : (t : ℝ) → F := fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x₀]] t;
    ∫ (t : ℝ) in x₀..x₀, u t • deriv v t = u x₀ • v x₀ - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x₀, deriv u t • v t
⊢ f x₀ - taylorWithinEval f n [[x₀, x₀]] x₀ x₀ =
    ∫ (t : ℝ) in x₀..x₀, ((x₀ - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x₀]] t

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this : x₀ ≠ x
hf :
  ∀ k ≤ 0,
    let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
    let v : (t : ℝ) → F := fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
inr : f x - f x₀ = ∫ (t : ℝ) in x₀..x, derivWithin f [[x₀, x]] t
⊢ f x - taylorWithinEval f 0 [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x,
      (HPow.hPow (β := ℕ) (x - t) 0 / (↑0! : ℝ)) • iteratedDerivWithin (HAdd.hAdd (α := ℕ) 0 1) f [[x₀, x]] t

Tactic:
simp only [taylor_within_zero_eval, pow_zero, Nat.factorial_zero, Nat.cast_one, ne_eq,
      one_ne_zero, not_false_eq_true, div_self, zero_add, iteratedDerivWithin_one, one_smul]

Premises used: iteratedDerivWithin_one, taylor_within_zero_eval, zero_add, ne_eq, pow_zero, one_smul, Nat.factorial_zero, one_ne_zero, not_false_eq_true, Nat.cast_one, div_self
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this : x₀ ≠ x
hf :
  ∀ k ≤ 0,
    let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
    let v : (t : ℝ) → F := fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
⊢ ∫ (t : ℝ) in x₀..x, deriv (fun (t : ℝ) ↦ f t) t = f x - f x₀

Tactic:
simp only [nonpos_iff_eq_zero, sub_self, deriv_div_const, forall_eq, pow_zero,
      Nat.factorial_zero, Nat.cast_one, ne_eq, one_ne_zero, not_false_eq_true, div_self,
      iteratedDerivWithin_zero, one_smul, deriv_const', div_one, zero_smul,
      intervalIntegral.integral_zero, sub_zero] at hf

Premises used: deriv_const', sub_self, sub_zero, forall_eq, iteratedDerivWithin_zero, ne_eq, pow_zero, one_smul, zero_smul, intervalIntegral.integral_zero, Nat.factorial_zero, one_ne_zero, not_false_eq_true, div_one, Nat.cast_one, div_self, deriv_div_const, nonpos_iff_eq_zero
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this : x₀ ≠ x
hf : ∫ (t : ℝ) in x₀..x, deriv (fun (t : ℝ) ↦ f t) t = f x - f x₀
inr :
  Eq.{u_3 + 1} (α := F) (∫ (t : ℝ) in x₀..x, deriv (fun (t : ℝ) ↦ f t) t)
    (∫ (t : ℝ) in x₀..x, derivWithin f [[x₀, x]] t)
⊢ f x - f x₀ = ∫ (t : ℝ) in x₀..x, derivWithin f [[x₀, x]] t

Tactic:
rw [← hf]
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this : x₀ ≠ x
hf : ∫ (t : ℝ) in x₀..x, deriv (fun (t : ℝ) ↦ f t) t = f x - f x₀
inr : ∀ᵐ (x_1 : ℝ), x_1 ∈ Ι x₀ x → deriv (fun (t : ℝ) ↦ f t) x_1 = derivWithin f [[x₀, x]] x_1
⊢ Eq.{u_3 + 1} (α := F) (∫ (t : ℝ) in x₀..x, deriv (fun (t : ℝ) ↦ f t) t)
    (∫ (t : ℝ) in x₀..x, derivWithin f [[x₀, x]] t)

Tactic:
apply intervalIntegral.integral_congr_ae

Premises used: intervalIntegral.integral_congr_ae
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this : x₀ ≠ x
hf : ∫ (t : ℝ) in x₀..x, deriv (fun (t : ℝ) ↦ f t) t = f x - f x₀
a : ℝ
h : a ≠ x₀ → a ≠ x → a ∈ Ι x₀ x → deriv (fun (t : ℝ) ↦ f t) a = derivWithin f [[x₀, x]] a
⊢ a ≠ x₀ → a ≠ x → a ∈ Ι x₀ x → deriv (fun (t : ℝ) ↦ f t) a = derivWithin f [[x₀, x]] a

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this : x₀ ≠ x
hf : ∫ (t : ℝ) in x₀..x, deriv (fun (t : ℝ) ↦ f t) t = f x - f x₀
a : ℝ
h_1 : a ≠ x₀
h : a ≠ x → a ∈ Ι x₀ x → deriv (fun (t : ℝ) ↦ f t) a = derivWithin f [[x₀, x]] a
⊢ a ≠ x → a ∈ Ι x₀ x → deriv (fun (t : ℝ) ↦ f t) a = derivWithin f [[x₀, x]] a

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this : x₀ ≠ x
hf : ∫ (t : ℝ) in x₀..x, deriv (fun (t : ℝ) ↦ f t) t = f x - f x₀
a : ℝ
h_1 : a ≠ x₀
h_2 : a ≠ x
h : a ∈ Ι x₀ x → deriv (fun (t : ℝ) ↦ f t) a = derivWithin f [[x₀, x]] a
⊢ a ∈ Ι x₀ x → deriv (fun (t : ℝ) ↦ f t) a = derivWithin f [[x₀, x]] a

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this : x₀ ≠ x
hf : ∫ (t : ℝ) in x₀..x, deriv (fun (t : ℝ) ↦ f t) t = f x - f x₀
h : ∀ (a : ℝ), a ≠ x₀ → a ≠ x → a ∈ Ι x₀ x → deriv (fun (t : ℝ) ↦ f t) a = derivWithin f [[x₀, x]] a
⊢ ∀ᵐ (x_1 : ℝ), x_1 ∈ Ι x₀ x → deriv (fun (t : ℝ) ↦ f t) x_1 = derivWithin f [[x₀, x]] x_1

Tactic:
filter_upwards [MeasureTheory.volume.ae_ne x₀, MeasureTheory.volume.ae_ne x] with _ _ _ _

Premises used: MeasureTheory.Measure.ae_ne, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this : x₀ ≠ x
hf : ∫ (t : ℝ) in x₀..x, deriv (fun (t : ℝ) ↦ f t) t = f x - f x₀
a : ℝ
h : a ≠ x₀
h_1 : a ≠ x
h_2 : a ∈ Ι x₀ x
⊢ deriv (fun (t : ℝ) ↦ f t) a = derivWithin f [[x₀, x]] a

Tactic:
grind [derivWithin_of_mem_nhds, Icc_mem_nhds, uIcc]

Premises used: Set.uIcc, derivWithin_of_mem_nhds, Icc_mem_nhds
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this : x₀ ≠ x
n : ℕ
ih :
  ∀
    (hf :
      ∀ k ≤ n,
        let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
        let v : (t : ℝ) → F := fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t;
        ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t),
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
hf :
  ∀ k ≤ n + 1,
    let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
    let v : (t : ℝ) → F := fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
⊢ min x₀ x < max x₀ x

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this : x₀ ≠ x
n : ℕ
ih :
  ∀
    (hf :
      ∀ k ≤ n,
        let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
        let v : (t : ℝ) → F := fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t;
        ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t),
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
hf :
  ∀ k ≤ n + 1,
    let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
    let v : (t : ℝ) → F := fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
⊢ UniqueDiffOn ℝ [[x₀, x]]

Tactic:
have : UniqueDiffOn ℝ [[x₀, x]] := uniqueDiffOn_Icc (by grind)