awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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₂f : meromorphicOrderAt f x = ⊤
this : toMeromorphicNFAt f x =ᶠ[𝓝 x] 0
pos : AnalyticAt 𝕜 (toMeromorphicNFAt f x) x
⊢ MeromorphicNFAt (toMeromorphicNFAt f x) x

Tactic:
apply AnalyticAt.meromorphicNFAt

Premises used: AnalyticAt.meromorphicNFAt
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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₂f : meromorphicOrderAt f x = ⊤
this : toMeromorphicNFAt f x =ᶠ[𝓝 x] 0
pos : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) 0 x
⊢ AnalyticAt 𝕜 (toMeromorphicNFAt f x) x

Tactic:
rw [analyticAt_congr this]

Premises used: analyticAt_congr
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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₂f : meromorphicOrderAt f x = ⊤
this : toMeromorphicNFAt f x =ᶠ[𝓝 x] 0
⊢ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) 0 x

Tactic:
analyticAt_const

Premises used: analyticAt_const
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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₂f : meromorphicOrderAt f x = ⊤
this : toMeromorphicNFAt f x =ᶠ[𝓝 x] 0
⊢ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) 0 x

Tactic:
exact analyticAt_const

Premises used: analyticAt_const
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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₂f : ¬meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt f x ≠ ⊤

Tactic:
h₂f
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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₂f : ¬meromorphicOrderAt f x = ⊤
neg : ∀ (n : ℤ) (hn : (↑n : WithTop ℤ) = meromorphicOrderAt f x), MeromorphicNFAt (toMeromorphicNFAt f x) x
⊢ MeromorphicNFAt (toMeromorphicNFAt f x) x

Tactic:
lift meromorphicOrderAt f x to ℤ using h₂f with n hn

Premises used: meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
neg :
  ∀ (g : 𝕜 → E) (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0) (h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z),
    MeromorphicNFAt (toMeromorphicNFAt f x) x
⊢ MeromorphicNFAt (toMeromorphicNFAt f x) x

Tactic:
obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_eq_int_iff hf).1 hn.symm

Premises used: meromorphicOrderAt_eq_int_iff, Iff.mp, Eq.symm
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
neg :
  ∃ (n : ℤ) (g : 𝕜 → E),
    AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ toMeromorphicNFAt f x =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ MeromorphicNFAt (toMeromorphicNFAt f x) x

Tactic:
right
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
right : toMeromorphicNFAt f x =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ ∃ (n : ℤ) (g : 𝕜 → E),
    AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ toMeromorphicNFAt f x =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g

Tactic:
use n, g, h₁g, h₂g
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
right : toMeromorphicNFAt f x x = (x - x) ^ n • g x
⊢ toMeromorphicNFAt f x =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g

Tactic:
apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE (hf.eq_nhdsNE_toMeromorphicNFAt.symm.trans h₃g)

Premises used: Filter.EventuallyEq.trans, MeromorphicAt.eq_nhdsNE_toMeromorphicNFAt, eventuallyEq_nhds_of_eventuallyEq_nhdsNE, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
right :
  (if h : n = 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) =
    HPow.hPow (α := 𝕜) 0 n • g x
⊢ toMeromorphicNFAt f x x = (x - x) ^ n • g x

Tactic:
simp only [toMeromorphicNFAt, hf, ↓reduceDIte, ← hn, WithTop.coe_zero,
        WithTop.coe_eq_zero, ne_eq, Function.update_self, sub_self]

Premises used: sub_self, WithTop.coe_eq_zero, reduceDIte, WithTop.coe_zero, ne_eq, toMeromorphicNFAt, Function.update_self
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
pos :
  ∀ (h₃f : n = 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) ⋯ x =
      HPow.hPow (α := 𝕜) 0 n • g x
neg : ∀ (h₃f : ¬n = 0), 0 = HPow.hPow (α := 𝕜) 0 n • g x
⊢ (if h : n = 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) =
    HPow.hPow (α := 𝕜) 0 n • g x

Tactic:
split_ifs with h₃f
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
⊢ 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

Tactic:
obtain ⟨h₁G, _, h₃G⟩ :=
          Classical.choose_spec ((meromorphicOrderAt_eq_int_iff hf).1 (h₃f ▸ hn.symm))

Premises used: meromorphicOrderAt_eq_int_iff, Classical.choose_spec, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
⊢ 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

Tactic:
obtain ⟨h₁G, _, h₃G⟩ :=
          Classical.choose_spec ((meromorphicOrderAt_eq_int_iff hf).1 (h₃f ▸ hn.symm))

Premises used: meromorphicOrderAt_eq_int_iff, Classical.choose_spec, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
⊢ ∀ᶠ (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

Tactic:
obtain ⟨h₁G, _, h₃G⟩ :=
          Classical.choose_spec ((meromorphicOrderAt_eq_int_iff hf).1 (h₃f ▸ hn.symm))

Premises used: meromorphicOrderAt_eq_int_iff, Classical.choose_spec, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
pos :
  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
⊢ 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 =
    HPow.hPow (α := 𝕜) 0 n • g x

Tactic:
apply Filter.EventuallyEq.eq_of_nhds

Premises used: Filter.EventuallyEq.eq_of_nhds
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
⊢ ContinuousAt.{u_1, u_2} (Y := E) (fun {x : 𝕜} ↦ HPow.hPow (α := 𝕜) 0 n • g x) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
pos :
  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
⊢ 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

Tactic:
apply (h₁G.continuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE (by fun_prop)).1

Premises used: Iff.mp, AnalyticAt.continuousAt, ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
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) ⋯ 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) ⋯ a =
          HPow.hPow (α := 𝕜) 0 n • g 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) ⋯ =ᶠ[𝓝[≠] x]
    fun {x : 𝕜} ↦ HPow.hPow (α := 𝕜) 0 n • g x

Tactic:
filter_upwards [h₃g, h₃G]
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
⊢ ∀ (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) ⋯ 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) ⋯ a =
          HPow.hPow (α := 𝕜) 0 n • g a

Tactic:
simp_all
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
⊢ 0 = HPow.hPow (α := 𝕜) 0 n • g x

Tactic:
simp [h₃f, zero_zpow]

Premises used: zero_zpow
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
neg : MeromorphicNFAt.{u_1, u_2} (E := E) 0 x
⊢ MeromorphicNFAt (toMeromorphicNFAt f x) x

Tactic:
simp only [toMeromorphicNFAt, hf, ↓reduceDIte]

Premises used: reduceDIte, toMeromorphicNFAt
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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.{u_1, u_2} (E := E) 0 x

Tactic:
analyticAt_const.meromorphicNFAt

Premises used: analyticAt_const, AnalyticAt.meromorphicNFAt
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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.{u_1, u_2} (E := E) 0 x

Tactic:
exact analyticAt_const.meromorphicNFAt

Premises used: analyticAt_const, AnalyticAt.meromorphicNFAt
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
rw : MeromorphicNFAt (toMeromorphicNFAt f x) x
⊢ MeromorphicNFAt f x

Tactic:
rw [hf.symm]

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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 (toMeromorphicNFAt f x) x

Tactic:
meromorphicNFAt_toMeromorphicNFAt

Premises used: meromorphicNFAt_toMeromorphicNFAt
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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 (toMeromorphicNFAt f x) x

Tactic:
exact meromorphicNFAt_toMeromorphicNFAt

Premises used: meromorphicNFAt_toMeromorphicNFAt
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
h : ∀ (z : 𝕜), toMeromorphicNFAt f x z = f z
⊢ toMeromorphicNFAt f x = f

Tactic:
funext z
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
neg : ∀ (hz : ¬z = x), toMeromorphicNFAt f x z = f z
⊢ toMeromorphicNFAt f x z = f z

Tactic:
by_cases hz : z = x
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
pos : toMeromorphicNFAt f x x = f x
⊢ toMeromorphicNFAt f x z = f z

Tactic:
rw [hz]
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
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) ⋯ x
          else 0)
      else 0)
      x =
    f x
⊢ toMeromorphicNFAt f x x = f x

Tactic:
simp only [toMeromorphicNFAt, hf.meromorphicAt, WithTop.coe_zero, ne_eq]

Premises used: WithTop.coe_zero, MeromorphicNFAt.meromorphicAt, ne_eq, toMeromorphicNFAt
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
⊢ MeromorphicNFAt f x

Tactic:
have h₀f := hf
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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
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) ⋯ 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

Tactic:
rcases hf with h₁f | h₁f
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
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 : 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

Tactic:
simpa [meromorphicOrderAt_eq_top_iff.2 (h₁f.filter_mono nhdsWithin_le_nhds)]
          using h₁f.eq_of_nhds.symm

Premises used: Iff.mpr, Filter.EventuallyEq.filter_mono, Filter.EventuallyEq.eq_of_nhds, meromorphicOrderAt_eq_top_iff, nhdsWithin_le_nhds, Eq.symm