awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
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
N : ℕ
h : True
n : ℕ
hn : N ≤ n
refine : (1 / (2 * ‖c‖)) ^ n ≤ 1 / HPow.hPow (α := ℝ) 2 N / ‖c‖ ^ n
⊢ ‖d n‖ < 1 / HPow.hPow (α := ℝ) 2 N / ‖c‖ ^ n

Tactic:
refine (hd n).trans_le ?_

Premises used: LT.lt.trans_le
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
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
N : ℕ
h : True
n : ℕ
hn : N ≤ n
grw : (1 / (2 * ‖c‖)) ^ n ≤ 1 / HPow.hPow (α := ℝ) 2 n / ‖c‖ ^ n
h₂ : LE.le (α := ℝ) 1 2
⊢ (1 / (2 * ‖c‖)) ^ n ≤ 1 / HPow.hPow (α := ℝ) 2 N / ‖c‖ ^ n

Tactic:
grw [hn]
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
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
N : ℕ
h : True
n : ℕ
hn : N ≤ n
⊢ (1 / (2 * ‖c‖)) ^ n ≤ 1 / HPow.hPow (α := ℝ) 2 n / ‖c‖ ^ n

Tactic:
simp [mul_pow, div_eq_inv_mul]

Premises used: div_eq_inv_mul, mul_pow
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
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
N : ℕ
h : True
n : ℕ
hn : N ≤ n
⊢ LE.le (α := ℝ) 1 2

Tactic:
norm_num1
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
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
h₂ h₃ : ∀ (N : ℕ), True → ∀ (n : ℕ) (hn : N ≤ n), LE.le (α := ℝ) 1 2
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((fun (x : ℕ) ↦ c ^ x) n) (d n)) atTop
    (𝓝 0)

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

Premises used: Filter.atTop_basis, lt_div_iff₀', Filter.HasBasis.tendsto_iff, one_half_lt_one, one_half_pos, Set.mem_Ici, div_eq_inv_mul, mul_pow, Metric.nhds_basis_ball_pow
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
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
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)
⊢ 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)

Tactic:
rw [mem_tangentConeAt_iff_exists_seq]

Premises used: mem_tangentConeAt_iff_exists_seq
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
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)

Tactic:
⟨c, d, ?_, hds, hcd⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
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)
mp : Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop
⊢ ∃ (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:
refine ⟨c, d, ?_, hds, hcd⟩
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
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 : ℕ) ↦ ‖d x‖) atTop (𝓝 (norm.{u_2} (E := E) 0))

Tactic:
replace hd₀ := hd₀.norm
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
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))
⊢ ∀ᶠ (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
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
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 • d x‖) atTop (𝓝 ‖y‖)

Tactic:
replace hcd := hcd.norm
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
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 : ℕ) ↦ ‖d x‖) atTop (𝓝 0)

Tactic:
simp only [norm_smul, norm_zero, ← div_inv_eq_mul] at hd₀ hcd

Premises used: norm_smul, norm_zero, div_inv_eq_mul
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
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‖ / ‖d x‖⁻¹) atTop (𝓝 ‖y‖)

Tactic:
simp only [norm_smul, norm_zero, ← div_inv_eq_mul] at hd₀ hcd

Premises used: norm_smul, norm_zero, div_inv_eq_mul
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
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‖)
⊢ 0 < ‖y‖

Tactic:
simpa
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
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‖)
mp : Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖d x‖⁻¹) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop

Tactic:
refine .num ?_ (by simpa) hcd
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
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‖)
mp : Tendsto (α := ℕ) (β := ℝ) (Inv.inv ∘ fun (x : ℕ) ↦ ‖d x‖⁻¹) atTop (𝓝[>] 0)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖d x‖⁻¹) atTop atTop

Tactic:
rw [← inv_nhdsGT_zero (𝕜 := ℝ), ← Filter.comap_inv, Filter.tendsto_comap_iff]

Premises used: Filter.tendsto_comap_iff, inv_nhdsGT_zero, Filter.comap_inv
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
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 (α := ℕ) (β := ℝ) (Inv.inv ∘ fun (x : ℕ) ↦ ‖d x‖⁻¹) atTop (𝓝[>] 0)

Tactic:
simpa [Function.comp_def, tendsto_nhdsWithin_iff, hd₀] using hd₀'

Premises used: tendsto_nhdsWithin_iff, Function.comp_def
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x y : E
c : ℕ → 𝕜
d : ℕ → E
hc : Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop
hds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hcd : Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
⊢ y ∈ tangentConeAt 𝕜 s x

Tactic:
mem_tangentConeAt_of_seq atTop c d (tangentConeAt.lim_zero atTop hc hcd) hds hcd

Premises used: tangentConeAt.lim_zero, Filter.atTop, mem_tangentConeAt_of_seq
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x y : E
c : ℕ → 𝕜
d : ℕ → E
hc : Tendsto (β := ℝ) (fun (x : ℕ) ↦ ‖c x‖) atTop atTop
hds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hcd : Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
⊢ y ∈ tangentConeAt 𝕜 s x

Tactic:
exact mem_tangentConeAt_of_seq atTop c d (tangentConeAt.lim_zero atTop hc hcd) hds hcd

Premises used: tangentConeAt.lim_zero, Filter.atTop, mem_tangentConeAt_of_seq
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
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₀)
⊢ 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₀

Tactic:
simp_rw [taylorWithinEval, taylorWithin_succ, map_add, PolynomialModule.comp_eval]

Premises used: taylorWithinEval, taylorWithin_succ, map_add, PolynomialModule.comp_eval
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
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₀
⊢ 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:
congr
-- Module: Mathlib.Analysis.Calculus.Taylor
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) • taylorCoeffWithin f (n + 1) s x₀ =
    ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s 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₀

Tactic:
simp only [Polynomial.eval_sub, Polynomial.eval_X, Polynomial.eval_C,
    PolynomialModule.eval_single, mul_inv_rev]

Premises used: Polynomial.eval_C, Polynomial.eval_X, mul_inv_rev, Polynomial.eval_sub, PolynomialModule.eval_single
-- Module: Mathlib.Analysis.Calculus.Taylor
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) • 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₀
⊢ (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:
dsimp only [taylorCoeffWithin]

Premises used: taylorCoeffWithin
-- Module: Mathlib.Analysis.Calculus.Taylor
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₀
e_a₆ 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₀
⊢ (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:
rw [← mul_smul, mul_comm, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one,
    mul_inv_rev]

Premises used: Nat.factorial_succ, Nat.cast_add, Nat.cast_mul, mul_comm, mul_inv_rev, Nat.cast_one, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
dsimp : (PolynomialModule.eval x : (a : PolynomialModule ℝ E) → E) (taylorWithin f 0 s x₀) = f x₀
⊢ taylorWithinEval f 0 s x₀ x = f x₀

Tactic:
dsimp only [taylorWithinEval]

Premises used: taylorWithinEval
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
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₀
⊢ (PolynomialModule.eval x : (a : PolynomialModule ℝ E) → E) (taylorWithin f 0 s x₀) = f x₀

Tactic:
dsimp only [taylorWithin]

Premises used: taylorWithin
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
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₀
⊢ (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 [taylorCoeffWithin]

Premises used: taylorCoeffWithin
-- Module: Mathlib.Analysis.Calculus.Taylor
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)
            (HSMul.hSMul (α := ℝ) (↑k ! : ℝ)⁻¹ (iteratedDerivWithin k f s x₀)))) =
    f x₀

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ : ℝ
⊢ taylorWithinEval f 0 s x₀ x₀ = f x₀

Tactic:
taylor_within_zero_eval _ _ _ _

Premises used: taylor_within_zero_eval
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ : ℝ
⊢ taylorWithinEval f 0 s x₀ x₀ = f x₀

Tactic:
exact taylor_within_zero_eval _ _ _ _

Premises used: taylor_within_zero_eval
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ : ℝ
k : ℕ
hk : taylorWithinEval f k s x₀ x₀ = f x₀
⊢ taylorWithinEval f (k + 1) s x₀ x₀ = f x₀

Tactic:
simp [hk]
-- Module: Mathlib.Analysis.Calculus.Taylor
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₀
succ : ∀ (k : ℕ) (hk : taylorWithinEval f k s x₀ x₀ = f x₀), taylorWithinEval f (k + 1) s x₀ x₀ = f x₀
⊢ taylorWithinEval f n s x₀ x₀ = f x₀

Tactic:
induction n with
  | zero => exact taylor_within_zero_eval _ _ _ _
  | succ k hk => simp [hk]

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

Tactic:
simp