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
z₀ : 𝕜
hf :
  Eq (α := ℕ∞)
    (if hf : AnalyticAt 𝕜 f z₀ then
      if h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0 then ⊤
      else
        (↑(⋯.choose (p := fun (n : ℕ) ↦
              ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
          ℕ∞)
    else 0)
    ⊤
pos : ∀ (h : AnalyticAt 𝕜 f z₀), (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) → ∀ (hf : Eq (α := ℕ∞) ⊤ ⊤), ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
neg :
  ∀ (h : AnalyticAt 𝕜 f z₀) (h_1 : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0)
    (hf :
      Eq (α := ℕ∞)
        (↑(⋯.choose (p := fun (n : ℕ) ↦
              ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
          ℕ∞)
        ⊤),
    ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
neg₁ : ∀ (h : ¬AnalyticAt 𝕜 f z₀) (hf : Eq (α := ℕ∞) 0 ⊤), ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

Tactic:
split_ifs at hf with h
-- 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
z₀ : 𝕜
h : AnalyticAt 𝕜 f z₀
h_1 : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
hf : Eq (α := ℕ∞) ⊤ ⊤
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

Tactic:
simp [*] at *
-- 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
z₀ : 𝕜
h : AnalyticAt 𝕜 f z₀
h_1 : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
hf :
  Eq (α := ℕ∞)
    (↑(⋯.choose (p := fun (n : ℕ) ↦
          ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
      ℕ∞)
    ⊤
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

Tactic:
simp [*] at *
-- 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
z₀ : 𝕜
h : ¬AnalyticAt 𝕜 f z₀
hf : Eq (α := ℕ∞) 0 ⊤
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

Tactic:
simp [*] at *
-- 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
z₀ : 𝕜
hf : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ Eq (α := ℕ∞)
    (if hf : AnalyticAt 𝕜 f z₀ then
      if h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0 then ⊤
      else
        (↑(⋯.choose (p := fun (n : ℕ) ↦
              ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
          ℕ∞)
    else 0)
    ⊤

Tactic:
simp [hf, analyticAt_congr hf, analyticAt_const]

Premises used: analyticAt_const, 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
f : 𝕜 → E
z₀ : 𝕜
⊢ EventuallyConst f (𝓝 z₀) ↔ analyticOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ f x - f z₀) z₀ = ⊤

Tactic:
simpa [eventuallyConst_iff_exists_eventuallyEq, analyticOrderAt_eq_top, sub_eq_zero]
    using ⟨fun ⟨c, hc⟩ ↦ (show f z₀ = c from hc.self_of_nhds) ▸ hc, fun h ↦ ⟨_, h⟩⟩

Premises used: analyticOrderAt_eq_top, sub_eq_zero, Filter.eventuallyConst_iff_exists_eventuallyEq
-- 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₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
pos :
  ∀ (h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0),
    Eq (α := ℕ∞) ⊤ (↑n : ℕ∞) ↔
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
neg :
  ∀ (h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0),
    Eq (α := ℕ∞)
        (↑(⋯.choose (p := fun (n : ℕ) ↦
              ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
          ℕ∞)
        (↑n : ℕ∞) ↔
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ Eq (α := ℕ∞)
      (if hf : AnalyticAt 𝕜 f z₀ then
        if h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0 then ⊤
        else
          (↑(⋯.choose (p := fun (n : ℕ) ↦
                ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
            ℕ∞)
      else 0)
      (↑n : ℕ∞) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
split_ifs with h
-- 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₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
pos : ¬∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ Eq (α := ℕ∞) ⊤ (↑n : ℕ∞) ↔ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
simp only [ENat.top_ne_coe, false_iff]

Premises used: false_iff, ENat.top_ne_coe
-- 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₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
pos :
  ∀ (h : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z),
    ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ¬∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
contrapose h
-- 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₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
pos : ∃ (n : ℕ) (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

Tactic:
rw [← hf.exists_eventuallyEq_pow_smul_nonzero_iff]

Premises used: AnalyticAt.exists_eventuallyEq_pow_smul_nonzero_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₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ ∃ (n : ℕ) (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
⟨n, h⟩

Premises used: Exists.intro
-- 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₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ ∃ (n : ℕ) (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
exact ⟨n, h⟩
-- 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₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ∃ (n : ℕ) (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
rw [← hf.exists_eventuallyEq_pow_smul_nonzero_iff] at h

Premises used: AnalyticAt.exists_eventuallyEq_pow_smul_nonzero_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₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h_1 : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
h : ∃ (n : ℕ) (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ Eq (α := ℕ∞)
      (↑(⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
        ℕ∞)
      (↑n : ℕ∞) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
⟨fun hn ↦ (WithTop.coe_inj.mp hn : h.choose = n) ▸ h.choose_spec, fun h' ↦ ?_⟩

Premises used: WithTop.coe_inj, Exists.choose_spec, Eq.rec, Iff.intro, Iff.mp
-- 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₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h_1 : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
h : ∃ (n : ℕ) (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
neg :
  ∀ (h' : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z),
    Eq (α := ℕ∞)
      (↑(⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
        ℕ∞)
      (↑n : ℕ∞)
⊢ Eq (α := ℕ∞)
      (↑(⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
        ℕ∞)
      (↑n : ℕ∞) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
refine ⟨fun hn ↦ (WithTop.coe_inj.mp hn : h.choose = n) ▸ h.choose_spec, fun h' ↦ ?_⟩
-- 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₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h_1 : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
h : ∃ (n : ℕ) (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h' : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
neg neg₁ : Eq (α := ℕ∞) (↑n : ℕ∞) (↑n : ℕ∞)
⊢ Eq (α := ℕ∞)
    (↑(⋯.choose (p := fun (n : ℕ) ↦
          ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
      ℕ∞)
    (↑n : ℕ∞)

Tactic:
rw [AnalyticAt.unique_eventuallyEq_pow_smul_nonzero h.choose_spec h']

Premises used: AnalyticAt.unique_eventuallyEq_pow_smul_nonzero, Exists.choose_spec
-- 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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hf' : analyticOrderAt f z₀ ≠ ⊤
n : ℕ
⊢ analyticOrderNatAt f z₀ = n ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
simp [← Nat.cast_inj (R := ℕ∞), Nat.cast_analyticOrderNatAt hf', hf.analyticOrderAt_eq_natCast]

Premises used: Nat.cast_analyticOrderNatAt, Nat.cast_inj, AnalyticAt.analyticOrderAt_eq_natCast
-- 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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt f z₀ ≠ ⊤ ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ f =ᶠ[𝓝 z₀] fun (z : 𝕜) ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • g z

Tactic:
simp only [← ENat.coe_toNat_eq_self, Eq.comm, EventuallyEq, ← hf.analyticOrderAt_eq_natCast,
    analyticOrderNatAt]

Premises used: analyticOrderNatAt, Filter.EventuallyEq, AnalyticAt.analyticOrderAt_eq_natCast, ENat.coe_toNat_eq_self, Eq.comm
-- 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
z₀ : 𝕜
pos : ∀ (hf : AnalyticAt 𝕜 f z₀), analyticOrderAt f z₀ = 0 ↔ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0
neg : ∀ (hf : ¬AnalyticAt 𝕜 f z₀), analyticOrderAt f z₀ = 0 ↔ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0
⊢ analyticOrderAt f z₀ = 0 ↔ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0

Tactic:
by_cases hf : AnalyticAt 𝕜 f z₀

Premises used: AnalyticAt
-- 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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
pos :
  (∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℕ) (z - z₀) 0 • g z) ↔
    ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0
⊢ analyticOrderAt f z₀ = 0 ↔ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0

Tactic:
rw [← ENat.coe_zero, hf.analyticOrderAt_eq_natCast]

Premises used: AnalyticAt.analyticOrderAt_eq_natCast, ENat.coe_zero
-- 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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
pos :
  (∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℕ) (z - z₀) 0 • g z) →
    ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0
pos₁ :
  ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0 →
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℕ) (z - z₀) 0 • g z
⊢ (∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℕ) (z - z₀) 0 • g z) ↔
    ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0

Tactic:
constructor
-- 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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
g : 𝕜 → E
left : AnalyticAt 𝕜 g z₀
left_1 : g z₀ ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℕ) (z - z₀) 0 • g z
⊢ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0

Tactic:
simpa [hf, hg.self_of_nhds]

Premises used: Filter.Eventually.self_of_nhds
-- 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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hz : ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℕ) (z - z₀) 0 • f z

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
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0 →
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℕ) (z - z₀) 0 • g z

Tactic:
exact fun hz ↦ ⟨f, hf, hz.resolve_left <| not_not_intro hf, by simp⟩
-- 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
z₀ : 𝕜
hf : ¬AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt f z₀ = 0 ↔ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0

Tactic:
simp [hf]
-- 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
z₀ : 𝕜
⊢ analyticOrderAt f z₀ ≠ 0 ↔ AnalyticAt 𝕜 f z₀ ∧ f z₀ = 0

Tactic:
simp [analyticOrderAt_eq_zero]

Premises used: analyticOrderAt_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
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt f z₀ = 0 ↔ f z₀ ≠ 0

Tactic:
simp [hf, analyticOrderAt_eq_zero]

Premises used: analyticOrderAt_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
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt f z₀ ≠ 0 ↔ f z₀ = 0

Tactic:
hf.analyticOrderAt_eq_zero.not_left

Premises used: Iff.not_left, AnalyticAt.analyticOrderAt_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
f : 𝕜 → E
z₀ : 𝕜
hf : analyticOrderAt f z₀ ≠ 0
pos : ∀ (hf' : AnalyticAt 𝕜 f z₀), f z₀ = 0
neg : ∀ (hf' : ¬AnalyticAt 𝕜 f z₀), f z₀ = 0
⊢ f z₀ = 0

Tactic:
by_cases hf' : AnalyticAt 𝕜 f z₀

Premises used: AnalyticAt
-- 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
z₀ : 𝕜
hf : analyticOrderAt f z₀ ≠ 0
hf' : AnalyticAt 𝕜 f z₀
⊢ f z₀ = 0

Tactic:
simp_all [analyticOrderAt_eq_zero]

Premises used: analyticOrderAt_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
f : 𝕜 → E
z₀ : 𝕜
hf : analyticOrderAt f z₀ ≠ 0
hf' : ¬AnalyticAt 𝕜 f z₀
⊢ f z₀ = 0

Tactic:
simp_all [analyticOrderAt_eq_zero]

Premises used: analyticOrderAt_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
f : 𝕜 → E
z₀ : 𝕜
hf : analyticOrderNatAt f z₀ ≠ 0
pos : ∀ (hf' : AnalyticAt 𝕜 f z₀), f z₀ = 0
neg : ∀ (hf' : ¬AnalyticAt 𝕜 f z₀), f z₀ = 0
⊢ f z₀ = 0

Tactic:
by_cases hf' : AnalyticAt 𝕜 f z₀

Premises used: AnalyticAt
-- 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
z₀ : 𝕜
hf : analyticOrderNatAt f z₀ ≠ 0
hf' : AnalyticAt 𝕜 f z₀
⊢ f z₀ = 0

Tactic:
simp_all [analyticOrderNatAt, analyticOrderAt_eq_zero]

Premises used: analyticOrderNatAt, analyticOrderAt_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
f : 𝕜 → E
z₀ : 𝕜
hf : analyticOrderNatAt f z₀ ≠ 0
hf' : ¬AnalyticAt 𝕜 f z₀
⊢ f z₀ = 0

Tactic:
simp_all [analyticOrderNatAt, analyticOrderAt_eq_zero]

Premises used: analyticOrderNatAt, analyticOrderAt_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
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
pos :
  ∀ (h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0),
    LE.le (α := ℕ∞) (↑n : ℕ∞) ⊤ ↔ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
neg :
  ∀ (h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0),
    LE.le (α := ℕ∞) (↑n : ℕ∞)
        (↑(⋯.choose (p := fun (n : ℕ) ↦
              ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
          ℕ∞) ↔
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ LE.le (α := ℕ∞) (↑n : ℕ∞)
      (if hf : AnalyticAt 𝕜 f z₀ then
        if h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0 then ⊤
        else
          (↑(⋯.choose (p := fun (n : ℕ) ↦
                ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
            ℕ∞)
      else 0) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
split_ifs with h
-- 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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HSMul.hSMul (β := E) ((z - z₀) ^ n) (0 z)

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
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ LE.le (α := ℕ∞) (↑n : ℕ∞) ⊤ ↔ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
simpa using ⟨0, analyticAt_const .., by simpa⟩
-- 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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ :=
  ⋯.choose (p := fun (n : ℕ) ↦
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
neg :
  ∀ (g : 𝕜 → E) (hg : AnalyticAt 𝕜 g z₀) (hg_ne : g z₀ ≠ 0)
    (hm :
      ∀ᶠ (z : 𝕜) in 𝓝 z₀,
        f z =
          (z - z₀) ^
              ⋯.choose (p := fun (n : ℕ) ↦
                ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
            g z),
    LE.le (α := ℕ∞) (↑n : ℕ∞)
        (↑(⋯.choose (p := fun (n : ℕ) ↦
              ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
          ℕ∞) ↔
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ LE.le (α := ℕ∞) (↑n : ℕ∞)
      (↑(⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
        ℕ∞) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
obtain ⟨g, hg, hg_ne, hm⟩ := (hf.exists_eventuallyEq_pow_smul_nonzero_iff.mpr h).choose_spec

Premises used: Iff.mpr, Exists.choose_spec, AnalyticAt.exists_eventuallyEq_pow_smul_nonzero_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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ :=
  ⋯.choose (p := fun (n : ℕ) ↦
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg_ne : g z₀ ≠ 0
hm :
  ∀ᶠ (z : 𝕜) in 𝓝 z₀,
    f z =
      (z - z₀) ^
          ⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
        g z
neg :
  n ≤
      ⋯.choose (p := fun (n : ℕ) ↦
        ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ LE.le (α := ℕ∞) (↑n : ℕ∞)
      (↑(⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)) :
        ℕ∞) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
rw [ENat.coe_le_coe]

Premises used: ENat.coe_le_coe
-- 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
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ :=
  ⋯.choose (p := fun (n : ℕ) ↦
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg_ne : g z₀ ≠ 0
hm :
  ∀ᶠ (z : 𝕜) in 𝓝 z₀,
    f z =
      (z - z₀) ^
          ⋯.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
        g z
hmn :
  n ≤
    ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
⊢ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (m - n) • g z) z₀

Tactic:
fun_prop