awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ (PolynomialModule.eval x : (a : PolynomialModule ℝ E) → E) (taylorWithin f 0 s x₀) = f x₀
have dsimp : (PolynomialModule.eval x : (a : PolynomialModule ℝ E) → E)
    (∑ k ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
      (PolynomialModule.comp
            (HSub.hSub (α := Polynomial ℝ) (β := Polynomial ℝ) Polynomial.X
              ((Polynomial.C : (a : ℝ) → Polynomial ℝ) x₀ : Polynomial ℝ)) :
          (a : PolynomialModule ℝ E) → PolynomialModule ℝ E)
        ((PolynomialModule.single ℝ k : (a : E) → PolynomialModule ℝ E) (taylorCoeffWithin f k s x₀))) =
  f x₀
Tactic: dsimp only [taylorWithin]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ (PolynomialModule.eval x : (a : PolynomialModule ℝ E) → E)
      (∑ k ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
        (PolynomialModule.comp
              (HSub.hSub (α := Polynomial ℝ) (β := Polynomial ℝ) Polynomial.X
                ((Polynomial.C : (a : ℝ) → Polynomial ℝ) x₀ : Polynomial ℝ)) :
            (a : PolynomialModule ℝ E) → PolynomialModule ℝ E)
          ((PolynomialModule.single ℝ k : (a : E) → PolynomialModule ℝ E) (taylorCoeffWithin f k s x₀))) =
    f x₀
have dsimp : (PolynomialModule.eval x : (a : PolynomialModule ℝ E) → E)
    (∑ k ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
      (PolynomialModule.comp
            (HSub.hSub (α := Polynomial ℝ) (β := Polynomial ℝ) Polynomial.X
              ((Polynomial.C : (a : ℝ) → Polynomial ℝ) x₀ : Polynomial ℝ)) :
          (a : PolynomialModule ℝ E) → PolynomialModule ℝ E)
        ((PolynomialModule.single ℝ k : (a : E) → PolynomialModule ℝ E)
          (HSMul.hSMul (α := ℝ) (↑k ! : ℝ)⁻¹ (iteratedDerivWithin k f s x₀)))) =
  f x₀
Tactic: dsimp only [taylorCoeffWithin]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ : ℝ
⊢ taylorWithinEval f n s x₀ x₀ = f x₀
have zero : taylorWithinEval f 0 s x₀ x₀ = f x₀
Tactic: induction n with
  | zero => exact taylor_within_zero_eval _ _ _ _
  | succ k hk => simp [hk]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ : ℝ
zero : taylorWithinEval f 0 s x₀ x₀ = f x₀
⊢ taylorWithinEval f n s x₀ x₀ = f x₀
have succ : ∀ (k : ℕ) (hk : taylorWithinEval f k s x₀ x₀ = f x₀), taylorWithinEval f (k + 1) s x₀ x₀ = f x₀
Tactic: induction n with
  | zero => exact taylor_within_zero_eval _ _ _ _
  | succ k hk => simp [hk]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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₀
⊢ taylorWithinEval f (k + 1) s x₀ x =
    ∑ k ∈ Finset.range (k + 1 + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
have 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₀
Tactic: rw [taylorWithinEval_succ, Finset.sum_range_succ, hk]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
⊢ taylorWithinEval f n s x₀ x = ∑ k ∈ Finset.range (n + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
have zero : taylorWithinEval f 0 s x₀ x =
  ∑ k ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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₀
⊢ taylorWithinEval f n s x₀ x = ∑ k ∈ Finset.range (n + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
have 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₀
Tactic: induction n with
  | zero => simp
  | succ k hk =>
    rw [taylorWithinEval_succ, Finset.sum_range_succ, hk]
    simp [Nat.factorial]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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 : ℝ) ↦ taylorWithinEval f n s t x) s
have 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
Tactic: simp_rw [taylor_within_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
have 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
Tactic: refine continuousOn_finsetSum (Finset.range (n + 1)) fun i hi => ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
have refine : ContinuousOn (iteratedDerivWithin i f s) s
Tactic: refine (continuousOn_const.mul ((continuousOn_const.sub continuousOn_id).pow _)).smul ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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 (iteratedDerivWithin i f s) s
have 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
Tactic: rw [contDiffOn_nat_iff_continuousOn_differentiableOn_deriv hs] at hf
Cleared hypotheses: hf, i, hi
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
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)
⊢ ContinuousOn (iteratedDerivWithin i f s) s
have hi₁ : i < n + 1
Tactic: simp only [Finset.mem_range] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
have refine : i ≤ n
Tactic: refine hf.1 i ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
t x : ℝ
n : ℕ
⊢ HasDerivAt (fun (y : ℝ) ↦ (x - y) ^ (n + 1)) (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - t) ^ n) t
have simp_rw : HasDerivAt (fun (y : ℝ) ↦ (-y + x) ^ (n + 1)) (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (-t + x) ^ n) t
Tactic: simp_rw [sub_eq_neg_add]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
t x : ℝ
n : ℕ
⊢ HasDerivAt (fun (y : ℝ) ↦ (-y + x) ^ (n + 1)) (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (-t + x) ^ n) t
have rw : HasDerivAt (fun (y : ℝ) ↦ (-y + x) ^ (n + 1)) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (-t + x) ^ n * -1) t
Tactic: rw [← neg_one_mul, mul_comm (-1 : ℝ), mul_assoc, mul_comm (-1 : ℝ), ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
t x : ℝ
n : ℕ
⊢ HasDerivAt (fun (y : ℝ) ↦ (-y + x) ^ (n + 1)) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (-t + x) ^ n * -1) t
have h : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 = (↑(n + 1) : ℝ)
Tactic: convert! ((hasDerivAt_id t).neg.add_const x).pow (n + 1)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
have h : iteratedDerivWithin (k + 2) f s y = derivWithin (iteratedDerivWithin (k + 1) f s) t y
Tactic: convert! (hf.mono_of_mem_nhdsWithin hs).hasDerivWithinAt using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
⊢ iteratedDerivWithin (k + 2) f s y = derivWithin (iteratedDerivWithin (k + 1) f s) t y
have h : derivWithin (iteratedDerivWithin (k + 1) f s) s y = derivWithin (iteratedDerivWithin (k + 1) f s) t y
Tactic: rw [iteratedDerivWithin_succ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
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
    (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
have hf₁ : 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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
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
have this : -((↑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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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))
    (-((↑k ! : ℝ)⁻¹ * (x - y) ^ k)) t y
have 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
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
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 (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
have this : 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 _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
    (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
have 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
Tactic: convert! this.smul hf using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
⊢ ((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
have 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
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
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
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ taylorWithinEval f n s t x)
    (((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f s y) s' y
have hs'_unique : UniqueDiffWithinAt ℝ s' y
Tactic: have hs'_unique : UniqueDiffWithinAt ℝ s' y :=
    UniqueDiffWithinAt.mono_nhds (hs_unique _ (h hy)) (nhdsWithin_le_iff.mpr hs')
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
⊢ 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
have zero : HasDerivWithinAt (fun (t : ℝ) ↦ f t) (iteratedDerivWithin 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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
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
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ f t) (iteratedDerivWithin 1 f s y) s' y
have hf'₁ : DifferentiableWithinAt ℝ f s y
Tactic: simp only [iteratedDerivWithin_zero] at hf'
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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) (iteratedDerivWithin 1 f s y) s' y
have zero : HasDerivWithinAt (fun (t : ℝ) ↦ f t) (derivWithin f s y) s' y
Tactic: rw [iteratedDerivWithin_one]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
k : ℕ
hk :
  ∀ (hf : ContDiffOn ℝ (↑k : WithTop ℕ∞) f s) (hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin k f s) s y),
    HasDerivWithinAt (fun (t : ℝ) ↦ taylorWithinEval f k s t x)
      (((↑k ! : ℝ)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) s' y
hf : ContDiffOn ℝ (↑(k + 1) : WithTop ℕ∞) f s
hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ taylorWithinEval f (k + 1) s t x)
    (((↑(k + 1)! : ℝ)⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 1 + 1) f s y) s' y
have succ : HasDerivWithinAt
  (fun (t : ℝ) ↦
    taylorWithinEval f k s t x +
      ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - t) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s t)
  (((↑(k + 0).succ ! : ℝ)⁻¹ * (x - y) ^ (k + 0).succ) • iteratedDerivWithin ((k + 0).succ + 0).succ f s y) s' y
Tactic: simp_rw [Nat.add_succ, taylorWithinEval_succ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
k : ℕ
hk :
  ∀ (hf : ContDiffOn ℝ (↑k : WithTop ℕ∞) f s) (hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin k f s) s y),
    HasDerivWithinAt (fun (t : ℝ) ↦ taylorWithinEval f k s t x)
      (((↑k ! : ℝ)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) s' y
hf : ContDiffOn ℝ (↑(k + 1) : WithTop ℕ∞) f s
hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ HasDerivWithinAt
    (fun (t : ℝ) ↦
      taylorWithinEval f k s t x +
        ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - t) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s t)
    (((↑(k + 0).succ ! : ℝ)⁻¹ * (x - y) ^ (k + 0).succ) • iteratedDerivWithin ((k + 0).succ + 0).succ f s y) s' y
have succ : HasDerivWithinAt
  (fun (t : ℝ) ↦
    taylorWithinEval f k s t x +
      ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - t) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s t)
  (((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - y) ^ k.succ) • iteratedDerivWithin k.succ.succ f s y) s' y
Tactic: simp only [add_zero, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
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
k : ℕ
hk :
  ∀ (hf : ContDiffOn ℝ (↑k : WithTop ℕ∞) f s) (hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin k f s) s y),
    HasDerivWithinAt (fun (t : ℝ) ↦ taylorWithinEval f k s t x)
      (((↑k ! : ℝ)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) s' y
hf : ContDiffOn ℝ (↑(k + 1) : WithTop ℕ∞) f s
hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ HasDerivWithinAt
    (fun (t : ℝ) ↦
      taylorWithinEval f k s t x +
        ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - t) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s t)
    (((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - y) ^ k.succ) • iteratedDerivWithin k.succ.succ f s y) s' y
have coe_lt_succ : LT.lt (α := WithTop ℕ) (↑k : WithTop ℕ) (↑k.succ : WithTop ℕ)
Tactic: have coe_lt_succ : (k : WithTop ℕ) < k.succ := Nat.cast_lt.2 k.lt_succ_self
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
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
k : ℕ
hk :
  ∀ (hf : ContDiffOn ℝ (↑k : WithTop ℕ∞) f s) (hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin k f s) s y),
    HasDerivWithinAt (fun (t : ℝ) ↦ taylorWithinEval f k s t x)
      (((↑k ! : ℝ)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) s' y
hf : ContDiffOn ℝ (↑(k + 1) : WithTop ℕ∞) f s
hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
coe_lt_succ : LT.lt (α := WithTop ℕ) (↑k : WithTop ℕ) (↑k.succ : WithTop ℕ)
⊢ HasDerivWithinAt
    (fun (t : ℝ) ↦
      taylorWithinEval f k s t x +
        ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - t) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s t)
    (((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - y) ^ k.succ) • iteratedDerivWithin k.succ.succ f s y) s' y
have hdiff : DifferentiableOn ℝ (iteratedDerivWithin k f s) s'
Tactic: have hdiff : DifferentiableOn ℝ (iteratedDerivWithin k f s) s' :=
      (hf.differentiableOn_iteratedDerivWithin (mod_cast coe_lt_succ) hs_unique).mono h