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 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
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) ⋯ 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:
obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := 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
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
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 =
    (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 =
    f x

Tactic:
rw [Filter.EventuallyEq.eq_of_nhds h₃g]

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 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
rw : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ meromorphicOrderAt f x = (↑n : WithTop ℤ)

Tactic:
rw [meromorphicOrderAt_eq_int_iff h₀f.meromorphicAt]

Premises used: meromorphicOrderAt_eq_int_iff, MeromorphicNFAt.meromorphicAt
-- 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
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
right : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
use 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 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
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
eventually_nhdsWithin_of_eventually_nhds h₃g

Premises used: eventually_nhdsWithin_of_eventually_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 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
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
exact eventually_nhdsWithin_of_eventually_nhds h₃g

Premises used: eventually_nhdsWithin_of_eventually_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 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 ℤ)

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
-- 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
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
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) ⋯ 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

Tactic:
by_cases h₃f : meromorphicOrderAt f x = 0

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 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
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) ⋯ x)
      x =
    HPow.hPow (α := 𝕜) 0 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

Tactic:
simp only [Pi.smul_apply', Pi.pow_apply, sub_self, h₃f, ↓reduceDIte]

Premises used: sub_self, Pi.smul_apply', reduceDIte, Pi.pow_apply
-- 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
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
⊢ 0 = (↑n : WithTop ℤ)

Tactic:
rw [h₃f] at this
-- 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
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
this₁ : 0 = (↑n : WithTop ℤ)
⊢ meromorphicOrderAt f x = 0

Tactic:
rw [h₃f] at this
-- 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
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 : 0 = (↑n : WithTop ℤ)
h₃f : meromorphicOrderAt f x = 0
⊢ n = 0

Tactic:
WithTop.coe_eq_zero.mp this.symm

Premises used: WithTop.coe_eq_zero, 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 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 : 0 = (↑n : WithTop ℤ)
h₃f : meromorphicOrderAt f x = 0
⊢ n = 0

Tactic:
exact WithTop.coe_eq_zero.mp this.symm

Premises used: WithTop.coe_eq_zero, 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 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

Tactic:
have hn : n = (0 : ℤ) := by
            rw [h₃f] at this
            exact WithTop.coe_eq_zero.mp this.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 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
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) ⋯ x)
      x =
    HPow.hPow (α := 𝕜) (β := ℤ) 0 0 • g x
⊢ 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

Tactic:
simp_rw [hn]
-- 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
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
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) ⋯ x)
      x =
    g x
⊢ 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

Tactic:
simp only [zpow_zero, one_smul]

Premises used: zpow_zero, one_smul
-- 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
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
⊢ 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₀, h₁, h₂⟩ := Classical.choose_spec
              ((meromorphicOrderAt_eq_int_iff h₀f.meromorphicAt).1 h₃f)

Premises used: meromorphicOrderAt_eq_int_iff, MeromorphicNFAt.meromorphicAt, 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 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
⊢ 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₀, h₁, h₂⟩ := Classical.choose_spec
              ((meromorphicOrderAt_eq_int_iff h₀f.meromorphicAt).1 h₃f)

Premises used: meromorphicOrderAt_eq_int_iff, MeromorphicNFAt.meromorphicAt, 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 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
⊢ ∀ᶠ (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₀, h₁, h₂⟩ := Classical.choose_spec
              ((meromorphicOrderAt_eq_int_iff h₀f.meromorphicAt).1 h₃f)

Premises used: meromorphicOrderAt_eq_int_iff, MeromorphicNFAt.meromorphicAt, 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 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
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) ⋯
⊢ 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) ⋯

Tactic:
rw [← h₁g.continuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE h₀.continuousAt]

Premises used: 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 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
⊢ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) 0 • g

Tactic:
rw [hn] at 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 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
h₃g₁ : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) 0 • g
⊢ meromorphicOrderAt f x = (↑n : WithTop ℤ)

Tactic:
rw [hn] at 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 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
h₃g₁ : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) 0 • g
this₁ : meromorphicOrderAt f x = (↑n : WithTop ℤ)
⊢ meromorphicOrderAt f x = 0

Tactic:
rw [hn] at 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 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
h₃g₁ : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) 0 • g
this₁ : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f₁ : meromorphicOrderAt f x = 0
⊢ n = 0

Tactic:
rw [hn] at 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 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
h₃g₁ : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) 0 • g
this₁ : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f₁ : meromorphicOrderAt f x = 0
hn₁ : 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:
rw [hn] at h₃g