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 : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : (↑n : WithTop ℤ) = meromorphicOrderAt f x
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
h₃f : n = 0
h₁G :
  AnalyticAt 𝕜
    (Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯)
    x
left :
  Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x ≠
    0
h₃G :
  ∀ᶠ (z : 𝕜) in 𝓝[≠] x,
    f z =
      HPow.hPow (β := ℤ) (z - x) 0 •
        Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
          AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ z
⊢ Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ =ᶠ[𝓝[≠] x]
    fun {x : 𝕜} ↦ HPow.hPow (α := 𝕜) 0 n • g x
have h : ∀ (a : 𝕜),
  f a = (a - x) ^ n • g a →
    f a =
        HPow.hPow (β := ℤ) (a - x) 0 •
          Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
            AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) sorry a →
      Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
          AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) sorry a =
        HPow.hPow (α := 𝕜) 0 n • g a
Tactic: filter_upwards [h₃g, h₃G]
-- 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 : 𝕜
hf : ¬MeromorphicAt f x
⊢ MeromorphicNFAt (toMeromorphicNFAt f x) x
have neg : MeromorphicNFAt.{u_1, u_2} (E := E) 0 x
Tactic: simp only [toMeromorphicNFAt, hf, ↓reduceDIte]
-- 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 : 𝕜
hf : toMeromorphicNFAt f x = f
⊢ MeromorphicNFAt f x
have rw : MeromorphicNFAt (toMeromorphicNFAt f x) x
Tactic: rw [hf.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
x : 𝕜
hf : MeromorphicNFAt f x
⊢ toMeromorphicNFAt f x = f
have h : ∀ (z : 𝕜), toMeromorphicNFAt f x z = f z
Tactic: funext 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
x : 𝕜
hf : MeromorphicNFAt f x
z : 𝕜
⊢ toMeromorphicNFAt f x z = f z
have pos : ∀ (hz : z = x), toMeromorphicNFAt f x z = f z
Tactic: by_cases hz : z = 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
x : 𝕜
hf : MeromorphicNFAt f x
z : 𝕜
pos : ∀ (hz : z = x), toMeromorphicNFAt f x z = f z
⊢ toMeromorphicNFAt f x z = f z
have neg : ∀ (hz : ¬z = x), toMeromorphicNFAt f x z = f z
Tactic: by_cases hz : z = 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
x : 𝕜
hf : MeromorphicNFAt f x
z : 𝕜
hz : z = x
⊢ toMeromorphicNFAt f x z = f z
have pos : toMeromorphicNFAt f x x = f x
Tactic: rw [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
x : 𝕜
hf : MeromorphicNFAt f x
z : 𝕜
hz : z = x
⊢ toMeromorphicNFAt f x x = f x
have pos : (if h : True then
      Function.update (β := fun (a : 𝕜) ↦ E) f x
        (if h_1 : meromorphicOrderAt f x = 0 then
          Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
            AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) sorry x
        else 0)
    else 0)
    x =
  f x
Tactic: simp only [toMeromorphicNFAt, hf.meromorphicAt, WithTop.coe_zero, ne_eq]
-- 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 : 𝕜
hf : MeromorphicNFAt f x
z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
⊢ (if h : True then
        Function.update (β := fun (a : 𝕜) ↦ E) f x
          (if h_1 : meromorphicOrderAt f x = 0 then
            Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
              AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x
          else 0)
      else 0)
      x =
    f x
have pos : ∀ (h₁f : f =ᶠ[𝓝 x] 0),
  (if h : True then
        Function.update (β := fun (a : 𝕜) ↦ E) f x
          (if h_1 : meromorphicOrderAt f x = 0 then
            Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
              AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) sorry x
          else 0)
      else 0)
      x =
    f x
Tactic: rcases hf with h₁f | h₁f
Cleared hypotheses: hf
-- 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 : 𝕜
hf : MeromorphicNFAt f x
z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
pos :
  ∀ (h₁f : f =ᶠ[𝓝 x] 0),
    (if h : True then
          Function.update (β := fun (a : 𝕜) ↦ E) f x
            (if h_1 : meromorphicOrderAt f x = 0 then
              Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
                AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x
            else 0)
        else 0)
        x =
      f x
⊢ (if h : True then
        Function.update (β := fun (a : 𝕜) ↦ E) f x
          (if h_1 : meromorphicOrderAt f x = 0 then
            Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
              AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x
          else 0)
      else 0)
      x =
    f x
have pos₁ : ∀
  (h₁f :
    ∃ (n : ℤ) (g : 𝕜 → E),
      AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g),
  (if h : True then
        Function.update (β := fun (a : 𝕜) ↦ E) f x
          (if h_1 : meromorphicOrderAt f x = 0 then
            Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
              AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) sorry x
          else 0)
      else 0)
      x =
    f x
Tactic: rcases hf with h₁f | h₁f
Cleared hypotheses: hf
-- 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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
h₁f :
  ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ (if h : True then
        Function.update (β := fun (a : 𝕜) ↦ E) f x
          (if h_1 : meromorphicOrderAt f x = 0 then
            Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
              AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x
          else 0)
      else 0)
      x =
    f x
have pos : ∀ (n : ℤ) (g : 𝕜 → E) (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0)
  (h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g),
  (if h : True then
        Function.update (β := fun (a : 𝕜) ↦ E) f x
          (if h_1 : meromorphicOrderAt f x = 0 then
            Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
              AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) sorry x
          else 0)
      else 0)
      x =
    f x
Tactic: obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h₁f
Cleared hypotheses: h₁f
-- 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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ (if h : True then
        Function.update (β := fun (a : 𝕜) ↦ E) f x
          (if h_1 : meromorphicOrderAt f x = 0 then
            Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
              AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x
          else 0)
      else 0)
      x =
    f x
have pos : (if h : True then
      Function.update (β := fun (a : 𝕜) ↦ E) f x
        (if h_1 : meromorphicOrderAt f x = 0 then
          Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
            AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) sorry x
        else 0)
    else 0)
    x =
  (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x
Tactic: rw [Filter.EventuallyEq.eq_of_nhds h₃g]
-- 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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ meromorphicOrderAt f x = (↑n : WithTop ℤ)
have rw : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
Tactic: rw [meromorphicOrderAt_eq_int_iff h₀f.meromorphicAt]
-- 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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
have right : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
Tactic: use g, h₁g, h₂g
-- 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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ (if h : True then
        Function.update (β := fun (a : 𝕜) ↦ E) f x
          (if h_1 : meromorphicOrderAt f x = 0 then
            Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
              AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x
          else 0)
      else 0)
      x =
    (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x
have this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
Tactic: have : meromorphicOrderAt f x = n := by
          rw [meromorphicOrderAt_eq_int_iff h₀f.meromorphicAt]
          use g, h₁g, h₂g
          exact eventually_nhdsWithin_of_eventually_nhds h₃g
-- 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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
⊢ (if h : True then
        Function.update (β := fun (a : 𝕜) ↦ E) f x
          (if h_1 : meromorphicOrderAt f x = 0 then
            Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
              AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x
          else 0)
      else 0)
      x =
    (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x
have pos : ∀ (h₃f : meromorphicOrderAt f x = 0),
  (if h : True then
        Function.update (β := fun (a : 𝕜) ↦ E) f x
          (if h_1 : meromorphicOrderAt f x = 0 then
            Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
              AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) sorry x
          else 0)
      else 0)
      x =
    (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x
Tactic: by_cases h₃f : meromorphicOrderAt f x = 0
-- 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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
pos :
  ∀ (h₃f : meromorphicOrderAt f x = 0),
    (if h : True then
          Function.update (β := fun (a : 𝕜) ↦ E) f x
            (if h_1 : meromorphicOrderAt f x = 0 then
              Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
                AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x
            else 0)
        else 0)
        x =
      (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x
⊢ (if h : True then
        Function.update (β := fun (a : 𝕜) ↦ E) f x
          (if h_1 : meromorphicOrderAt f x = 0 then
            Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
              AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x
          else 0)
      else 0)
      x =
    (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x
have neg : ∀ (h₃f : ¬meromorphicOrderAt f x = 0),
  (if h : True then
        Function.update (β := fun (a : 𝕜) ↦ E) f x
          (if h_1 : meromorphicOrderAt f x = 0 then
            Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
              AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) sorry x
          else 0)
      else 0)
      x =
    (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x
Tactic: by_cases h₃f : meromorphicOrderAt f x = 0
-- 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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : meromorphicOrderAt f x = 0
⊢ (if h : True then
        Function.update (β := fun (a : 𝕜) ↦ E) f x
          (if h_1 : meromorphicOrderAt f x = 0 then
            Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
              AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x
          else 0)
      else 0)
      x =
    (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x
have pos : Function.update (β := fun (a : 𝕜) ↦ E) f x
    (Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) sorry x)
    x =
  HPow.hPow (α := 𝕜) 0 n • g x
Tactic: simp only [Pi.smul_apply', Pi.pow_apply, sub_self, h₃f, ↓reduceDIte]
-- 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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : meromorphicOrderAt f x = 0
⊢ n = 0
have this₁ : 0 = (↑n : WithTop ℤ)
Tactic: rw [h₃f] at this
Cleared hypotheses: this, h₃f
-- 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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : meromorphicOrderAt f x = 0
⊢ Function.update (β := fun (a : 𝕜) ↦ E) f x
      (Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
        AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x)
      x =
    HPow.hPow (α := 𝕜) 0 n • g x
have hn : n = 0
Tactic: have hn : n = (0 : ℤ) := by
            rw [h₃f] at this
            exact WithTop.coe_eq_zero.mp this.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
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
⊢ Function.update (β := fun (a : 𝕜) ↦ E) f x
      (Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
        AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x)
      x =
    HPow.hPow (α := 𝕜) 0 n • g x
have pos : Function.update (β := fun (a : 𝕜) ↦ E) f x
    (Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) sorry x)
    x =
  HPow.hPow (α := 𝕜) (β := ℤ) 0 0 • g x
Tactic: simp_rw [hn]
-- 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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
⊢ Function.update (β := fun (a : 𝕜) ↦ E) f x
      (Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
        AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x)
      x =
    HPow.hPow (α := 𝕜) (β := ℤ) 0 0 • g x
have pos : Function.update (β := fun (a : 𝕜) ↦ E) f x
    (Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ ¬x_1 x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) sorry x)
    x =
  g x
Tactic: simp only [zpow_zero, one_smul]
-- 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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
⊢ g =ᶠ[𝓝 x]
    Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯
have h₀ : AnalyticAt 𝕜
  (Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
    AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) sorry)
  x
Tactic: obtain ⟨h₀, h₁, h₂⟩ := Classical.choose_spec
              ((meromorphicOrderAt_eq_int_iff h₀f.meromorphicAt).1 h₃f)
-- 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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
h₀ :
  AnalyticAt 𝕜
    (Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯)
    x
⊢ g =ᶠ[𝓝 x]
    Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯
have h₁ : Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
    AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) sorry x ≠
  0
Tactic: obtain ⟨h₀, h₁, h₂⟩ := Classical.choose_spec
              ((meromorphicOrderAt_eq_int_iff h₀f.meromorphicAt).1 h₃f)
-- 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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
h₀ :
  AnalyticAt 𝕜
    (Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯)
    x
h₁ :
  Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x ≠
    0
⊢ g =ᶠ[𝓝 x]
    Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯
have h₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x,
  f z =
    HPow.hPow (β := ℤ) (z - x) 0 •
      Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
        AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) sorry z
Tactic: obtain ⟨h₀, h₁, h₂⟩ := Classical.choose_spec
              ((meromorphicOrderAt_eq_int_iff h₀f.meromorphicAt).1 h₃f)
-- 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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
h₀ :
  AnalyticAt 𝕜
    (Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯)
    x
h₁ :
  Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ x ≠
    0
h₂ :
  ∀ᶠ (z : 𝕜) in 𝓝[≠] x,
    f z =
      HPow.hPow (β := ℤ) (z - x) 0 •
        Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
          AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯ z
⊢ g =ᶠ[𝓝 x]
    Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
      AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) ⋯
have rw : g =ᶠ[𝓝[≠] x]
  Classical.choose (p := fun (x_1 : 𝕜 → E) ↦
    AnalyticAt 𝕜 x_1 x ∧ x_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • x_1 z) sorry
Tactic: rw [← h₁g.continuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE h₀.continuousAt]