awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
⊢ toMeromorphicNFOn f U =ᶠ[𝓝[≠] x] f
have h : ∀ (a : 𝕜) (ha : AnalyticAt 𝕜 f a ∨ a ∈ Uᶜ), toMeromorphicNFOn f U a = f a
Tactic: filter_upwards [hf.eventually_analyticAt_or_mem_compl hx] with a ha
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
a : 𝕜
ha : AnalyticAt 𝕜 f a ∨ a ∈ Uᶜ
⊢ toMeromorphicNFOn f U a = f a
have h : ∀ (ha : AnalyticAt 𝕜 f a), toMeromorphicNFOn f U a = f a
Tactic: rcases ha with ha | ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
a : 𝕜
ha : AnalyticAt 𝕜 f a ∨ a ∈ Uᶜ
h : ∀ (ha : AnalyticAt 𝕜 f a), toMeromorphicNFOn f U a = f a
⊢ toMeromorphicNFOn f U a = f a
have h₁ : ∀ (ha : a ∈ Uᶜ), toMeromorphicNFOn f U a = f a
Tactic: rcases ha with ha | ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
a : 𝕜
ha : a ∈ Uᶜ
⊢ toMeromorphicNFOn f U a = f a
have ha₁ : a ∉ U
Tactic: simp only [Set.mem_compl_iff] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
⊢ toMeromorphicNFOn f U =ᶠ[𝓝 x] toMeromorphicNFAt f x
have h₁ : toMeromorphicNFOn f U =ᶠ[𝓝[≠] x] toMeromorphicNFAt f x
Tactic: apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
h₁ : toMeromorphicNFOn f U =ᶠ[𝓝[≠] x] toMeromorphicNFAt f x
⊢ toMeromorphicNFOn f U =ᶠ[𝓝 x] toMeromorphicNFAt f x
have h₂ : toMeromorphicNFOn f U x = toMeromorphicNFAt f x x
Tactic: apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
⊢ toMeromorphicNFOn f U x = toMeromorphicNFAt f x x
have apply : toMeromorphicNFOn f U =ᶠ[𝓝 x] toMeromorphicNFAt f x
Tactic: apply Filter.EventuallyEq.eq_of_nhds (g := toMeromorphicNFAt f x)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
⊢ MeromorphicNFOn (toMeromorphicNFOn f U) U
have pos : ∀ (hf : MeromorphicOn f U), MeromorphicNFOn (toMeromorphicNFOn f U) U
Tactic: by_cases hf : MeromorphicOn f U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
pos : ∀ (hf : MeromorphicOn f U), MeromorphicNFOn (toMeromorphicNFOn f U) U
⊢ MeromorphicNFOn (toMeromorphicNFOn f U) U
have neg : ∀ (hf : ¬MeromorphicOn f U), MeromorphicNFOn (toMeromorphicNFOn f U) U
Tactic: by_cases hf : MeromorphicOn f U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : 𝕜
hz : z ∈ U
⊢ MeromorphicNFAt (toMeromorphicNFOn f U) z
have pos : MeromorphicNFAt (toMeromorphicNFAt f z) z
Tactic: rw [meromorphicNFAt_congr (toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhds hf hz)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
⊢ toMeromorphicNFOn f U = f ↔ MeromorphicNFOn f U
have mp : toMeromorphicNFOn f U = f → MeromorphicNFOn f U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
mp : toMeromorphicNFOn f U = f → MeromorphicNFOn f U
⊢ toMeromorphicNFOn f U = f ↔ MeromorphicNFOn f U
have mpr : MeromorphicNFOn f U → toMeromorphicNFOn f U = f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : toMeromorphicNFOn f U = f
⊢ MeromorphicNFOn f U
have mp : MeromorphicNFOn (toMeromorphicNFOn f U) U
Tactic: rw [h.symm]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicNFOn f U
⊢ toMeromorphicNFOn f U = f
have mpr : ∀ (x : 𝕜), toMeromorphicNFOn f U x = f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicNFOn f U
x : 𝕜
⊢ toMeromorphicNFOn f U x = f x
have pos : ∀ (hx : x ∈ U), toMeromorphicNFOn f U x = f x
Tactic: by_cases hx : x ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicNFOn f U
x : 𝕜
pos : ∀ (hx : x ∈ U), toMeromorphicNFOn f U x = f x
⊢ toMeromorphicNFOn f U x = f x
have neg : ∀ (hx : x ∉ U), toMeromorphicNFOn f U x = f x
Tactic: by_cases hx : x ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicNFOn f U
x : 𝕜
hx : x ∈ U
⊢ toMeromorphicNFOn f U x = f x
have pos : toMeromorphicNFAt f x x = f x
Tactic: simp only [toMeromorphicNFOn, h.meromorphicOn, ↓reduceDIte, hx]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicNFOn f U
x : 𝕜
hx : x ∈ U
⊢ toMeromorphicNFAt f x x = f x
have pos : f x = f x
Tactic: rw [toMeromorphicNFAt_eq_self.2 (h hx)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
⊢ meromorphicOrderAt (toMeromorphicNFOn f U) x = meromorphicOrderAt f x
have hf₁₂ : toMeromorphicNFOn f U =ᶠ[𝓝[≠] x] f
Tactic: apply meromorphicOrderAt_congr
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (toMeromorphicNFOn f U) U) (divisor f U)
have h : ∀ (z : 𝕜), Eq (α := ℤ) ((divisor (toMeromorphicNFOn f U) U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f U : (a : 𝕜) → ℤ) z : ℤ)
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : 𝕜
⊢ Eq (α := ℤ) ((divisor (toMeromorphicNFOn f U) U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f U : (a : 𝕜) → ℤ) z : ℤ)
have pos : ∀ (hz : z ∈ U),
  Eq (α := ℤ) ((divisor (toMeromorphicNFOn f U) U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f U : (a : 𝕜) → ℤ) z : ℤ)
Tactic: by_cases hz : z ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.NormalForm (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : 𝕜
pos :
  ∀ (hz : z ∈ U),
    Eq (α := ℤ) ((divisor (toMeromorphicNFOn f U) U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f U : (a : 𝕜) → ℤ) z : ℤ)
⊢ Eq (α := ℤ) ((divisor (toMeromorphicNFOn f U) U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f U : (a : 𝕜) → ℤ) z : ℤ)
have neg : ∀ (hz : z ∉ U),
  Eq (α := ℤ) ((divisor (toMeromorphicNFOn f U) U : (a : 𝕜) → ℤ) z : ℤ) ((divisor f U : (a : 𝕜) → ℤ) z : ℤ)
Tactic: by_cases hz : z ∈ U
-- 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 : meromorphicOrderAt f x ≠ 0
⊢ MeromorphicAt f x
have contrapose : ∀ (hf : ¬MeromorphicAt f x), meromorphicOrderAt f x = 0
Tactic: contrapose hf
Cleared hypotheses: hf
-- 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 : 𝕜
⊢ meromorphicOrderAt f x = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
have pos : ∀ (hf : MeromorphicAt f x), meromorphicOrderAt f x = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
Tactic: by_cases hf : MeromorphicAt f 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 : 𝕜
pos : ∀ (hf : MeromorphicAt f x), meromorphicOrderAt f x = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ meromorphicOrderAt f x = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
have neg : ∀ (hf : ¬MeromorphicAt f x), meromorphicOrderAt f x = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
Tactic: by_cases hf : MeromorphicAt f 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 : 𝕜
hf : ¬MeromorphicAt f x
⊢ meromorphicOrderAt f x = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
have neg : ¬∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
Tactic: simp only [hf, not_false_eq_true, meromorphicOrderAt_of_not_meromorphicAt, WithTop.zero_ne_top,
      false_iff]
-- 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
⊢ ¬∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
have neg : ∀ (hf : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0), MeromorphicAt f x
Tactic: contrapose hf
Cleared hypotheses: hf
-- 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
⊢ meromorphicOrderAt f x = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
have pos : 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 =
    ⊤ ↔
  ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
Tactic: simp only [meromorphicOrderAt, hf, ↓reduceDIte, sub_eq_top_iff, ENat.map_eq_top_iff,
    WithTop.natCast_ne_top, or_false]
-- 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
⊢ 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 =
      ⊤ ↔
    ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
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 =
      ⊤),
  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 =
      ⊤ ↔
    ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
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 : 𝕜
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 =
        ⊤),
    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 =
        ⊤ ↔
      ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ 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 =
      ⊤ ↔
    ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
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 =
        ⊤),
  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 =
      ⊤ ↔
    ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
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 : 𝕜
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 =
    ⊤
⊢ 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 =
      ⊤ ↔
    ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
have pos : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, ¬x_1 = x → f x_1 = 0
Tactic: simp only [h, eventually_nhdsWithin_iff, mem_compl_iff, mem_singleton_iff, true_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 : 𝕜
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 =
    ⊤
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, ¬x_1 = x → f x_1 = 0
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 : 𝕜
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
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, ¬x_1 = x → f x_1 = 0
have h₁ : ∀ (z : 𝕜)
  (hf :
    (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)
  (hz : ¬z = x), f z = 0
Tactic: filter_upwards [h] with z hf 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 : 𝕜
hf_1 : 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_1 •
        f z =
      0
z : 𝕜
hf :
  (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_1 •
      f z =
    0
hz : ¬z = x
⊢ f z = 0
have h₁ : ∀ (hf : f z = 0) (hz : ¬z = x), f z = 0
Tactic: rwa [smul_eq_zero_iff_right <| pow_ne_zero _ (sub_ne_zero.mpr hz)] at hf
Cleared hypotheses: hf, 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 : 𝕜
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 =
      ⊤
⊢ 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 =
      ⊤ ↔
    ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
have neg : ∀ (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),
  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 =
      ⊤ ↔
    ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
Tactic: obtain ⟨m, hm⟩ := 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 : 𝕜
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 =
      ⊤
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
⊢ 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 =
      ⊤ ↔
    ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
have neg : ¬∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
Tactic: simp only [← hm, ENat.coe_ne_top, false_iff]
-- 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
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 =
      ⊤
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
⊢ ¬∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
have neg : ∀ (h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0),
  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 =
    ⊤
Tactic: contrapose 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 : 𝕜
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
⊢ 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 =
    ⊤
have neg : ∀ᶠ (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]
-- 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 : ∃ᶠ (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 [← hf.choose_spec.frequently_eq_iff_eventually_eq analyticAt_const]