awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
m : ℕ
hm :
  (↑m : ℕ∞) =
    analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ ∃ᶠ (z : 𝕜) in 𝓝[≠] x,
    (z - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f z =
      0
have neg : ∀ᶠ (x_1 : 𝕜) in 𝓝[≠] x,
  (x_1 - x) ^
        Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
          hf •
      f x_1 =
    0
Tactic: apply Eventually.frequently
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
m : ℕ
hm :
  (↑m : ℕ∞) =
    analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[≠] x,
    (x_1 - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f x_1 =
      0
have h₁ : ∀ (z : 𝕜) (hfz : f z = 0),
  (z - x) ^
        Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
          hf •
      f z =
    0
Tactic: filter_upwards [h] with z hfz
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
m : ℕ
hm :
  (↑m : ℕ∞) =
    analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
z : 𝕜
hfz : f z = 0
⊢ (z - x) ^
        Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
          hf •
      f z =
    0
have h₁ : HSMul.hSMul (β := E)
    ((z - x) ^
      Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf)
    0 =
  0
Tactic: rw [hfz, smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
m : ℕ
hm :
  (↑m : ℕ∞) =
    analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
z : 𝕜
hfz : f z = 0
h₁ :
  HSMul.hSMul (β := E)
      ((z - x) ^
        Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf)
      0 =
    0
⊢ (z - x) ^
        Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
          hf •
      f z =
    0
have h₂ : Eq.{u_2 + 1} (α := E) 0 0
Tactic: rw [hfz, smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
⊢ meromorphicOrderAt f x = (↑n : WithTop ℤ) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
have simp : HSub.hSub (α := WithTop ℤ)
      (ENat.map (fun (x : ℕ) ↦ (↑x : ℤ))
        (analyticOrderAt.{u_1, u_2} (E := E)
          (fun (z : 𝕜) ↦
            (z - x) ^
                Exists.choose (p := fun (n : ℕ) ↦
                  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) sorry •
              f z)
          x))
      (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            sorry) :
        WithTop ℤ) =
    (↑n : WithTop ℤ) ↔
  ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
Tactic: simp only [meromorphicOrderAt, hf, ↓reduceDIte]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
⊢ HSub.hSub (α := WithTop ℤ)
        (ENat.map (fun (x : ℕ) ↦ (↑x : ℤ))
          (analyticOrderAt.{u_1, u_2} (E := E)
            (fun (z : 𝕜) ↦
              (z - x) ^
                  Exists.choose (p := fun (n : ℕ) ↦
                    AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) ⋯ •
                f z)
            x))
        (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              ⋯) :
          WithTop ℤ) =
      (↑n : WithTop ℤ) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
have pos : ∀
  (h :
    analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
            f z)
        x =
      ⊤),
  HSub.hSub (α := WithTop ℤ)
        (ENat.map (fun (x : ℕ) ↦ (↑x : ℤ))
          (analyticOrderAt.{u_1, u_2} (E := E)
            (fun (z : 𝕜) ↦
              (z - x) ^
                  Exists.choose (p := fun (n : ℕ) ↦
                    AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) sorry •
                f z)
            x))
        (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              sorry) :
          WithTop ℤ) =
      (↑n : WithTop ℤ) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
Tactic: by_cases h : analyticOrderAt (fun z ↦ (z - x) ^ hf.choose • f z) x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
pos :
  ∀
    (h :
      analyticOrderAt.{u_1, u_2} (E := E)
          (fun (z : 𝕜) ↦
            (z - x) ^
                Exists.choose (p := fun (n : ℕ) ↦
                  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
              f z)
          x =
        ⊤),
    HSub.hSub (α := WithTop ℤ)
          (ENat.map (fun (x : ℕ) ↦ (↑x : ℤ))
            (analyticOrderAt.{u_1, u_2} (E := E)
              (fun (z : 𝕜) ↦
                (z - x) ^
                    Exists.choose (p := fun (n : ℕ) ↦
                      AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) ⋯ •
                  f z)
              x))
          (↑(Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) ⋯) :
            WithTop ℤ) =
        (↑n : WithTop ℤ) ↔
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ HSub.hSub (α := WithTop ℤ)
        (ENat.map (fun (x : ℕ) ↦ (↑x : ℤ))
          (analyticOrderAt.{u_1, u_2} (E := E)
            (fun (z : 𝕜) ↦
              (z - x) ^
                  Exists.choose (p := fun (n : ℕ) ↦
                    AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) ⋯ •
                f z)
            x))
        (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              ⋯) :
          WithTop ℤ) =
      (↑n : WithTop ℤ) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
have neg : ∀
  (h :
    ¬analyticOrderAt.{u_1, u_2} (E := E)
          (fun (z : 𝕜) ↦
            (z - x) ^
                Exists.choose (p := fun (n : ℕ) ↦
                  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
              f z)
          x =
        ⊤),
  HSub.hSub (α := WithTop ℤ)
        (ENat.map (fun (x : ℕ) ↦ (↑x : ℤ))
          (analyticOrderAt.{u_1, u_2} (E := E)
            (fun (z : 𝕜) ↦
              (z - x) ^
                  Exists.choose (p := fun (n : ℕ) ↦
                    AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) sorry •
                f z)
            x))
        (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              sorry) :
          WithTop ℤ) =
      (↑n : WithTop ℤ) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
Tactic: by_cases h : analyticOrderAt (fun z ↦ (z - x) ^ hf.choose • f z) x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h :
  analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x =
    ⊤
⊢ HSub.hSub (α := WithTop ℤ)
        (ENat.map (fun (x : ℕ) ↦ (↑x : ℤ))
          (analyticOrderAt.{u_1, u_2} (E := E)
            (fun (z : 𝕜) ↦
              (z - x) ^
                  Exists.choose (p := fun (n : ℕ) ↦
                    AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) ⋯ •
                f z)
            x))
        (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              ⋯) :
          WithTop ℤ) =
      (↑n : WithTop ℤ) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
have pos : ¬∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
Tactic: rw [h, ENat.map_top, ← WithTop.coe_natCast, top_sub,
      eq_false_intro WithTop.top_ne_coe, false_iff]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h :
  analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x =
    ⊤
⊢ ¬∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
have h₁ : ∀ᶠ (z : 𝕜) in 𝓝 x,
  (z - x) ^
        Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
          hf •
      f z =
    0
Tactic: rw [analyticOrderAt_eq_top] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h :
  ∀ᶠ (z : 𝕜) in 𝓝 x,
    (z - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f z =
      0
⊢ ¬∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
have pos : (∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z) →
  ∀ (g : 𝕜 → E) (hg_an : AnalyticAt 𝕜 g x) (hg_ne : g x ≠ 0) (hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z),
    g x = 0
Tactic: refine fun ⟨g, hg_an, hg_ne, hg_eq⟩ ↦ hg_ne ?_
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h :
  ∀ᶠ (z : 𝕜) in 𝓝 x,
    (z - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f z =
      0
h_1 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ g x = 0
have pos : g =ᶠ[𝓝 x] fun {x : 𝕜} ↦ 0
Tactic: apply EventuallyEq.eq_of_nhds
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h :
  ∀ᶠ (z : 𝕜) in 𝓝 x,
    (z - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f z =
      0
h_1 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ g =ᶠ[𝓝 x] fun {x : 𝕜} ↦ 0
have pos : ∃ᶠ (z : 𝕜) in 𝓝[≠] x, g z = 0
Tactic: rw [EventuallyEq, ← AnalyticAt.frequently_eq_iff_eventually_eq hg_an analyticAt_const]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h :
  ∀ᶠ (z : 𝕜) in 𝓝 x,
    (z - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f z =
      0
h_1 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ ∃ᶠ (z : 𝕜) in 𝓝[≠] x, g z = 0
have pos : ∀ᶠ (x : 𝕜) in 𝓝[≠] x, g x = 0
Tactic: apply Eventually.frequently
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h :
  ∀ᶠ (z : 𝕜) in 𝓝 x,
    (z - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f z =
      0
h_1 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ ∀ᶠ (x : 𝕜) in 𝓝[≠] x, g x = 0
have pos : ∀ (hg_eq : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = (x_1 - x) ^ n • g x_1),
  ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → g x_1 = 0
Tactic: rw [eventually_nhdsWithin_iff] at hg_eq ⊢
Cleared hypotheses: hg_eq
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h :
  ∀ᶠ (z : 𝕜) in 𝓝 x,
    (z - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f z =
      0
h_1 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = (x_1 - x) ^ n • g x_1
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → g x_1 = 0
have h₁ : ∀ (z : 𝕜)
  (hfz :
    (z - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f z =
      0)
  (hfz_eq : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = (z - x) ^ n • g z) (hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z),
  g z = 0
Tactic: filter_upwards [h, hg_eq] with z hfz hfz_eq hz
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h :
  ∀ᶠ (z : 𝕜) in 𝓝 x,
    (z - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f z =
      0
h_1 : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = (x_1 - x) ^ n • g x_1
z : 𝕜
hfz :
  (z - x) ^
        Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
          hf •
      f z =
    0
hfz_eq : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = (z - x) ^ n • g z
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z
⊢ g z = 0
have h₁ : ∀
  (hfz :
    ((z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf *
          (z - x) ^ n) •
        g z =
      0)
  (hfz_eq : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = (z - x) ^ n • g z) (hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z),
  (z - x) ^
        Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
          hf *
      (z - x) ^ n ≠
    0
Tactic: rwa [hfz_eq hz, ← mul_smul, smul_eq_zero_iff_right] at hfz
Cleared hypotheses: hfz, hfz_eq, hz
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h :
  ¬analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
            f z)
        x =
      ⊤
⊢ HSub.hSub (α := WithTop ℤ)
        (ENat.map (fun (x : ℕ) ↦ (↑x : ℤ))
          (analyticOrderAt.{u_1, u_2} (E := E)
            (fun (z : 𝕜) ↦
              (z - x) ^
                  Exists.choose (p := fun (n : ℕ) ↦
                    AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) ⋯ •
                f z)
            x))
        (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              ⋯) :
          WithTop ℤ) =
      (↑n : WithTop ℤ) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
have neg : ∀ (m : ℕ)
  (h :
    (↑m : ℕ∞) =
      analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
            f z)
        x),
  HSub.hSub (α := WithTop ℤ)
        (ENat.map (fun (x : ℕ) ↦ (↑x : ℤ))
          (analyticOrderAt.{u_1, u_2} (E := E)
            (fun (z : 𝕜) ↦
              (z - x) ^
                  Exists.choose (p := fun (n : ℕ) ↦
                    AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) sorry •
                f z)
            x))
        (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              sorry) :
          WithTop ℤ) =
      (↑n : WithTop ℤ) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
Tactic: obtain ⟨m, h⟩ := ENat.ne_top_iff_exists.mp h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h_1 :
  ¬analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
            f z)
        x =
      ⊤
m : ℕ
h :
  (↑m : ℕ∞) =
    analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x
⊢ HSub.hSub (α := WithTop ℤ)
        (ENat.map (fun (x : ℕ) ↦ (↑x : ℤ))
          (analyticOrderAt.{u_1, u_2} (E := E)
            (fun (z : 𝕜) ↦
              (z - x) ^
                  Exists.choose (p := fun (n : ℕ) ↦
                    AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) ⋯ •
                f z)
            x))
        (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              ⋯) :
          WithTop ℤ) =
      (↑n : WithTop ℤ) ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
have neg : HSub.hSub (α := ℤ) (↑m : ℤ)
      (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            sorry) :
        ℤ) =
    n ↔
  ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
Tactic: rw [← h, ENat.map_coe, ← WithTop.coe_natCast, ← coe_sub, WithTop.coe_inj]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h_1 :
  ¬analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
            f z)
        x =
      ⊤
m : ℕ
h :
  (↑m : ℕ∞) =
    analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x
⊢ HSub.hSub (α := ℤ) (↑m : ℤ)
        (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              ⋯) :
          ℤ) =
      n ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
have neg : ∀ (g : 𝕜 → E) (hg_an : AnalyticAt 𝕜 g x) (hg_ne : g x ≠ 0)
  (hg_eq :
    ∀ᶠ (z : 𝕜) in 𝓝 x,
      (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z =
        (z - x) ^ m • g z),
  HSub.hSub (α := ℤ) (↑m : ℤ)
        (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              sorry) :
          ℤ) =
      n ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
Tactic: obtain ⟨g, hg_an, hg_ne, hg_eq⟩ := hf.choose_spec.analyticOrderAt_eq_natCast.mp h.symm