awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
⊢ 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
have 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
Tactic: split_ifs with h
-- 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
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
⊢ 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
have neg : ∀ (h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0),
  LE.le (α := ℕ∞) (↑n : ℕ∞)
      (↑(sorry.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: split_ifs with h
-- 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
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)
⊢ 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
have neg : ∀ (g : 𝕜 → E) (hg : AnalyticAt 𝕜 g z₀) (hg_ne : g z₀ ≠ 0)
  (hm :
    ∀ᶠ (z : 𝕜) in 𝓝 z₀,
      f z =
        (z - z₀) ^
            sorry.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 : ℕ∞)
      (↑(sorry.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
-- 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
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
⊢ 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
have neg : n ≤
    sorry.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]
-- 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
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
⊢ 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
have neg : ∀
  (hmn :
    n ≤
      sorry.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 = HSMul.hSMul (β := E) ((z - z₀) ^ n) ((fun (z : 𝕜) ↦ (z - z₀) ^ (m - n) • g z) z)
Tactic: refine ⟨fun hmn ↦ ⟨fun z ↦ (z - z₀) ^ (m - n) • g z, by fun_prop, ?_⟩, fun ⟨h, hh, hfh⟩ ↦ ?_⟩
-- 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
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 :
  ∀
    (hmn :
      n ≤
        ⋯.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 = HSMul.hSMul (β := E) ((z - z₀) ^ n) ((fun (z : 𝕜) ↦ (z - z₀) ^ (m - n) • g z) z)
⊢ 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
have neg₁ : (∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) →
  ∀ (h_1 : 𝕜 → E) (hh : AnalyticAt 𝕜 h_1 z₀) (hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h_1 z),
    n ≤
      sorry.choose (p := fun (n : ℕ) ↦
        ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
Tactic: refine ⟨fun hmn ↦ ⟨fun z ↦ (z - z₀) ^ (m - n) • g z, by fun_prop, ?_⟩, fun ⟨h, hh, hfh⟩ ↦ ?_⟩
-- 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
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)
z : 𝕜
hz :
  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
⊢ f z = (z - z₀) ^ n • (z - z₀) ^ (m - n) • g z
have rwa : f z = ((z - z₀) ^ n * (z - z₀) ^ (m - n)) • g z
Tactic: rwa [← mul_smul, ← pow_add, Nat.add_sub_of_le hmn]
-- 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
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)
z : 𝕜
hz :
  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
rwa : f z = ((z - z₀) ^ n * (z - z₀) ^ (m - n)) • g z
⊢ f z = (z - z₀) ^ n • (z - z₀) ^ (m - n) • g z
have rwa₁ : f z = (z - z₀) ^ (n + (m - n)) • g z
Tactic: rwa [← mul_smul, ← pow_add, Nat.add_sub_of_le hmn]
-- 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
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)
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HSMul.hSMul (β := E) ((z - z₀) ^ n) ((fun (z : 𝕜) ↦ (z - z₀) ^ (m - n) • g z) z)
have h₁ : ∀ (a : 𝕜),
  Membership.mem (γ := Set 𝕜)
    {x : 𝕜 |
      Membership.mem (γ := Set 𝕜)
          {x : 𝕜 |
            (fun (z : 𝕜) ↦
                f z =
                  (z - z₀) ^
                      sorry.choose (p := fun (n : ℕ) ↦
                        ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
                    g z)
              x}
          x →
        Membership.mem (γ := Set 𝕜)
          {x : 𝕜 |
            (fun (z : 𝕜) ↦ f z = HSMul.hSMul (β := E) ((z - z₀) ^ n) ((fun (z : 𝕜) ↦ (z - z₀) ^ (m - n) • g z) z)) x}
          x}
    a
Tactic: filter_upwards [hm] with z hz using by rwa [← mul_smul, ← pow_add, Nat.add_sub_of_le hmn]
-- 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
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)
h₁ :
  ∀ (a : 𝕜),
    Membership.mem (γ := Set 𝕜)
      {x : 𝕜 |
        Membership.mem (γ := Set 𝕜)
            {x : 𝕜 |
              (fun (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)
                x}
            x →
          Membership.mem (γ := Set 𝕜)
            {x : 𝕜 |
              (fun (z : 𝕜) ↦ f z = HSMul.hSMul (β := E) ((z - z₀) ^ n) ((fun (z : 𝕜) ↦ (z - z₀) ^ (m - n) • g z) z)) x}
            x}
      a
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HSMul.hSMul (β := E) ((z - z₀) ^ n) ((fun (z : 𝕜) ↦ (z - z₀) ^ (m - n) • g z) z)
have h₂ : ∀ (a : 𝕜),
  f a =
      (a - z₀) ^
          sorry.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
        g a →
    f a = (a - z₀) ^ n • (a - z₀) ^ (m - n) • g a
Tactic: filter_upwards [hm] with z hz using by rwa [← mul_smul, ← pow_add, Nat.add_sub_of_le hmn]
-- 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
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h_1 : ¬∀ᶠ (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
h_2 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
⊢ n ≤
    ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z)
have neg : ∀
  (hg_ne :
    sorry.choose (p := fun (n : ℕ) ↦
        ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) <
      n),
  g z₀ = 0
Tactic: contrapose! hg_ne
Cleared hypotheses: hg_ne
-- 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
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h_1 : ¬∀ᶠ (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₀
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
h_2 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne :
  ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) <
    n
⊢ g z₀ = 0
have this : ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z) z₀
Tactic: have : ContinuousAt (fun z ↦ (z - z₀) ^ (n - m) • h z) z₀ := by 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
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h_1 : ¬∀ᶠ (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₀
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
h_2 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne :
  ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) <
    n
this : ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z) z₀
⊢ g z₀ = 0
have neg : Eq.{u_2 + 1} (α := E) ((fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z) z₀) 0
Tactic: rw [tendsto_nhds_unique_of_eventuallyEq (l := 𝓝[≠] z₀)
        hg.continuousAt.continuousWithinAt this.continuousWithinAt ?_]
-- 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
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h_1 : ¬∀ᶠ (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₀
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
h_2 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne :
  ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) <
    n
this : ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z) z₀
neg : Eq.{u_2 + 1} (α := E) ((fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z) z₀) 0
⊢ g z₀ = 0
have rw : g =ᶠ[𝓝[≠] z₀] fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z
Tactic: rw [tendsto_nhds_unique_of_eventuallyEq (l := 𝓝[≠] z₀)
        hg.continuousAt.continuousWithinAt this.continuousWithinAt ?_]
-- 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
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h_1 : ¬∀ᶠ (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₀
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
h_2 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne :
  ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) <
    n
this : ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z) z₀
⊢ g =ᶠ[𝓝[≠] z₀] fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z
have h₁ : ∀ (z : 𝕜) (hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z)
  (hf' :
    f z =
      (z - z₀) ^
          sorry.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) •
        g z)
  (hf'' : f z = (z - z₀) ^ n • h z), g z = (z - z₀) ^ (n - m) • h z
Tactic: filter_upwards [self_mem_nhdsWithin, hm.filter_mono nhdsWithin_le_nhds,
          hfh.filter_mono nhdsWithin_le_nhds] with z hz hf' hf''
-- 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
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h_1 : ¬∀ᶠ (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₀
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
h_2 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne :
  ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) <
    n
this : ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z) z₀
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z
hf' :
  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
hf'' : f z = (z - z₀) ^ n • h z
⊢ g z = (z - z₀) ^ (n - m) • h z
have hf'₁ : ((z - z₀) ^ n *
      ((z - z₀) ^
          sorry.choose (p := fun (n : ℕ) ↦
            ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z))⁻¹) •
    h z =
  g z
Tactic: rw [← inv_smul_eq_iff₀ (pow_ne_zero _ <| sub_ne_zero_of_ne hz), hf'', smul_comm,
          ← mul_smul] at hf'
Cleared hypotheses: hf', 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
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h_1 : ¬∀ᶠ (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₀
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
h_2 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne :
  ⋯.choose (p := fun (n : ℕ) ↦
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) <
    n
this : ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (n - m) • h z) z₀
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z
hf' :
  ((z - z₀) ^ n *
        ((z - z₀) ^
            ⋯.choose (p := fun (n : ℕ) ↦
              ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z))⁻¹) •
      h z =
    g z
hf'' : f z = (z - z₀) ^ n • h z
⊢ g z = (z - z₀) ^ (n - m) • h z
have h₁ : g z = ((z - z₀) ^ n * ((z - z₀) ^ m)⁻¹) • h z
Tactic: rw [pow_sub₀ _ (sub_ne_zero_of_ne hz) (by lia), ← hf']