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
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
convert_2 :
  iteratedDeriv i f 0 -
      iteratedDeriv i (fun (z : 𝕜) ↦ ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0) 0 =
    0
⊢ 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 [iteratedDeriv_fun_sub (AnalyticAt.contDiffAt <| by fun_prop) this.contDiffAt]

Premises used: AnalyticAt.contDiffAt, iteratedDeriv_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
i : ℕ
hi : i < n
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
⊢ iteratedDeriv i f 0 -
      iteratedDeriv i (fun (z : 𝕜) ↦ ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0) 0 =
    0

Tactic:
simp (disch := fun_prop) only [iteratedDeriv_fun_sum, iteratedDeriv_smul_const,
      iteratedDeriv_div_const, iteratedDeriv_fun_pow_zero]

Premises used: iteratedDeriv_fun_sum, iteratedDeriv_div_const, iteratedDeriv_smul_const, iteratedDeriv_fun_pow_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
⊢ 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 [ite_div, Finset.sum_ite_eq_of_mem _ _ _ (Finset.mem_range.mpr hi)]

Premises used: Iff.mpr, ite_div, Finset.mem_range, Finset.sum_ite_eq_of_mem
-- 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 : ℕ
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
⊢ ∃ (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

Premises used: AnalyticAt.exists_eventuallyEq_sum_add_pow_mul
-- 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 : ℕ
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
rwa rwa₁ rwa₂ 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
⊢ ∃ (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

Premises used: Filter.eventually_iff_exists_mem
-- 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 : ℕ
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
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
⊢ ∃ (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
-- 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 : ℕ
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

Tactic:
⟨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 ↦ ?_⟩

Premises used: HSub.hSub, Membership.mem, HDiv.hDiv, Nat.cast, Finset.range, Inv.inv, HPow.hPow, Nat.factorial, And.intro, Exists.intro, HSMul.hSMul, iteratedDeriv, OfNat.ofNat, Finset.sum, ite
-- 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 : ℕ
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
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)
⊢ ∃ (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:
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 ↦ ?_⟩
-- 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 : ℕ
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
⊢ ∀ 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:
simp +contextual
-- 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 : ℕ
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
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)
⊢ 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)

Tactic:
filter_upwards [hU0] using by simp +contextual
-- 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 : ℕ
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
⊢ 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:
exact hFa.congr (by filter_upwards [hU0] using by simp +contextual)

Premises used: AnalyticAt.congr
-- 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 : ℕ
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)
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)
⊢ 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
-- 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 : ℕ
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)

Tactic:
simpa [hz] using hU' z hz
-- 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 : ℕ
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
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)
⊢ 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:
simp only [if_neg hz]

Premises used: if_neg
-- 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 : ℕ
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
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)
neg₁ : z ^ n ≠ 0
⊢ 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:
rw [smul_inv_smul₀]

Premises used: smul_inv_smul₀
-- 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 : ℕ
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 +
      (f z - ∑ i ∈ Finset.range n, (z ^ i / (↑i.factorial : 𝕜)) • iteratedDeriv i f 0)

Tactic:
module
-- 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 : ℕ
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
neg : ∀ (hz : z ^ n = 0), z ∈ U
⊢ z ^ n ≠ 0

Tactic:
contrapose hz
-- 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 : ℕ
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 ^ n = 0
⊢ z ∈ U

Tactic:
(pow_eq_zero_iff'.mp hz).1 ▸ mem_of_mem_nhds hU0

Premises used: pow_eq_zero_iff', Eq.rec, mem_of_mem_nhds, And.left, Iff.mp, Eq.symm
-- 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 : ℕ
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 ^ n = 0
⊢ z ∈ U

Tactic:
exact (pow_eq_zero_iff'.mp hz).1 ▸ mem_of_mem_nhds hU0
-- 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 : ℕ
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
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)
    (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
refine_1 :
  ∀ (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),
    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
refine_2 refine_2₁ :
  ∀ (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)
⊢ ∃ (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:
classical
  obtain ⟨F, hFa, hF⟩ := hf.exists_eventuallyEq_sum_add_pow_mul n
  obtain ⟨U, hU0, hU'⟩ := by rwa [eventually_iff_exists_mem] at hF
  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 ↦ ?_⟩
  · exact hFa.congr (by filter_upwards [hU0] using by simp +contextual)
  · by_cases hz : z ∈ U
    · simpa [hz] using hU' z hz
    · simp only [if_neg hz]
      rw [smul_inv_smul₀]
      · module
      · contrapose hz
        exact (pow_eq_zero_iff'.mp hz).1 ▸ mem_of_mem_nhds hU0

Premises used: AnalyticAt.exists_eventuallyEq_sum_add_pow_mul, smul_inv_smul₀
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z₀ : 𝕜
n : ℕ
⊢ AnalyticAt 𝕜 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - z₀) n) z₀

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z₀ : 𝕜
n : ℕ
rw :
  ∃ (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g z₀ ∧
      g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - z₀) n z = (z - z₀) ^ n • g z
⊢ analyticOrderAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - z₀) n) z₀ = (↑n : ℕ∞)

Tactic:
rw [AnalyticAt.analyticOrderAt_eq_natCast (by fun_prop)]

Premises used: AnalyticAt.analyticOrderAt_eq_natCast
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z₀ : 𝕜
n : ℕ
⊢ AnalyticAt 𝕜 (F := 𝕜) 1 z₀ ∧
    Ne.{u_1 + 1} (α := 𝕜) (1 z₀) 0 ∧
      ∀ᶠ (z : 𝕜) in 𝓝 z₀, HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - z₀) n z = HSMul.hSMul (β := 𝕜) ((z - z₀) ^ n) (1 z)

Tactic:
simp [Pi.one_def, analyticAt_const]

Premises used: analyticAt_const, Pi.one_def
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z₀ : 𝕜
n : ℕ
⊢ ∃ (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g z₀ ∧
      g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - z₀) n z = (z - z₀) ^ n • g z

Tactic:
exact ⟨1, by simp [Pi.one_def, analyticAt_const]⟩
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
z₀ : 𝕜
hf : analyticOrderAt f z₀ = ⊤
⊢ analyticOrderAt (f * g) z₀ = ⊤

Tactic:
analyticOrderAt_smul_eq_top_of_left hf

Premises used: analyticOrderAt_smul_eq_top_of_left
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
z₀ : 𝕜
hg : analyticOrderAt g z₀ = ⊤
⊢ analyticOrderAt (f * g) z₀ = ⊤

Tactic:
analyticOrderAt_smul_eq_top_of_right hg

Premises used: analyticOrderAt_smul_eq_top_of_right
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
⊢ analyticOrderAt (f * g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀

Tactic:
analyticOrderAt_smul hf hg

Premises used: analyticOrderAt_smul
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
hf' : analyticOrderAt f z₀ ≠ ⊤
hg' : analyticOrderAt g z₀ ≠ ⊤
⊢ analyticOrderNatAt (f * g) z₀ = analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀

Tactic:
simp [analyticOrderNatAt, analyticOrderAt_mul, ENat.toNat_add, *]

Premises used: analyticOrderNatAt, analyticOrderAt_mul, ENat.toNat_add