awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
inst_4 : CharZero 𝕜
n' : ℕ
hk : ∀ {n : ℕ}, (↑n : ℕ∞) = analyticOrderAt f z₀ → n ≠ 0 → n' ≤ n → analyticOrderAt (deriv^[n'] f) z₀ = (↑(n - n') : ℕ∞)
n : ℕ
Hn : (↑n : ℕ∞) = analyticOrderAt f z₀
Hpos : n ≠ 0
Hk : n' + 1 ≤ n
⊢ analyticOrderAt (deriv^[n'] f) z₀ = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) (↑n'.succ : ℕ∞) + 1
have refine : (↑(n - n') : ℕ∞) = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) (↑n'.succ : ℕ∞) + 1
Tactic: refine (hk Hn Hpos (by lia)).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (hypothesis)
Goal:
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
inst_4 : CharZero 𝕜
n' : ℕ
hk : ∀ {n : ℕ}, (↑n : ℕ∞) = analyticOrderAt f z₀ → n ≠ 0 → n' ≤ n → analyticOrderAt (deriv^[n'] f) z₀ = (↑(n - n') : ℕ∞)
n : ℕ
Hn : (↑n : ℕ∞) = analyticOrderAt f z₀
Hpos : n ≠ 0
Hk : n' + 1 ≤ n
⊢ (↑(n - n') : ℕ∞) = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) (↑n'.succ : ℕ∞) + 1
have this : n - n'.succ + 1 = n - n'
Tactic: have : (n - n'.succ) + 1 = n - n' := by grind
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
inst_4 : CharZero 𝕜
n' : ℕ
hk : ∀ {n : ℕ}, (↑n : ℕ∞) = analyticOrderAt f z₀ → n ≠ 0 → n' ≤ n → analyticOrderAt (deriv^[n'] f) z₀ = (↑(n - n') : ℕ∞)
n : ℕ
Hn : (↑n : ℕ∞) = analyticOrderAt f z₀
Hpos : n ≠ 0
Hk : n' + 1 ≤ n
this : n - n'.succ + 1 = n - n'
⊢ (↑(n - n') : ℕ∞) = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) (↑n'.succ : ℕ∞) + 1
have rw : (↑(n - n'.succ + 1) : ℕ∞) = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) (↑n'.succ : ℕ∞) + 1
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (hypothesis)
Goal:
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
inst_4 : CharZero 𝕜
n' : ℕ
hk : ∀ {n : ℕ}, (↑n : ℕ∞) = analyticOrderAt f z₀ → n ≠ 0 → n' ≤ n → analyticOrderAt (deriv^[n'] f) z₀ = (↑(n - n') : ℕ∞)
n : ℕ
Hn : (↑n : ℕ∞) = analyticOrderAt f z₀
Hpos : n ≠ 0
Hk : n' + 1 ≤ n
⊢ analyticOrderAt ((deriv ∘ deriv^[n']) f) z₀ = (↑(n - (n' + 1)) : ℕ∞)
have horder : analyticOrderAt (deriv^[n'] f) z₀ = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) (↑n'.succ : ℕ∞) + 1
Tactic: have horder : analyticOrderAt (deriv^[n'] f) z₀ = (n - n'.succ) + 1 := by
      refine (hk Hn Hpos (by lia)).trans ?_
      have : (n - n'.succ) + 1 = n - n' := by grind
      rw [← this]
      simp
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
k n : ℕ
inst_4 : CharZero 𝕜
⊢ (↑n : ℕ∞) = analyticOrderAt f z₀ → n ≠ 0 → k ≤ n → analyticOrderAt (deriv^[k] f) z₀ = (↑(n - k) : ℕ∞)
have zero : ∀ {n : ℕ}, (↑n : ℕ∞) = analyticOrderAt f z₀ → n ≠ 0 → 0 ≤ n → analyticOrderAt (deriv^[0] f) z₀ = (↑(n - 0) : ℕ∞)
Tactic: induction k generalizing n with
  | zero => exact fun Hn Hpos Hk ↦ Hn.symm
  | succ n' hk =>
    intro Hn Hpos Hk
    rw [Function.iterate_succ']
    have horder : analyticOrderAt (deriv^[n'] f) z₀ = (n - n'.succ) + 1 := by
      refine (hk Hn Hpos (by lia)).trans ?_
      have : (n - n'.succ) + 1 = n - n' := by grind
      rw [← this]
      simp
    simpa using (analyticOrderAt_deriv_of_pos (hf := AnalyticAt.iterated_deriv hf n')
      (n := n - n'.succ) horder)
Cleared hypotheses: k, n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
k n : ℕ
inst_4 : CharZero 𝕜
zero : ∀ {n : ℕ}, (↑n : ℕ∞) = analyticOrderAt f z₀ → n ≠ 0 → 0 ≤ n → analyticOrderAt (deriv^[0] f) z₀ = (↑(n - 0) : ℕ∞)
⊢ (↑n : ℕ∞) = analyticOrderAt f z₀ → n ≠ 0 → k ≤ n → analyticOrderAt (deriv^[k] f) z₀ = (↑(n - k) : ℕ∞)
have succ : ∀ (n' : ℕ)
  (hk :
    ∀ {n : ℕ}, (↑n : ℕ∞) = analyticOrderAt f z₀ → n ≠ 0 → n' ≤ n → analyticOrderAt (deriv^[n'] f) z₀ = (↑(n - n') : ℕ∞))
  {n : ℕ},
  (↑n : ℕ∞) = analyticOrderAt f z₀ → n ≠ 0 → n' + 1 ≤ n → analyticOrderAt (deriv^[n' + 1] f) z₀ = (↑(n - (n' + 1)) : ℕ∞)
Tactic: induction k generalizing n with
  | zero => exact fun Hn Hpos Hk ↦ Hn.symm
  | succ n' hk =>
    intro Hn Hpos Hk
    rw [Function.iterate_succ']
    have horder : analyticOrderAt (deriv^[n'] f) z₀ = (n - n'.succ) + 1 := by
      refine (hk Hn Hpos (by lia)).trans ?_
      have : (n - n'.succ) + 1 = n - n' := by grind
      rw [← this]
      simp
    simpa using (analyticOrderAt_deriv_of_pos (hf := AnalyticAt.iterated_deriv hf n')
      (n := n - n'.succ) horder)
Cleared hypotheses: k, n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
⊢ ∃ (F : 𝕜 → E),
    AnalyticAt 𝕜 F 0 ∧
      ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
have simp : ∃ (F : 𝕜 → E),
  AnalyticAt 𝕜 F 0 ∧
    ∀ᶠ (z : 𝕜) in 𝓝 0, f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 = z ^ n • F z
Tactic: simp only [← sub_eq_iff_eq_add']
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
⊢ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E)
    (fun (z : 𝕜) ↦ ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0) 0
have refine : ∀ (i : ℕ) (hi : i ∈ Finset.range n),
  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0) 0
Tactic: refine Finset.analyticAt_fun_sum _ fun i hi ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
⊢ ∃ (F : 𝕜 → E),
    AnalyticAt 𝕜 F 0 ∧
      ∀ᶠ (z : 𝕜) in 𝓝 0, f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 = z ^ n • F z
have this : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E)
  (fun (z : 𝕜) ↦ ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0) 0
Tactic: have : AnalyticAt 𝕜
      (fun z : 𝕜 ↦ ∑ i ∈ .range n, (z ^ i / i.factorial) • iteratedDeriv i f 0) 0 := by
    refine Finset.analyticAt_fun_sum _ fun i hi ↦ ?_
    fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
this :
  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E)
    (fun (z : 𝕜) ↦ ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0) 0
⊢ ∃ (F : 𝕜 → E),
    AnalyticAt 𝕜 F 0 ∧
      ∀ᶠ (z : 𝕜) in 𝓝 0, f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 = z ^ n • F z
have h : ∀ (x : 𝕜 → E) (x : 𝕜), x = x - 0
Tactic: convert! (natCast_le_analyticOrderAt (hf.fun_sub this)).mp ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
this :
  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E)
    (fun (z : 𝕜) ↦ ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0) 0
h : ∀ (x : 𝕜 → E) (x : 𝕜), x = x - 0
⊢ ∃ (F : 𝕜 → E),
    AnalyticAt 𝕜 F 0 ∧
      ∀ᶠ (z : 𝕜) in 𝓝 0, f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 = z ^ n • F z
have convert_2 : (↑n : ℕ∞) ≤
  analyticOrderAt.{u_1, u_2} (E := E)
    (fun (i : 𝕜) ↦ f i - ∑ i_1 ∈ Finset.range n, (i ^ i_1 / (↑i_1.factorial : 𝕜)) • iteratedDeriv i_1 f 0) 0
Tactic: convert! (natCast_le_analyticOrderAt (hf.fun_sub this)).mp ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
this :
  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E)
    (fun (z : 𝕜) ↦ ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0) 0
⊢ (↑n : ℕ∞) ≤
    analyticOrderAt.{u_1, u_2} (E := E)
      (fun (i : 𝕜) ↦ f i - ∑ i_1 ∈ Finset.range n, (i ^ i_1 / (↑i_1.factorial : 𝕜)) • iteratedDeriv i_1 f 0) 0
have convert_2 : ∀ i < n,
  Eq.{u_2 + 1} (α := E)
    (iteratedDeriv i
      (fun (i : 𝕜) ↦ f i - ∑ i_1 ∈ Finset.range n, (i ^ i_1 / (↑i_1.factorial : 𝕜)) • iteratedDeriv i_1 f 0) 0)
    0
Tactic: rw [natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero (hf.fun_sub this)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
this :
  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E)
    (fun (z : 𝕜) ↦ ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0) 0
i : ℕ
hi : i < n
⊢ Eq.{u_2 + 1} (α := E)
    (iteratedDeriv i
      (fun (i : 𝕜) ↦ f i - ∑ i_1 ∈ Finset.range n, (i ^ i_1 / (↑i_1.factorial : 𝕜)) • iteratedDeriv i_1 f 0) 0)
    0
have convert_2 : iteratedDeriv i f 0 -
    iteratedDeriv i (fun (z : 𝕜) ↦ ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0) 0 =
  0
Tactic: rw [iteratedDeriv_fun_sub (AnalyticAt.contDiffAt <| by fun_prop) this.contDiffAt]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
this :
  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E)
    (fun (z : 𝕜) ↦ ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0) 0
i : ℕ
hi : i < n
⊢ iteratedDeriv i f 0 -
      iteratedDeriv i (fun (z : 𝕜) ↦ ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0) 0 =
    0
have convert_2 : iteratedDeriv i f 0 -
    ∑ x ∈ Finset.range n,
      HDiv.hDiv (α := 𝕜) (↑(if i = x then x.factorial else 0) : 𝕜) (↑x.factorial : 𝕜) • iteratedDeriv x f 0 =
  0
Tactic: simp (disch := fun_prop) only [iteratedDeriv_fun_sum, iteratedDeriv_smul_const,
      iteratedDeriv_div_const, iteratedDeriv_fun_pow_zero]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
⊢ ∃ (F : 𝕜 → E),
    AnalyticAt 𝕜 F 0 ∧
      ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
have obtain : ∀ (F : 𝕜 → E) (hFa : AnalyticAt 𝕜 F 0)
  (hF :
    ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z),
  ∃ (F : 𝕜 → E),
    AnalyticAt 𝕜 F 0 ∧
      ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
Tactic: obtain ⟨F, hFa, hF⟩ := hf.exists_eventuallyEq_sum_add_pow_mul n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
⊢ ∃ (v : Set 𝕜),
    Membership.mem (γ := Filter 𝕜) (𝓝 0) v ∧
      ∀ y ∈ v, f y = ∑ i ∈ Finset.range n, (y ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + y ^ n • F y
have rwa : ∀
  (hF :
    ∃ (v : Set 𝕜),
      Membership.mem (γ := Filter 𝕜) (𝓝 0) v ∧
        ∀ y ∈ v, f y = ∑ i ∈ Finset.range n, (y ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + y ^ n • F y),
  ∃ (v : Set 𝕜),
    Membership.mem (γ := Filter 𝕜) (𝓝 0) v ∧
      ∀ y ∈ v, f y = ∑ i ∈ Finset.range n, (y ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + y ^ n • F y
Tactic: rwa [eventually_iff_exists_mem] at hF
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
⊢ ∃ (F : 𝕜 → E),
    AnalyticAt 𝕜 F 0 ∧
      ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
have obtain : ∀ (U : Set 𝕜) (hU0 : Membership.mem (γ := Filter 𝕜) (𝓝 0) U)
  (hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + y ^ n • F y),
  ∃ (F : 𝕜 → E),
    AnalyticAt 𝕜 F 0 ∧
      ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
Tactic: obtain ⟨U, hU0, hU'⟩ := by rwa [eventually_iff_exists_mem] at hF
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : Membership.mem (γ := Filter 𝕜) (𝓝 0) U
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + y ^ n • F y
⊢ ∃ (F : 𝕜 → E),
    AnalyticAt 𝕜 F 0 ∧
      ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
have refine_1 : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E)
  (fun (z : 𝕜) ↦
    if z ∈ U then F z else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0))
  0
Tactic: refine ⟨fun z ↦ if z ∈ U then F z else (z ^ n)⁻¹ • (f z
      - (∑ i ∈ .range n, (z ^ i / i.factorial) • iteratedDeriv i f 0)), ?_, fun z ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : Membership.mem (γ := Filter 𝕜) (𝓝 0) U
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + y ^ n • F y
refine_1 :
  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E)
    (fun (z : 𝕜) ↦
      if z ∈ U then F z
      else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0))
    0
⊢ ∃ (F : 𝕜 → E),
    AnalyticAt 𝕜 F 0 ∧
      ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
have refine_2 : ∀ (z : 𝕜),
  f z =
    ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 +
      HSMul.hSMul (β := E) (z ^ n)
        ((fun (z : 𝕜) ↦
            if z ∈ U then F z
            else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0))
          z)
Tactic: refine ⟨fun z ↦ if z ∈ U then F z else (z ^ n)⁻¹ • (f z
      - (∑ i ∈ .range n, (z ^ i / i.factorial) • iteratedDeriv i f 0)), ?_, fun z ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : Membership.mem (γ := Filter 𝕜) (𝓝 0) U
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + y ^ n • F y
⊢ F =ᶠ[𝓝 0] fun (z : 𝕜) ↦
    if z ∈ U then F z else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0)
have h : ∀ (a : 𝕜),
  Membership.mem (γ := Set 𝕜)
    {x : 𝕜 |
      x ∈ U →
        Membership.mem (γ := Set 𝕜)
          {x : 𝕜 |
            (fun (x : 𝕜) ↦
                F x =
                  (fun (z : 𝕜) ↦
                      if z ∈ U then F z
                      else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0))
                    x)
              x}
          x}
    a
Tactic: filter_upwards [hU0] using by simp +contextual
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : Membership.mem (γ := Filter 𝕜) (𝓝 0) U
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + y ^ n • F y
h :
  ∀ (a : 𝕜),
    Membership.mem (γ := Set 𝕜)
      {x : 𝕜 |
        x ∈ U →
          Membership.mem (γ := Set 𝕜)
            {x : 𝕜 |
              (fun (x : 𝕜) ↦
                  F x =
                    (fun (z : 𝕜) ↦
                        if z ∈ U then F z
                        else
                          (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0))
                      x)
                x}
            x}
      a
⊢ F =ᶠ[𝓝 0] fun (z : 𝕜) ↦
    if z ∈ U then F z else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0)
have h₁ : ∀ a ∈ U,
  F a =
    if a ∈ U then F a else (a ^ n)⁻¹ • (f a - ∑ i ∈ Finset.range n, (a ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0)
Tactic: filter_upwards [hU0] using by simp +contextual
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : Membership.mem (γ := Filter 𝕜) (𝓝 0) U
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + y ^ n • F y
z : 𝕜
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 +
      HSMul.hSMul (β := E) (z ^ n)
        ((fun (z : 𝕜) ↦
            if z ∈ U then F z
            else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0))
          z)
have pos : ∀ (hz : z ∈ U),
  f z =
    ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 +
      HSMul.hSMul (β := E) (z ^ n)
        ((fun (z : 𝕜) ↦
            if z ∈ U then F z
            else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0))
          z)
Tactic: by_cases hz : z ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : Membership.mem (γ := Filter 𝕜) (𝓝 0) U
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + y ^ n • F y
z : 𝕜
pos :
  ∀ (hz : z ∈ U),
    f z =
      ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 +
        HSMul.hSMul (β := E) (z ^ n)
          ((fun (z : 𝕜) ↦
              if z ∈ U then F z
              else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0))
            z)
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 +
      HSMul.hSMul (β := E) (z ^ n)
        ((fun (z : 𝕜) ↦
            if z ∈ U then F z
            else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0))
          z)
have neg : ∀ (hz : z ∉ U),
  f z =
    ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 +
      HSMul.hSMul (β := E) (z ^ n)
        ((fun (z : 𝕜) ↦
            if z ∈ U then F z
            else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0))
          z)
Tactic: by_cases hz : z ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : Membership.mem (γ := Filter 𝕜) (𝓝 0) U
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + y ^ n • F y
z : 𝕜
hz : z ∉ U
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 +
      HSMul.hSMul (β := E) (z ^ n)
        ((fun (z : 𝕜) ↦
            if z ∈ U then F z
            else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0))
          z)
have neg : f z =
  ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 +
    z ^ n • (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0)
Tactic: simp only [if_neg hz]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Order (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : Membership.mem (γ := Filter 𝕜) (𝓝 0) U
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 + y ^ n • F y
z : 𝕜
hz : z ∉ U
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 +
      z ^ n • (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0)
have neg : f z =
  ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 +
    (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0)
Tactic: rw [smul_inv_smul₀]