awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : (n : ℕ) → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
case case₁ case₂ :
  ∀ (ib : ℕ),
    True →
      ∃ (ia : ℕ),
        True ∧
          ∀ x ∈ Set.Ici ia,
            Membership.mem (γ := Set E) (Metric.ball 0 ((1 / 2) ^ ib))
              (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) x) (d x))
case₃ :
  ∀ (N : ℕ),
    True →
      ∀ (n : ℕ) (hn : n ∈ Set.Ici N),
        Membership.mem (γ := Set E) (Metric.ball 0 ((1 / 2) ^ N))
          (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) n) (d n))
case₄ :
  ∀ (N : ℕ),
    True →
      ∀ (n : ℕ) (hn : N ≤ n),
        Membership.mem (γ := Set E) (Metric.ball 0 ((1 / 2) ^ N))
          (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) n) (d n))
case₅ : ∀ (N : ℕ), True → ∀ (n : ℕ) (hn : N ≤ n), ‖c‖ ^ n * ‖d n‖ < 1 / HPow.hPow (α := ℝ) 2 N
case₆ : ∀ (N : ℕ), True → ∀ (n : ℕ) (hn : N ≤ n), ‖d n‖ < 1 / HPow.hPow (α := ℝ) 2 N / ‖c‖ ^ n
case₇ : ∀ (N : ℕ), True → ∀ (n : ℕ) (hn : N ≤ n), (1 / (2 * ‖c‖)) ^ n ≤ 1 / HPow.hPow (α := ℝ) 2 N / ‖c‖ ^ n
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) n) (d n)) atTop
    (𝓝 0)
have case₈ : ∀ (N : ℕ), True → ∀ (n : ℕ) (hn : N ≤ n), (1 / (2 * ‖c‖)) ^ n ≤ 1 / HPow.hPow (α := ℝ) 2 n / ‖c‖ ^ n
Tactic: case tendsto_cd =>
        rw [atTop_basis.tendsto_iff (Metric.nhds_basis_ball_pow one_half_pos one_half_lt_one)]
        refine fun N _ ↦ ⟨N, trivial, fun n hn ↦ ?_⟩
        rw [Set.mem_Ici] at hn
        suffices ‖c‖ ^ n * ‖d n‖ < 1 / (2 ^ N) by simpa [norm_smul]
        rw [← lt_div_iff₀' (by positivity)]
        refine (hd n).trans_le ?_
        grw [hn]
        · simp [mul_pow, div_eq_inv_mul]
        · norm_num1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : (n : ℕ) → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
case case₁ case₂ :
  ∀ (ib : ℕ),
    True →
      ∃ (ia : ℕ),
        True ∧
          ∀ x ∈ Set.Ici ia,
            Membership.mem (γ := Set E) (Metric.ball 0 ((1 / 2) ^ ib))
              (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) x) (d x))
case₃ :
  ∀ (N : ℕ),
    True →
      ∀ (n : ℕ) (hn : n ∈ Set.Ici N),
        Membership.mem (γ := Set E) (Metric.ball 0 ((1 / 2) ^ N))
          (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) n) (d n))
case₄ :
  ∀ (N : ℕ),
    True →
      ∀ (n : ℕ) (hn : N ≤ n),
        Membership.mem (γ := Set E) (Metric.ball 0 ((1 / 2) ^ N))
          (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) n) (d n))
case₅ : ∀ (N : ℕ), True → ∀ (n : ℕ) (hn : N ≤ n), ‖c‖ ^ n * ‖d n‖ < 1 / HPow.hPow (α := ℝ) 2 N
case₆ : ∀ (N : ℕ), True → ∀ (n : ℕ) (hn : N ≤ n), ‖d n‖ < 1 / HPow.hPow (α := ℝ) 2 N / ‖c‖ ^ n
case₇ : ∀ (N : ℕ), True → ∀ (n : ℕ) (hn : N ≤ n), (1 / (2 * ‖c‖)) ^ n ≤ 1 / HPow.hPow (α := ℝ) 2 N / ‖c‖ ^ n
case₈ : ∀ (N : ℕ), True → ∀ (n : ℕ) (hn : N ≤ n), (1 / (2 * ‖c‖)) ^ n ≤ 1 / HPow.hPow (α := ℝ) 2 n / ‖c‖ ^ n
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) n) (d n)) atTop
    (𝓝 0)
have h₂ : ∀ (N : ℕ), True → ∀ (n : ℕ) (hn : N ≤ n), LE.le (α := ℝ) 1 2
Tactic: case tendsto_cd =>
        rw [atTop_basis.tendsto_iff (Metric.nhds_basis_ball_pow one_half_pos one_half_lt_one)]
        refine fun N _ ↦ ⟨N, trivial, fun n hn ↦ ?_⟩
        rw [Set.mem_Ici] at hn
        suffices ‖c‖ ^ n * ‖d n‖ < 1 / (2 ^ N) by simpa [norm_smul]
        rw [← lt_div_iff₀' (by positivity)]
        refine (hd n).trans_le ?_
        grw [hn]
        · simp [mul_pow, div_eq_inv_mul]
        · norm_num1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x y : E
hy₀ : y ≠ 0
⊢ y ∈ tangentConeAt 𝕜 s x →
    ∃ (c : ℕ → 𝕜) (d : ℕ → E),
      Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
        (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
have mp : (∃ (c : ℕ → 𝕜) (d : ℕ → E),
    Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)) →
  ∃ (c : ℕ → 𝕜) (d : ℕ → E),
    Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
      (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
Tactic: rw [mem_tangentConeAt_iff_exists_seq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x y : E
hy₀ : y ≠ 0
c : ℕ → 𝕜
d : ℕ → E
hd₀ : Tendsto d atTop (𝓝 0)
hds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hcd : Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
⊢ ∃ (c : ℕ → 𝕜) (d : ℕ → E),
    Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop ∧
      (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
have mp : Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop
Tactic: refine ⟨c, d, ?_, hds, hcd⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x y : E
hy₀ : y ≠ 0
c : ℕ → 𝕜
d : ℕ → E
hd₀ : Tendsto d atTop (𝓝 0)
hds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hcd : Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop
have hd₁ : Tendsto (fun (x : ℕ) ↦ ‖d x‖) atTop (𝓝 (norm.{u_2} (E := E) 0))
Tactic: replace hd₀ := hd₀.norm
Cleared hypotheses: hd₀
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x y : E
hy₀ : y ≠ 0
c : ℕ → 𝕜
d : ℕ → E
hds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hcd : Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
hd₀ : Tendsto (fun (x : ℕ) ↦ ‖d x‖) atTop (𝓝 (norm.{u_2} (E := E) 0))
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop
have hd₀' : ∀ᶠ (n : ℕ) in atTop, d n ≠ 0
Tactic: have hd₀' : ∀ᶠ n in .atTop, d n ≠ 0 :=
        hcd.eventually_ne hy₀ |>.mono fun _ ↦ right_ne_zero_of_smul
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x y : E
hy₀ : y ≠ 0
c : ℕ → 𝕜
d : ℕ → E
hds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hcd : Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
hd₀ : Tendsto (fun (x : ℕ) ↦ ‖d x‖) atTop (𝓝 (norm.{u_2} (E := E) 0))
hd₀' : ∀ᶠ (n : ℕ) in atTop, d n ≠ 0
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop
have hcd₁ : Tendsto (fun (x : ℕ) ↦ ‖c x • d x‖) atTop (𝓝 ‖y‖)
Tactic: replace hcd := hcd.norm
Cleared hypotheses: hcd
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x y : E
hy₀ : y ≠ 0
c : ℕ → 𝕜
d : ℕ → E
hds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hd₀ : Tendsto (fun (x : ℕ) ↦ ‖d x‖) atTop (𝓝 (norm.{u_2} (E := E) 0))
hd₀' : ∀ᶠ (n : ℕ) in atTop, d n ≠ 0
hcd : Tendsto (fun (x : ℕ) ↦ ‖c x • d x‖) atTop (𝓝 ‖y‖)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop
have hd₁ : Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖d x‖) atTop (𝓝 0)
Tactic: simp only [norm_smul, norm_zero, ← div_inv_eq_mul] at hd₀ hcd
Cleared hypotheses: hd₀, hcd
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x y : E
hy₀ : y ≠ 0
c : ℕ → 𝕜
d : ℕ → E
hds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hd₀ : Tendsto (fun (x : ℕ) ↦ ‖d x‖) atTop (𝓝 (norm.{u_2} (E := E) 0))
hd₀' : ∀ᶠ (n : ℕ) in atTop, d n ≠ 0
hcd : Tendsto (fun (x : ℕ) ↦ ‖c x • d x‖) atTop (𝓝 ‖y‖)
hd₁ : Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖d x‖) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop
have hcd₁ : Tendsto (fun (x : ℕ) ↦ ‖c x‖ / ‖d x‖⁻¹) atTop (𝓝 ‖y‖)
Tactic: simp only [norm_smul, norm_zero, ← div_inv_eq_mul] at hd₀ hcd
Cleared hypotheses: hd₀, hcd
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x y : E
hy₀ : y ≠ 0
c : ℕ → 𝕜
d : ℕ → E
hds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hd₀' : ∀ᶠ (n : ℕ) in atTop, d n ≠ 0
hd₀ : Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖d x‖) atTop (𝓝 0)
hcd : Tendsto (fun (x : ℕ) ↦ ‖c x‖ / ‖d x‖⁻¹) atTop (𝓝 ‖y‖)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop
have mp : Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖d x‖⁻¹) atTop atTop
Tactic: refine .num ?_ (by simpa) hcd
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Seq (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x y : E
hy₀ : y ≠ 0
c : ℕ → 𝕜
d : ℕ → E
hds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hd₀' : ∀ᶠ (n : ℕ) in atTop, d n ≠ 0
hd₀ : Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖d x‖) atTop (𝓝 0)
hcd : Tendsto (fun (x : ℕ) ↦ ‖c x‖ / ‖d x‖⁻¹) atTop (𝓝 ‖y‖)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖d x‖⁻¹) atTop atTop
have mp : Tendsto (α := ℕ) (β := ℝ) (Inv.inv ∘ fun (x : ℕ) ↦ ‖d x‖⁻¹) atTop (𝓝[>] 0)
Tactic: rw [← inv_nhdsGT_zero (𝕜 := ℝ), ← Filter.comap_inv, Filter.tendsto_comap_iff]
-- 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 + 1) s x₀ x =
    taylorWithinEval f n s x₀ x +
      ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
have simp_rw : HAdd.hAdd (α := E) (β := E) ((PolynomialModule.eval x : (a : PolynomialModule ℝ E) → E) (taylorWithin f n s x₀) : E)
    ((PolynomialModule.eval
            (Polynomial.eval x
              (HSub.hSub (α := Polynomial ℝ) (β := Polynomial ℝ) Polynomial.X
                ((Polynomial.C : (a : ℝ) → Polynomial ℝ) x₀ : Polynomial ℝ))) :
          (a : PolynomialModule ℝ E) → E)
        ((PolynomialModule.single ℝ (n + 1) : (a : E) → PolynomialModule ℝ E) (taylorCoeffWithin f (n + 1) s x₀) :
          PolynomialModule ℝ E) :
      E) =
  HAdd.hAdd (α := E) ((PolynomialModule.eval x : (a : PolynomialModule ℝ E) → E) (taylorWithin f n s x₀) : E)
    (((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀)
Tactic: simp_rw [taylorWithinEval, taylorWithin_succ, map_add, PolynomialModule.comp_eval]
-- 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 : ℝ
⊢ HAdd.hAdd (α := E) (β := E) ((PolynomialModule.eval x : (a : PolynomialModule ℝ E) → E) (taylorWithin f n s x₀) : E)
      ((PolynomialModule.eval
              (Polynomial.eval x
                (HSub.hSub (α := Polynomial ℝ) (β := Polynomial ℝ) Polynomial.X
                  ((Polynomial.C : (a : ℝ) → Polynomial ℝ) x₀ : Polynomial ℝ))) :
            (a : PolynomialModule ℝ E) → E)
          ((PolynomialModule.single ℝ (n + 1) : (a : E) → PolynomialModule ℝ E) (taylorCoeffWithin f (n + 1) s x₀) :
            PolynomialModule ℝ E) :
        E) =
    HAdd.hAdd (α := E) ((PolynomialModule.eval x : (a : PolynomialModule ℝ E) → E) (taylorWithin f n s x₀) : E)
      (((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀)
have e_a : (PolynomialModule.eval
        (Polynomial.eval x
          (HSub.hSub (α := Polynomial ℝ) (β := Polynomial ℝ) Polynomial.X
            ((Polynomial.C : (a : ℝ) → Polynomial ℝ) x₀ : Polynomial ℝ))) :
      (a : PolynomialModule ℝ E) → E)
    ((PolynomialModule.single ℝ (n + 1) : (a : E) → PolynomialModule ℝ E) (taylorCoeffWithin f (n + 1) s x₀) :
      PolynomialModule ℝ E) =
  ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
Tactic: congr
-- 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 : ℝ
⊢ (PolynomialModule.eval
          (Polynomial.eval x
            (HSub.hSub (α := Polynomial ℝ) (β := Polynomial ℝ) Polynomial.X
              ((Polynomial.C : (a : ℝ) → Polynomial ℝ) x₀ : Polynomial ℝ))) :
        (a : PolynomialModule ℝ E) → E)
      ((PolynomialModule.single ℝ (n + 1) : (a : E) → PolynomialModule ℝ E) (taylorCoeffWithin f (n + 1) s x₀) :
        PolynomialModule ℝ E) =
    ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
have e_a : (x - x₀) ^ (n + 1) • taylorCoeffWithin f (n + 1) s x₀ =
  ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
Tactic: simp only [Polynomial.eval_sub, Polynomial.eval_X, Polynomial.eval_C,
    PolynomialModule.eval_single, mul_inv_rev]
-- 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 : ℝ
⊢ (x - x₀) ^ (n + 1) • taylorCoeffWithin f (n + 1) s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
have e_a : (x - x₀) ^ (n + 1) • HSMul.hSMul (α := ℝ) (↑(n + 1)! : ℝ)⁻¹ (iteratedDerivWithin (n + 1) f s x₀) =
  ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s 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₀ x : ℝ
⊢ (x - x₀) ^ (n + 1) • HSMul.hSMul (α := ℝ) (↑(n + 1)! : ℝ)⁻¹ (iteratedDerivWithin (n + 1) f s x₀) =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
have e_a : ((x - x₀) ^ (n + 1) * (↑(n + 1)! : ℝ)⁻¹) • iteratedDerivWithin (n + 1) f s x₀ =
  ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
Tactic: rw [← mul_smul, mul_comm, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one,
    mul_inv_rev]
-- 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 : ℝ
e_a :
  ((x - x₀) ^ (n + 1) * (↑(n + 1)! : ℝ)⁻¹) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
⊢ (x - x₀) ^ (n + 1) • HSMul.hSMul (α := ℝ) (↑(n + 1)! : ℝ)⁻¹ (iteratedDerivWithin (n + 1) f s x₀) =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
have e_a₁ : ((↑(n + 1)! : ℝ)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
  ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
Tactic: rw [← mul_smul, mul_comm, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one,
    mul_inv_rev]
-- 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 : ℝ
e_a :
  ((x - x₀) ^ (n + 1) * (↑(n + 1)! : ℝ)⁻¹) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
e_a₁ :
  ((↑(n + 1)! : ℝ)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
⊢ (x - x₀) ^ (n + 1) • HSMul.hSMul (α := ℝ) (↑(n + 1)! : ℝ)⁻¹ (iteratedDerivWithin (n + 1) f s x₀) =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
have e_a₂ : ((↑((n + 1) * n !) : ℝ)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
  ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
Tactic: rw [← mul_smul, mul_comm, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one,
    mul_inv_rev]
-- 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 : ℝ
e_a :
  ((x - x₀) ^ (n + 1) * (↑(n + 1)! : ℝ)⁻¹) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
e_a₁ :
  ((↑(n + 1)! : ℝ)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
e_a₂ :
  ((↑((n + 1) * n !) : ℝ)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
⊢ (x - x₀) ^ (n + 1) • HSMul.hSMul (α := ℝ) (↑(n + 1)! : ℝ)⁻¹ (iteratedDerivWithin (n + 1) f s x₀) =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
have e_a₃ : ((HMul.hMul (α := ℝ) (↑(n + 1) : ℝ) (↑n ! : ℝ))⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
  ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
Tactic: rw [← mul_smul, mul_comm, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one,
    mul_inv_rev]
-- 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 : ℝ
e_a :
  ((x - x₀) ^ (n + 1) * (↑(n + 1)! : ℝ)⁻¹) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
e_a₁ :
  ((↑(n + 1)! : ℝ)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
e_a₂ :
  ((↑((n + 1) * n !) : ℝ)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
e_a₃ :
  ((HMul.hMul (α := ℝ) (↑(n + 1) : ℝ) (↑n ! : ℝ))⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
⊢ (x - x₀) ^ (n + 1) • HSMul.hSMul (α := ℝ) (↑(n + 1)! : ℝ)⁻¹ (iteratedDerivWithin (n + 1) f s x₀) =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
have e_a₄ : ((HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑1 : ℝ) * (↑n ! : ℝ))⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
  ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
Tactic: rw [← mul_smul, mul_comm, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one,
    mul_inv_rev]
-- 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 : ℝ
e_a :
  ((x - x₀) ^ (n + 1) * (↑(n + 1)! : ℝ)⁻¹) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
e_a₁ :
  ((↑(n + 1)! : ℝ)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
e_a₂ :
  ((↑((n + 1) * n !) : ℝ)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
e_a₃ :
  ((HMul.hMul (α := ℝ) (↑(n + 1) : ℝ) (↑n ! : ℝ))⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
e_a₄ :
  ((HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑1 : ℝ) * (↑n ! : ℝ))⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
⊢ (x - x₀) ^ (n + 1) • HSMul.hSMul (α := ℝ) (↑(n + 1)! : ℝ)⁻¹ (iteratedDerivWithin (n + 1) f s x₀) =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
have e_a₅ : ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
  ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
Tactic: rw [← mul_smul, mul_comm, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one,
    mul_inv_rev]
-- 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 : ℝ
e_a :
  ((x - x₀) ^ (n + 1) * (↑(n + 1)! : ℝ)⁻¹) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
e_a₁ :
  ((↑(n + 1)! : ℝ)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
e_a₂ :
  ((↑((n + 1) * n !) : ℝ)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
e_a₃ :
  ((HMul.hMul (α := ℝ) (↑(n + 1) : ℝ) (↑n ! : ℝ))⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
e_a₄ :
  ((HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑1 : ℝ) * (↑n ! : ℝ))⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
e_a₅ :
  ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
⊢ (x - x₀) ^ (n + 1) • HSMul.hSMul (α := ℝ) (↑(n + 1)! : ℝ)⁻¹ (iteratedDerivWithin (n + 1) f s x₀) =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
have e_a₆ : ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
  ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
Tactic: rw [← mul_smul, mul_comm, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one,
    mul_inv_rev]
-- 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 : ℝ
⊢ taylorWithinEval f 0 s x₀ x = f x₀
have dsimp : (PolynomialModule.eval x : (a : PolynomialModule ℝ E) → E) (taylorWithin f 0 s x₀) = f x₀
Tactic: dsimp only [taylorWithinEval]