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
s : Set ℝ
x₀ x : ℝ
k : ℕ
hk :
  taylorWithinEval f k s x₀ x = ∑ k ∈ Finset.range (k + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
succ :
  ∑ k ∈ Finset.range (k + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀ +
      ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - x₀) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s x₀ =
    ∑ x_1 ∈ Finset.range (k + 1), ((↑x_1 ! : ℝ)⁻¹ * (x - x₀) ^ x_1) • iteratedDerivWithin x_1 f s x₀ +
      ((↑(k + 1)! : ℝ)⁻¹ * (x - x₀) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s x₀
⊢ taylorWithinEval f (k + 1) s x₀ x =
    ∑ k ∈ Finset.range (k + 1 + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀

Tactic:
rw [taylorWithinEval_succ, Finset.sum_range_succ, hk]

Premises used: taylorWithinEval_succ, Finset.sum_range_succ
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
k : ℕ
hk :
  taylorWithinEval f k s x₀ x = ∑ k ∈ Finset.range (k + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
⊢ ∑ k ∈ Finset.range (k + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀ +
      ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - x₀) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s x₀ =
    ∑ x_1 ∈ Finset.range (k + 1), ((↑x_1 ! : ℝ)⁻¹ * (x - x₀) ^ x_1) • iteratedDerivWithin x_1 f s x₀ +
      ((↑(k + 1)! : ℝ)⁻¹ * (x - x₀) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s x₀

Tactic:
simp [Nat.factorial]

Premises used: Nat.factorial
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
zero :
  taylorWithinEval f 0 s x₀ x =
    ∑ k ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
succ :
  ∀ (k : ℕ)
    (hk :
      taylorWithinEval f k s x₀ x =
        ∑ k ∈ Finset.range (k + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀),
    taylorWithinEval f (k + 1) s x₀ x =
      ∑ k ∈ Finset.range (k + 1 + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
⊢ taylorWithinEval f n s x₀ x = ∑ k ∈ Finset.range (n + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀

Tactic:
induction n with
  | zero => simp
  | succ k hk =>
    rw [taylorWithinEval_succ, Finset.sum_range_succ, hk]
    simp [Nat.factorial]

Premises used: taylorWithinEval_succ, Nat.factorial, Finset.sum_range_succ
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
simp_rw :
  ContinuousOn.{0, u_2} (Y := E)
    (fun (t : ℝ) ↦ ∑ k ∈ Finset.range (n + 1), ((↑k ! : ℝ)⁻¹ * (x - t) ^ k) • iteratedDerivWithin k f s t) s
⊢ ContinuousOn.{0, u_2} (Y := E) (fun (t : ℝ) ↦ taylorWithinEval f n s t x) s

Tactic:
simp_rw [taylor_within_apply]

Premises used: taylor_within_apply
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
⊢ ContinuousOn.{0, u_2} (Y := E)
    (fun (t : ℝ) ↦ ∑ k ∈ Finset.range (n + 1), ((↑k ! : ℝ)⁻¹ * (x - t) ^ k) • iteratedDerivWithin k f s t) s

Tactic:
continuousOn_finsetSum (Finset.range (n + 1)) fun i hi => ?_

Premises used: continuousOn_finsetSum, Finset.range, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
refine :
  ∀ (i : ℕ) (hi : i ∈ Finset.range (n + 1)),
    ContinuousOn.{0, u_2} (Y := E) (fun (t : ℝ) ↦ ((↑i ! : ℝ)⁻¹ * (x - t) ^ i) • iteratedDerivWithin i f s t) s
⊢ ContinuousOn.{0, u_2} (Y := E)
    (fun (t : ℝ) ↦ ∑ k ∈ Finset.range (n + 1), ((↑k ! : ℝ)⁻¹ * (x - t) ^ k) • iteratedDerivWithin k f s t) s

Tactic:
refine continuousOn_finsetSum (Finset.range (n + 1)) fun i hi => ?_

Premises used: continuousOn_finsetSum, Finset.range, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ ContinuousOn.{0, u_2} (Y := E) (fun (t : ℝ) ↦ ((↑i ! : ℝ)⁻¹ * (x - t) ^ i) • iteratedDerivWithin i f s t) s

Tactic:
(continuousOn_const.mul ((continuousOn_const.sub continuousOn_id).pow _)).smul ?_

Premises used: ContinuousOn.sub, continuousOn_const, ContinuousOn.smul, continuousOn_id, ContinuousOn.mul, ContinuousOn.pow
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
i : ℕ
hi : i ∈ Finset.range (n + 1)
refine : ContinuousOn (iteratedDerivWithin i f s) s
⊢ ContinuousOn.{0, u_2} (Y := E) (fun (t : ℝ) ↦ ((↑i ! : ℝ)⁻¹ * (x - t) ^ i) • iteratedDerivWithin i f s t) s

Tactic:
refine (continuousOn_const.mul ((continuousOn_const.sub continuousOn_id).pow _)).smul ?_

Premises used: ContinuousOn.sub, continuousOn_const, ContinuousOn.smul, continuousOn_id, ContinuousOn.mul, ContinuousOn.pow
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
i : ℕ
hi : i ∈ Finset.range (n + 1)
rw :
  ∀
    (hf :
      (∀ m ≤ n, ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ m < n, DifferentiableOn ℝ (iteratedDerivWithin m f s) s)
    (i : ℕ) (hi : i ∈ Finset.range (n + 1)), ContinuousOn (iteratedDerivWithin i f s) s
⊢ ContinuousOn (iteratedDerivWithin i f s) s

Tactic:
rw [contDiffOn_nat_iff_continuousOn_differentiableOn_deriv hs] at hf

Premises used: contDiffOn_nat_iff_continuousOn_differentiableOn_deriv
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf : (∀ m ≤ n, ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ m < n, DifferentiableOn ℝ (iteratedDerivWithin m f s) s
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ i < n + 1

Tactic:
simp only [Finset.mem_range] at hi

Premises used: Finset.mem_range
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf : (∀ m ≤ n, ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ m < n, DifferentiableOn ℝ (iteratedDerivWithin m f s) s
i : ℕ
hi : i < n + 1
⊢ ContinuousOn (iteratedDerivWithin i f s) s

Tactic:
hf.1 i ?_

Premises used: And.left
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf : (∀ m ≤ n, ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ m < n, DifferentiableOn ℝ (iteratedDerivWithin m f s) s
i : ℕ
hi : i < n + 1
refine : i ≤ n
⊢ ContinuousOn (iteratedDerivWithin i f s) s

Tactic:
refine hf.1 i ?_

Premises used: And.left
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf : (∀ m ≤ n, ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ m < n, DifferentiableOn ℝ (iteratedDerivWithin m f s) s
i : ℕ
hi : i < n + 1
⊢ i ≤ n

Tactic:
simp only [Nat.lt_succ_iff.mp hi]

Premises used: Nat.lt_succ_iff, Iff.mp
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
t x : ℝ
n : ℕ
simp_rw : HasDerivAt (fun (y : ℝ) ↦ (-y + x) ^ (n + 1)) (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (-t + x) ^ n) t
⊢ HasDerivAt (fun (y : ℝ) ↦ (x - y) ^ (n + 1)) (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - t) ^ n) t

Tactic:
simp_rw [sub_eq_neg_add]

Premises used: sub_eq_neg_add
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
t x : ℝ
n : ℕ
rw : HasDerivAt (fun (y : ℝ) ↦ (-y + x) ^ (n + 1)) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (-t + x) ^ n * -1) t
⊢ HasDerivAt (fun (y : ℝ) ↦ (-y + x) ^ (n + 1)) (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (-t + x) ^ n) t

Tactic:
rw [← neg_one_mul, mul_comm (-1 : ℝ), mul_assoc, mul_comm (-1 : ℝ), ← mul_assoc]

Premises used: mul_assoc, neg_one_mul, mul_comm, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
t x : ℝ
n : ℕ
⊢ HasDerivAt (HPow.hPow (α := ℝ → ℝ) (fun (x_1 : ℝ) ↦ HAdd.hAdd (α := ℝ) ((-id) x_1 : ℝ) x) (n + 1))
    ((↑(n + 1) : ℝ) * HAdd.hAdd (α := ℝ) ((-id) t : ℝ) x ^ (n + 1 - 1) * -1) t

Tactic:
((hasDerivAt_id t).neg.add_const x).pow (n + 1)

Premises used: HasDerivAt.pow, HasDerivAt.neg, HasDerivAt.add_const, hasDerivAt_id, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
t x : ℝ
n : ℕ
h : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 = (↑(n + 1) : ℝ)
⊢ HasDerivAt (fun (y : ℝ) ↦ (-y + x) ^ (n + 1)) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (-t + x) ^ n * -1) t

Tactic:
convert! ((hasDerivAt_id t).neg.add_const x).pow (n + 1)

Premises used: HasDerivAt.pow, HasDerivAt.neg, HasDerivAt.add_const, hasDerivAt_id, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
t x : ℝ
n : ℕ
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 = (↑(n + 1) : ℝ)

Tactic:
simp only [Nat.cast_add, Nat.cast_one]

Premises used: Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (derivWithin (iteratedDerivWithin (k + 1) f s) t y) t y

Tactic:
(hf.mono_of_mem_nhdsWithin hs).hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, DifferentiableWithinAt.mono_of_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
h : iteratedDerivWithin (k + 2) f s y = derivWithin (iteratedDerivWithin (k + 1) f s) t y
⊢ HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y

Tactic:
convert! (hf.mono_of_mem_nhdsWithin hs).hasDerivWithinAt using 1

Premises used: DifferentiableWithinAt.hasDerivWithinAt, DifferentiableWithinAt.mono_of_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
h : derivWithin (iteratedDerivWithin (k + 1) f s) s y = derivWithin (iteratedDerivWithin (k + 1) f s) t y
⊢ iteratedDerivWithin (k + 2) f s y = derivWithin (iteratedDerivWithin (k + 1) f s) t y

Tactic:
rw [iteratedDerivWithin_succ]

Premises used: iteratedDerivWithin_succ
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ derivWithin (iteratedDerivWithin (k + 1) f s) s y = derivWithin (iteratedDerivWithin (k + 1) f s) t y

Tactic:
(derivWithin_of_mem_nhdsWithin hs ht hf).symm

Premises used: derivWithin_of_mem_nhdsWithin, Eq.symm
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ derivWithin (iteratedDerivWithin (k + 1) f s) s y = derivWithin (iteratedDerivWithin (k + 1) f s) t y

Tactic:
exact (derivWithin_of_mem_nhdsWithin hs ht hf).symm

Premises used: derivWithin_of_mem_nhdsWithin, Eq.symm
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y

Tactic:
replace hf :
    HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y := by
    convert! (hf.mono_of_mem_nhdsWithin hs).hasDerivWithinAt using 1
    rw [iteratedDerivWithin_succ]
    exact (derivWithin_of_mem_nhdsWithin hs ht hf).symm
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
⊢ -((↑k ! : ℝ)⁻¹ * (x - y) ^ k) =
    (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (x - y) ^ k)

Tactic:
field
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
⊢ -((↑k ! : ℝ)⁻¹ * (x - y) ^ k) =
    (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (x - y) ^ k)

Tactic:
have : -((k ! : ℝ)⁻¹ * (x - y) ^ k) = ((k + 1 : ℝ) * k !)⁻¹ * (-(k + 1) * (x - y) ^ k) := by
      field
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
this :
  -((↑k ! : ℝ)⁻¹ * (x - y) ^ k) =
    (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (x - y) ^ k)
rw :
  HasDerivWithinAt (fun (t : ℝ) ↦ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - t) ^ (k + 1))
    ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (x - y) ^ k)) t y
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - t) ^ (k + 1))
    (-((↑k ! : ℝ)⁻¹ * (x - y) ^ k)) t y

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
this :
  -((↑k ! : ℝ)⁻¹ * (x - y) ^ k) =
    (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (x - y) ^ k)
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - t) ^ (k + 1))
    ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (x - y) ^ k)) t y

Tactic:
(monomial_has_deriv_aux y x _).hasDerivWithinAt.const_mul _

Premises used: HasDerivAt.hasDerivWithinAt, monomial_has_deriv_aux, HasDerivWithinAt.const_mul
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
this :
  -((↑k ! : ℝ)⁻¹ * (x - y) ^ k) =
    (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (x - y) ^ k)
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - t) ^ (k + 1))
    ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (x - y) ^ k)) t y

Tactic:
exact (monomial_has_deriv_aux y x _).hasDerivWithinAt.const_mul _

Premises used: HasDerivAt.hasDerivWithinAt, monomial_has_deriv_aux, HasDerivWithinAt.const_mul
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - t) ^ (k + 1))
    (-((↑k ! : ℝ)⁻¹ * (x - y) ^ k)) t y

Tactic:
have : HasDerivWithinAt (fun t => ((k + 1 : ℝ) * k !)⁻¹ * (x - t) ^ (k + 1))
      (-((k ! : ℝ)⁻¹ * (x - y) ^ k)) t y := by
    -- Commuting the factors:
    have : -((k ! : ℝ)⁻¹ * (x - y) ^ k) = ((k + 1 : ℝ) * k !)⁻¹ * (-(k + 1) * (x - y) ^ k) := by
      field
    rw [this]
    exact (monomial_has_deriv_aux y x _).hasDerivWithinAt.const_mul _
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
this :
  HasDerivWithinAt (fun (t : ℝ) ↦ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - t) ^ (k + 1))
    (-((↑k ! : ℝ)⁻¹ * (x - y) ^ k)) t y
⊢ HasDerivWithinAt
    (HSMul.hSMul (α := ℝ → ℝ) (fun (t : ℝ) ↦ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - t) ^ (k + 1))
      (iteratedDerivWithin (k + 1) f s))
    (((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y +
      -((↑k ! : ℝ)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y)
    t y

Tactic:
this.smul hf

Premises used: HasDerivWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
this :
  HasDerivWithinAt (fun (t : ℝ) ↦ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - t) ^ (k + 1))
    (-((↑k ! : ℝ)⁻¹ * (x - y) ^ k)) t y
h :
  ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y -
      ((↑k ! : ℝ)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y =
    ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y +
      -((↑k ! : ℝ)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y
⊢ HasDerivWithinAt
    (fun (z : ℝ) ↦
      ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - z) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s z)
    (((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y -
      ((↑k ! : ℝ)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y)
    t y

Tactic:
convert! this.smul hf using 1

Premises used: HasDerivWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
this :
  HasDerivWithinAt (fun (t : ℝ) ↦ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - t) ^ (k + 1))
    (-((↑k ! : ℝ)⁻¹ * (x - y) ^ k)) t y
h :
  ((x - y) ^ (k + 1) / (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))) • iteratedDerivWithin (k + 2) f s y -
      ((x - y) ^ k / (↑k ! : ℝ)) • iteratedDerivWithin (k + 1) f s y =
    ((x - y) ^ (k + 1) / (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))) • iteratedDerivWithin (k + 2) f s y +
      -((x - y) ^ k / (↑k ! : ℝ)) • iteratedDerivWithin (k + 1) f s y
⊢ ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y -
      ((↑k ! : ℝ)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y =
    ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y +
      -((↑k ! : ℝ)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y

Tactic:
field_simp
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
this :
  HasDerivWithinAt (fun (t : ℝ) ↦ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - t) ^ (k + 1))
    (-((↑k ! : ℝ)⁻¹ * (x - y) ^ k)) t y
⊢ ((x - y) ^ (k + 1) / (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))) • iteratedDerivWithin (k + 2) f s y -
      ((x - y) ^ k / (↑k ! : ℝ)) • iteratedDerivWithin (k + 1) f s y =
    ((x - y) ^ (k + 1) / (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))) • iteratedDerivWithin (k + 2) f s y +
      -((x - y) ^ k / (↑k ! : ℝ)) • iteratedDerivWithin (k + 1) f s y

Tactic:
module
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
n : ℕ
s s' : Set ℝ
hs_unique : UniqueDiffOn ℝ s
hs' : s' ∈ 𝓝[s] y
hy : y ∈ s'
h : s' ⊆ s
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin n f s) s y
⊢ UniqueDiffWithinAt ℝ s' y

Tactic:
have hs'_unique : UniqueDiffWithinAt ℝ s' y :=
    UniqueDiffWithinAt.mono_nhds (hs_unique _ (h hy)) (nhdsWithin_le_iff.mpr hs')
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
s s' : Set ℝ
hs_unique : UniqueDiffOn ℝ s
hs' : s' ∈ 𝓝[s] y
hy : y ∈ s'
h : s' ⊆ s
hs'_unique : UniqueDiffWithinAt ℝ s' y
hf : ContDiffOn ℝ (↑0 : WithTop ℕ∞) f s
hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin 0 f s) s y
zero : HasDerivWithinAt (fun (t : ℝ) ↦ f t) (iteratedDerivWithin 1 f s y) s' y
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ taylorWithinEval f 0 s t x)
    (((↑0! : ℝ)⁻¹ * HPow.hPow (β := ℕ) (x - y) 0) • iteratedDerivWithin (HAdd.hAdd (α := ℕ) 0 1) f s y) s' y

Tactic:
simp only [taylor_within_zero_eval, Nat.factorial_zero, Nat.cast_one, inv_one, pow_zero,
      mul_one, zero_add, one_smul]

Premises used: inv_one, taylor_within_zero_eval, zero_add, pow_zero, one_smul, Nat.factorial_zero, mul_one, Nat.cast_one
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
s s' : Set ℝ
hs_unique : UniqueDiffOn ℝ s
hs' : s' ∈ 𝓝[s] y
hy : y ∈ s'
h : s' ⊆ s
hs'_unique : UniqueDiffWithinAt ℝ s' y
hf : ContDiffOn ℝ (↑0 : WithTop ℕ∞) f s
hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin 0 f s) s y
⊢ DifferentiableWithinAt ℝ f s y

Tactic:
simp only [iteratedDerivWithin_zero] at hf'

Premises used: iteratedDerivWithin_zero
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
s s' : Set ℝ
hs_unique : UniqueDiffOn ℝ s
hs' : s' ∈ 𝓝[s] y
hy : y ∈ s'
h : s' ⊆ s
hs'_unique : UniqueDiffWithinAt ℝ s' y
hf : ContDiffOn ℝ (↑0 : WithTop ℕ∞) f s
hf' : DifferentiableWithinAt ℝ f s y
zero : HasDerivWithinAt (fun (t : ℝ) ↦ f t) (derivWithin f s y) s' y
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ f t) (iteratedDerivWithin 1 f s y) s' y

Tactic:
rw [iteratedDerivWithin_one]

Premises used: iteratedDerivWithin_one
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
s s' : Set ℝ
hs_unique : UniqueDiffOn ℝ s
hs' : s' ∈ 𝓝[s] y
hy : y ∈ s'
h : s' ⊆ s
hs'_unique : UniqueDiffWithinAt ℝ s' y
hf : ContDiffOn ℝ (↑0 : WithTop ℕ∞) f s
hf' : DifferentiableWithinAt ℝ f s y
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ f t) (derivWithin f s y) s' y

Tactic:
hf'.hasDerivWithinAt.mono h

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.mono