awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
r : ℕ∞
h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = r
top : ∀ (h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = ⊤), Eq (α := ℕ∞) ⊤ 1
coe :
  ∀ (r : ℕ) (h : analyticOrderAt.{u_1, u_2} (E := E) (fun (x_1 : 𝕜) ↦ f x_1 - f x) x = (↑r : ℕ∞)),
    Eq (α := ℕ∞) (↑r : ℕ∞) 1
⊢ r = 1

Tactic:
cases r with
  | top =>
    simp_rw [analyticOrderAt_eq_top, sub_eq_zero] at h
    refine (hf' ?_).elim
    rw [EventuallyEq.deriv_eq h, deriv_const]
  | coe r =>
    norm_cast
    obtain ⟨F, hFa, hFne, hfF⟩ := (analyticOrderAt_eq_natCast (by fun_prop)).mp h
    apply eq_of_ge_of_le
    · by_contra! hr
      have := hfF.self_of_nhds
      simp_all
    · contrapose! hf'
      simp_rw [sub_eq_iff_eq_add] at hfF
      rw [EventuallyEq.deriv_eq hfF, deriv_add_const, deriv_fun_smul (by fun_prop) (by fun_prop),
        deriv_fun_pow (by fun_prop), sub_self, zero_pow (by lia), zero_pow (by lia),
        mul_zero, zero_mul, zero_smul, zero_smul, add_zero]

Premises used: sub_self, analyticOrderAt_eq_top, sub_eq_zero, deriv_fun_smul, False.elim, MulZeroClass.zero_mul, eq_of_ge_of_le, AnalyticAt.analyticOrderAt_eq_natCast, MulZeroClass.mul_zero, zero_smul, deriv_const, sub_eq_iff_eq_add, Iff.mp, deriv_add_const, deriv_fun_pow, add_zero, zero_pow
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
hfx : f x = 0
hf' : deriv f x ≠ 0
⊢ analyticOrderAt f x = 1

Tactic:
simpa [hfx] using hf.analyticOrderAt_sub_eq_one_of_deriv_ne_zero hf'

Premises used: AnalyticAt.analyticOrderAt_sub_eq_one_of_deriv_ne_zero
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
z₀ : 𝕜
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
⊢ (↑0 : ℕ∞) ≤ analyticOrderAt f z₀ ↔ ∀ i < 0, iteratedDeriv i f z₀ = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
z₀ : 𝕜
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
n : ℕ
IH : ∀ {f : 𝕜 → E} (hf : AnalyticAt 𝕜 f z₀), (↑n : ℕ∞) ≤ analyticOrderAt f z₀ ↔ ∀ i < n, iteratedDeriv i f z₀ = 0
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
pos : ∀ (hfz : f z₀ = 0), (↑(n + 1) : ℕ∞) ≤ analyticOrderAt f z₀ ↔ ∀ i < n + 1, iteratedDeriv i f z₀ = 0
neg : ∀ (hfz : ¬f z₀ = 0), (↑(n + 1) : ℕ∞) ≤ analyticOrderAt f z₀ ↔ ∀ i < n + 1, iteratedDeriv i f z₀ = 0
⊢ (↑(n + 1) : ℕ∞) ≤ analyticOrderAt f z₀ ↔ ∀ i < n + 1, iteratedDeriv i f z₀ = 0

Tactic:
by_cases hfz : f z₀ = 0
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
z₀ : 𝕜
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
n : ℕ
IH : ∀ {f : 𝕜 → E} (hf : AnalyticAt 𝕜 f z₀), (↑n : ℕ∞) ≤ analyticOrderAt f z₀ ↔ ∀ i < n, iteratedDeriv i f z₀ = 0
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hfz : ¬f z₀ = 0
⊢ 0 ≤ n

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
z₀ : 𝕜
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
n : ℕ
IH : ∀ {f : 𝕜 → E} (hf : AnalyticAt 𝕜 f z₀), (↑n : ℕ∞) ≤ analyticOrderAt f z₀ ↔ ∀ i < n, iteratedDeriv i f z₀ = 0
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hfz : ¬f z₀ = 0
⊢ ¬iteratedDeriv 0 f z₀ = 0

Tactic:
simpa
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
z₀ : 𝕜
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
n : ℕ
IH : ∀ {f : 𝕜 → E} (hf : AnalyticAt 𝕜 f z₀), (↑n : ℕ∞) ≤ analyticOrderAt f z₀ ↔ ∀ i < n, iteratedDeriv i f z₀ = 0
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hfz : ¬f z₀ = 0
⊢ (↑(n + 1) : ℕ∞) ≤ analyticOrderAt f z₀ ↔ ∀ i < n + 1, iteratedDeriv i f z₀ = 0

Tactic:
simpa [analyticOrderAt_eq_zero.mpr (.inr hfz)] using ⟨0, by simp, by simpa⟩

Premises used: Iff.mpr, analyticOrderAt_eq_zero, Or.inr
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
z₀ : 𝕜
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
n : ℕ
IH : ∀ {f : 𝕜 → E} (hf : AnalyticAt 𝕜 f z₀), (↑n : ℕ∞) ≤ analyticOrderAt f z₀ ↔ ∀ i < n, iteratedDeriv i f z₀ = 0
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hfz : f z₀ = 0
⊢ analyticOrderAt (deriv f) z₀ + 1 = analyticOrderAt f z₀

Tactic:
simpa [hfz] using hf.analyticOrderAt_deriv_add_one

Premises used: AnalyticAt.analyticOrderAt_deriv_add_one
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
z₀ : 𝕜
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
n : ℕ
IH : ∀ {f : 𝕜 → E} (hf : AnalyticAt 𝕜 f z₀), (↑n : ℕ∞) ≤ analyticOrderAt f z₀ ↔ ∀ i < n, iteratedDeriv i f z₀ = 0
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hfz : f z₀ = 0
⊢ analyticOrderAt (deriv f) z₀ + 1 = analyticOrderAt f z₀

Tactic:
have : analyticOrderAt (deriv f) z₀ + 1 = analyticOrderAt f z₀ := by
      simpa [hfz] using hf.analyticOrderAt_deriv_add_one
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
z₀ : 𝕜
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
n : ℕ
IH : ∀ {f : 𝕜 → E} (hf : AnalyticAt 𝕜 f z₀), (↑n : ℕ∞) ≤ analyticOrderAt f z₀ ↔ ∀ i < n, iteratedDeriv i f z₀ = 0
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hfz : f z₀ = 0
this : analyticOrderAt (deriv f) z₀ + 1 = analyticOrderAt f z₀
⊢ (↑(n + 1) : ℕ∞) ≤ analyticOrderAt f z₀ ↔ ∀ i < n + 1, iteratedDeriv i f z₀ = 0

Tactic:
simp [← this, IH hf.deriv, iteratedDeriv_succ',
      -Order.lt_add_one_iff, Nat.forall_lt_succ_left, hfz]

Premises used: Nat.forall_lt_succ_left, iteratedDeriv_succ', AnalyticAt.deriv, Order.lt_add_one_iff
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
n : ℕ
z₀ : 𝕜
inst_3 : CharZero 𝕜
inst_4 : CompleteSpace E
hf : AnalyticAt 𝕜 f z₀
zero : ∀ {f : 𝕜 → E} (hf : AnalyticAt 𝕜 f z₀), (↑0 : ℕ∞) ≤ analyticOrderAt f z₀ ↔ ∀ i < 0, iteratedDeriv i f z₀ = 0
succ :
  ∀ (n : ℕ)
    (IH : ∀ {f : 𝕜 → E} (hf : AnalyticAt 𝕜 f z₀), (↑n : ℕ∞) ≤ analyticOrderAt f z₀ ↔ ∀ i < n, iteratedDeriv i f z₀ = 0)
    {f : 𝕜 → E} (hf : AnalyticAt 𝕜 f z₀), (↑(n + 1) : ℕ∞) ≤ analyticOrderAt f z₀ ↔ ∀ i < n + 1, iteratedDeriv i f z₀ = 0
⊢ (↑n : ℕ∞) ≤ analyticOrderAt f z₀ ↔ ∀ i < n, iteratedDeriv i f z₀ = 0

Tactic:
induction n generalizing f with
  | zero => simp
  | succ n IH =>
    by_cases hfz : f z₀ = 0; swap
    · simpa [analyticOrderAt_eq_zero.mpr (.inr hfz)] using ⟨0, by simp, by simpa⟩
    have : analyticOrderAt (deriv f) z₀ + 1 = analyticOrderAt f z₀ := by
      simpa [hfz] using hf.analyticOrderAt_deriv_add_one
    simp [← this, IH hf.deriv, iteratedDeriv_succ',
      -Order.lt_add_one_iff, Nat.forall_lt_succ_left, hfz]

Premises used: Nat.forall_lt_succ_left, iteratedDeriv_succ', Order.lt_add_one_iff
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CharZero 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
horder : analyticOrderAt f z₀ = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
have :
  ∀ (g : 𝕜 → E) (hg : AnalyticAt 𝕜 g z₀) (hg₀ : g z₀ ≠ 0)
    (hfg : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℕ) (z - z₀) ((fun (x1 x2 : ℕ) ↦ x1 + x2) n 1) • g z),
    analyticOrderAt (deriv f) z₀ = (↑n : ℕ∞)
⊢ analyticOrderAt (deriv f) z₀ = (↑n : ℕ∞)

Tactic:
have ⟨g, hg, hg₀, hfg⟩ := (AnalyticAt.analyticOrderAt_eq_natCast hf).1 horder
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CharZero 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
horder : analyticOrderAt f z₀ = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg₀ : g z₀ ≠ 0
hfg : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℕ) (z - z₀) ((fun (x1 x2 : ℕ) ↦ x1 + x2) n 1) • g z
⊢ f z₀ = 0

Tactic:
simpa [sub_self, zero_pow, zero_smul] using Filter.Eventually.self_of_nhds hfg

Premises used: Filter.Eventually.self_of_nhds, sub_self, zero_smul, zero_pow
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CharZero 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
horder : analyticOrderAt f z₀ = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg₀ : g z₀ ≠ 0
hfg : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℕ) (z - z₀) ((fun (x1 x2 : ℕ) ↦ x1 + x2) n 1) • g z
⊢ f z₀ = 0

Tactic:
have hz₀ : f z₀ = 0 := by
    simpa [sub_self, zero_pow, zero_smul] using Filter.Eventually.self_of_nhds hfg
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CharZero 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
horder : analyticOrderAt f z₀ = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg₀ : g z₀ ≠ 0
hfg : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℕ) (z - z₀) ((fun (x1 x2 : ℕ) ↦ x1 + x2) n 1) • g z
hz₀ : f z₀ = 0
⊢ analyticOrderAt (deriv f) z₀ = (↑n : ℕ∞)

Tactic:
simpa [hz₀, sub_zero, horder] using hf.analyticOrderAt_deriv_add_one

Premises used: sub_zero, AnalyticAt.analyticOrderAt_deriv_add_one
-- Module: Mathlib.Analysis.Analytic.Order
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 : ℕ
⊢ (↑n : ℕ∞) = analyticOrderAt f z₀ → n ≠ 0 → 0 ≤ n → analyticOrderAt (deriv^[0] f) z₀ = (↑(n - 0) : ℕ∞)

Tactic:
fun Hn Hpos Hk ↦ Hn.symm

Premises used: Nat.iterate, Eq.symm
-- Module: Mathlib.Analysis.Analytic.Order
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 : ℕ
⊢ (↑n : ℕ∞) = analyticOrderAt f z₀ → n ≠ 0 → 0 ≤ n → analyticOrderAt (deriv^[0] f) z₀ = (↑(n - 0) : ℕ∞)

Tactic:
exact fun Hn Hpos Hk ↦ Hn.symm
-- Module: Mathlib.Analysis.Analytic.Order
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
succ : analyticOrderAt ((deriv ∘ deriv^[n']) f) z₀ = (↑(n - (n' + 1)) : ℕ∞)
⊢ analyticOrderAt (deriv^[n' + 1] f) z₀ = (↑(n - (n' + 1)) : ℕ∞)

Tactic:
rw [Function.iterate_succ']

Premises used: Function.iterate_succ'
-- Module: Mathlib.Analysis.Analytic.Order
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

Tactic:
lia
-- Module: Mathlib.Analysis.Analytic.Order
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
refine : (↑(n - n') : ℕ∞) = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) (↑n'.succ : ℕ∞) + 1
⊢ analyticOrderAt (deriv^[n'] f) z₀ = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) (↑n'.succ : ℕ∞) + 1

Tactic:
refine (hk Hn Hpos (by lia)).trans ?_

Premises used: Eq.trans
-- Module: Mathlib.Analysis.Analytic.Order
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'.succ + 1 = n - n'

Tactic:
grind
-- Module: Mathlib.Analysis.Analytic.Order
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'.succ + 1 = n - n'

Tactic:
have : (n - n'.succ) + 1 = n - n' := by grind
-- Module: Mathlib.Analysis.Analytic.Order
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'
rw : (↑(n - n'.succ + 1) : ℕ∞) = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) (↑n'.succ : ℕ∞) + 1
⊢ (↑(n - n') : ℕ∞) = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) (↑n'.succ : ℕ∞) + 1

Tactic:
rw [← this]
-- Module: Mathlib.Analysis.Analytic.Order
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'.succ + 1) : ℕ∞) = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) (↑n'.succ : ℕ∞) + 1

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Order
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

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
-- Module: Mathlib.Analysis.Analytic.Order
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
horder : analyticOrderAt (deriv^[n'] f) z₀ = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) (↑n'.succ : ℕ∞) + 1
⊢ analyticOrderAt ((deriv ∘ deriv^[n']) f) z₀ = (↑(n - (n' + 1)) : ℕ∞)

Tactic:
simpa using (analyticOrderAt_deriv_of_pos (hf := AnalyticAt.iterated_deriv hf n')
      (n := n - n'.succ) horder)

Premises used: AnalyticAt.iterated_deriv, analyticOrderAt_deriv_of_pos
-- Module: Mathlib.Analysis.Analytic.Order
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) : ℕ∞)
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)) : ℕ∞)
⊢ (↑n : ℕ∞) = analyticOrderAt f z₀ → n ≠ 0 → k ≤ n → analyticOrderAt (deriv^[k] f) z₀ = (↑(n - k) : ℕ∞)

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)

Premises used: Function.iterate_succ'
-- Module: Mathlib.Analysis.Analytic.Order
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 : ℕ
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
⊢ ∃ (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']

Premises used: sub_eq_iff_eq_add'
-- Module: Mathlib.Analysis.Analytic.Order
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

Tactic:
Finset.analyticAt_fun_sum _ fun i hi ↦ ?_

Premises used: Finset.analyticAt_fun_sum
-- Module: Mathlib.Analysis.Analytic.Order
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 : ℕ
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
⊢ 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:
refine Finset.analyticAt_fun_sum _ fun i hi ↦ ?_

Premises used: Finset.analyticAt_fun_sum
-- Module: Mathlib.Analysis.Analytic.Order
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 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:
fun_prop
-- Module: Mathlib.Analysis.Analytic.Order
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

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
-- Module: Mathlib.Analysis.Analytic.Order
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
⊢ ∃ (g : 𝕜 → E),
    AnalyticAt 𝕜 g 0 ∧
      ∀ᶠ (z : 𝕜) in 𝓝 0,
        f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0 = (z - 0) ^ n • g z

Tactic:
(natCast_le_analyticOrderAt (hf.fun_sub this)).mp ?_

Premises used: natCast_le_analyticOrderAt, Iff.mp, AnalyticAt.fun_sub
-- Module: Mathlib.Analysis.Analytic.Order
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
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
⊢ ∃ (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:
convert! (natCast_le_analyticOrderAt (hf.fun_sub this)).mp ?_

Premises used: natCast_le_analyticOrderAt, Iff.mp, AnalyticAt.fun_sub
-- Module: Mathlib.Analysis.Analytic.Order
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
x : 𝕜 → E
x_1 : 𝕜
⊢ x_1 = x_1 - 0

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Order
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
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
⊢ (↑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:
rw [natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero (hf.fun_sub this)]

Premises used: AnalyticAt.fun_sub, natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero
-- Module: Mathlib.Analysis.Analytic.Order
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
⊢ AnalyticAt 𝕜 f 0

Tactic:
fun_prop