awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ (n + 1)) [[x₀, x]]
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n ≠ 0
rcases :
  ∀ (y : ℝ) (hy : y ∈ uIoo x₀ x)
    (h :
      f x - taylorWithinEval f n [[x₀, x]] x₀ x =
        ((x - y) ^ n / (↑n ! : ℝ) * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) /
            (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n)) •
          iteratedDerivWithin (n + 1) f [[x₀, x]] y),
    ∃ x' ∈ uIoo x₀ x,
      f x - taylorWithinEval f n [[x₀, x]] x₀ x =
        iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)

Tactic:
rcases taylor_mean_remainder hx hf hf' gcont (fun y _ => monomial_has_deriv_aux y x _) hg' with
    ⟨y, hy, h⟩

Premises used: monomial_has_deriv_aux, taylor_mean_remainder
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ (n + 1)) [[x₀, x]]
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ((x - y) ^ n / (↑n ! : ℝ) * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) /
        (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f [[x₀, x]] y
right :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)

Tactic:
use y, hy
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ (n + 1)) [[x₀, x]]
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ((x - y) ^ n / (↑n ! : ℝ) * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) /
        (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f [[x₀, x]] y
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    (-((x - y) ^ n / (↑n ! : ℝ) * (x - x₀) ^ (n + 1)) / (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f [[x₀, x]] y

Tactic:
simp only [sub_self, zero_pow, Ne, Nat.succ_ne_zero, not_false_iff, zero_sub, mul_neg] at h

Premises used: sub_self, Ne, Nat.succ_ne_zero, not_false_iff, zero_pow, zero_sub, mul_neg
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ (n + 1)) [[x₀, x]]
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    (-((x - y) ^ n / (↑n ! : ℝ) * (x - x₀) ^ (n + 1)) / (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f [[x₀, x]] y
right :
  ((x - y) ^ n / (↑n ! : ℝ) * (x - x₀) ^ (n + 1) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f [[x₀, x]] y =
    iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)

Tactic:
rw [h, neg_div, ← div_neg, neg_mul, neg_neg]

Premises used: neg_div, neg_neg, div_neg, neg_mul
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ (n + 1)) [[x₀, x]]
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    (-((x - y) ^ n / (↑n ! : ℝ) * (x - x₀) ^ (n + 1)) / (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f [[x₀, x]] y
⊢ ((x - y) ^ n / (↑n ! : ℝ) * (x - x₀) ^ (n + 1) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f [[x₀, x]] y =
    iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)

Tactic:
simp [field, xy_ne y hy, Nat.factorial]

Premises used: Nat.factorial
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f [[x₀, x]]
⊢ min x₀ x < max x₀ x

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f [[x₀, x]]
⊢ UniqueDiffOn ℝ [[x₀, x]]

Tactic:
have hu : UniqueDiffOn ℝ (uIcc x₀ x) := uniqueDiffOn_Icc (by grind)
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
⊢ DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) [[x₀, x]]

Tactic:
hf.differentiableOn_iteratedDerivWithin ?_ hu

Premises used: ContDiffOn.differentiableOn_iteratedDerivWithin
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
refine : (↑n : WithTop ℕ∞) < HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1
⊢ DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) [[x₀, x]]

Tactic:
refine hf.differentiableOn_iteratedDerivWithin ?_ hu

Premises used: ContDiffOn.differentiableOn_iteratedDerivWithin
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
norm_cast : n < n + 1
⊢ (↑n : WithTop ℕ∞) < HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
⊢ n < n + 1

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
⊢ DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) [[x₀, x]]

Tactic:
have hd : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIcc x₀ x) := by
    refine hf.differentiableOn_iteratedDerivWithin ?_ hu
    norm_cast
    simp
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
hd : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) [[x₀, x]]
obtain :
  ∀ (x' : ℝ) (h1 : x' ∈ uIoo x₀ x)
    (h2 :
      f x - taylorWithinEval f n [[x₀, x]] x₀ x =
        iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)),
    ∃ x' ∈ uIoo x₀ x,
      f x - taylorWithinEval f n [[x₀, x]] x₀ x = iteratedDeriv (n + 1) f x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x = iteratedDeriv (n + 1) f x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)

Tactic:
obtain ⟨x', h1, h2⟩ := taylor_mean_remainder_lagrange hx hf.of_succ (hd.mono Ioo_subset_Icc_self)

Premises used: Set.Ioo_subset_Icc_self, ContDiffOn.of_succ, DifferentiableOn.mono, taylor_mean_remainder_lagrange
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
hd : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) [[x₀, x]]
x' : ℝ
h1 : x' ∈ uIoo x₀ x
h2 :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
right : f x - taylorWithinEval f n [[x₀, x]] x₀ x = iteratedDeriv (n + 1) f x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x = iteratedDeriv (n + 1) f x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)

Tactic:
use x', h1
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
hd : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) [[x₀, x]]
x' : ℝ
h1 : x' ∈ uIoo x₀ x
h2 :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
rw : ContDiffAt ℝ (↑(n + 1) : WithTop ℕ∞) f x'
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x = iteratedDeriv (n + 1) f x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)

Tactic:
rw [h2, iteratedDeriv_eq_iteratedFDeriv, iteratedDerivWithin_eq_iteratedFDerivWithin,
    iteratedFDerivWithin_eq_iteratedFDeriv hu _ ⟨le_of_lt h1.1, le_of_lt h1.2⟩]

Premises used: iteratedFDerivWithin_eq_iteratedFDeriv, iteratedDerivWithin_eq_iteratedFDerivWithin, le_of_lt, And.right, And.left, And.intro, iteratedDeriv_eq_iteratedFDeriv
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
hd : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) [[x₀, x]]
x' : ℝ
h1 : x' ∈ uIoo x₀ x
h2 :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
⊢ ContDiffAt ℝ (↑(n + 1) : WithTop ℕ∞) f x'

Tactic:
hf.contDiffAt (Icc_mem_nhds_iff.2 h1)

Premises used: Iff.mpr, WithTop.map₂, WithTop.some, ContDiffOn.contDiffAt, Icc_mem_nhds_iff, Option.map₂
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
hd : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) [[x₀, x]]
x' : ℝ
h1 : x' ∈ uIoo x₀ x
h2 :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
⊢ ContDiffAt ℝ (↑(n + 1) : WithTop ℕ∞) f x'

Tactic:
exact hf.contDiffAt (Icc_mem_nhds_iff.2 h1)

Premises used: Iff.mpr, ContDiffOn.contDiffAt, Icc_mem_nhds_iff
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
⊢ ContinuousOn id [[x₀, x]]

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
⊢ ContinuousOn id [[x₀, x]]

Tactic:
have gcont : ContinuousOn id (uIcc x₀ x) := by fun_prop
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn id [[x₀, x]]
⊢ ∀ x_1 ∈ uIoo x₀ x, HasDerivAt id ((fun (x : ℝ) ↦ (1 : ℝ)) x_1) x_1

Tactic:
have gdiff : ∀ x_1 : ℝ, x_1 ∈ uIoo x₀ x → HasDerivAt id ((fun _ : ℝ => (1 : ℝ)) x_1) x_1 :=
    fun _ _ => hasDerivAt_id _
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn id [[x₀, x]]
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt id ((fun (x : ℝ) ↦ (1 : ℝ)) x_1) x_1
x_1 : ℝ
h : x_1 ∈ uIoo x₀ x
⊢ Ne (α := ℝ) 1 0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn id [[x₀, x]]
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt id ((fun (x : ℝ) ↦ (1 : ℝ)) x_1) x_1
rcases :
  ∀ (y : ℝ) (hy : y ∈ uIoo x₀ x)
    (h :
      f x - taylorWithinEval f n [[x₀, x]] x₀ x =
        ((x - y) ^ n / (↑n ! : ℝ) * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f [[x₀, x]] y),
    ∃ x' ∈ uIoo x₀ x,
      f x - taylorWithinEval f n [[x₀, x]] x₀ x =
        iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x') ^ n / (↑n ! : ℝ) * (x - x₀)
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x') ^ n / (↑n ! : ℝ) * (x - x₀)

Tactic:
rcases taylor_mean_remainder hx hf hf' gcont gdiff fun _ _ => by simp with ⟨y, hy, h⟩

Premises used: taylor_mean_remainder
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn id [[x₀, x]]
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt id ((fun (x : ℝ) ↦ (1 : ℝ)) x_1) x_1
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ((x - y) ^ n / (↑n ! : ℝ) * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f [[x₀, x]] y
right :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - y) ^ n / (↑n ! : ℝ) * (x - x₀)
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x') ^ n / (↑n ! : ℝ) * (x - x₀)

Tactic:
use y, hy
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn id [[x₀, x]]
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt id ((fun (x : ℝ) ↦ (1 : ℝ)) x_1) x_1
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ((x - y) ^ n / (↑n ! : ℝ) * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f [[x₀, x]] y
right :
  ((x - y) ^ n / (↑n ! : ℝ) * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f [[x₀, x]] y =
    iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - y) ^ n / (↑n ! : ℝ) * (x - x₀)
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - y) ^ n / (↑n ! : ℝ) * (x - x₀)

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn id [[x₀, x]]
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt id ((fun (x : ℝ) ↦ (1 : ℝ)) x_1) x_1
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ((x - y) ^ n / (↑n ! : ℝ) * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f [[x₀, x]] y
⊢ ((x - y) ^ n / (↑n ! : ℝ) * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f [[x₀, x]] y =
    iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - y) ^ n / (↑n ! : ℝ) * (x - x₀)

Tactic:
simp [field]
-- 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
inl :
  ∀ (hab : a ≤ a) (hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a a)) (hx : x ∈ Icc a a)
    (hC : ∀ y ∈ Icc a a, ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C),
    ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ C * (x - a) ^ (n + 1) / (↑n ! : ℝ)
inr : ∀ (h : a < b), ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / (↑n ! : ℝ)
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / (↑n ! : ℝ)

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 C x : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a a)
hx : x ∈ Icc a a
hC : ∀ y ∈ Icc a a, ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C
⊢ x = a

Tactic:
rw [Icc_self, mem_singleton_iff] at hx

Premises used: Set.Icc_self, Set.mem_singleton_iff
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a C x : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a a)
hx : x ∈ Icc a a
hC : ∀ y ∈ Icc a a, ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C
hx₁ : x = a
⊢ ∀ y ∈ Icc a a, ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C

Tactic:
rw [Icc_self, mem_singleton_iff] at hx

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

Tactic:
simp [hx]
-- 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
⊢ DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)

Tactic:
have hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b) :=
    hf.differentiableOn_iteratedDerivWithin (mod_cast n.lt_succ_self)
      (uniqueDiffOn_Icc h)
-- 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)
y : ℝ
hay : a ≤ y
hyx : y < x
rw : |(↑n ! : ℝ)⁻¹ * (x - y) ^ n| * ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
⊢ ‖((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C

Tactic:
rw [norm_smul, Real.norm_eq_abs]

Premises used: norm_smul, Real.norm_eq_abs
-- 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)
y : ℝ
hay : a ≤ y
hyx : y < x
h₁ : |(↑n ! : ℝ)⁻¹ * (x - y) ^ n| ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n
h₂ : ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
⊢ |(↑n ! : ℝ)⁻¹ * (x - y) ^ n| * ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C

Tactic:
gcongr
-- 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)
y : ℝ
hay : a ≤ y
hyx : y < x
h₁ : (↑n ! : ℝ)⁻¹ * |x - y| ^ n ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n
⊢ |(↑n ! : ℝ)⁻¹ * (x - y) ^ n| ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n

Tactic:
rw [abs_mul, abs_pow, abs_inv, Nat.abs_cast]

Premises used: Nat.abs_cast, abs_inv, abs_mul, abs_pow
-- 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)
y : ℝ
hay : a ≤ y
hyx : y < x
h₁ : LE.le (α := ℝ) 0 (↑n ! : ℝ)⁻¹
h₂ : 0 ≤ |x - y|
h₃ : 0 ≤ x - y
⊢ (↑n ! : ℝ)⁻¹ * |x - y| ^ n ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n

Tactic:
gcongr
-- 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)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C

Tactic:
hC y ⟨hay, hyx.le.trans hx.2⟩

Premises used: LT.lt.le, And.right, And.intro, LE.le.trans
-- 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)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C

Tactic:
exact hC y ⟨hay, hyx.le.trans hx.2⟩

Premises used: LT.lt.le, And.right, And.intro, LE.le.trans
-- 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)
⊢ ∀ y ∈ Ico a x,
    ‖((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C

Tactic:
have h' : ∀ y ∈ Ico a x,
      ‖((n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤
        (n ! : ℝ)⁻¹ * |x - a| ^ n * C := by
    rintro y ⟨hay, hyx⟩
    rw [norm_smul, Real.norm_eq_abs]
    gcongr
    · rw [abs_mul, abs_pow, abs_inv, Nat.abs_cast]
      gcongr
    -- Estimate the iterated derivative by `C`
    · exact hC y ⟨hay, hyx.le.trans hx.2⟩
-- 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
⊢ Icc a x ⊆ Icc a b

Tactic:
have I : Icc a x ⊆ Icc a b := Icc_subset_Icc_right hx.2