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
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
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:
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
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:
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) 0 • 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] g

Tactic:
simp only [zpow_zero, one_smul, ne_eq] at h₃g h₂

Premises used: zpow_zero, ne_eq, 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) 0 • 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] g
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x,
    f 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) ⋯ z

Tactic:
simp only [zpow_zero, one_smul, ne_eq] at h₃g h₂

Premises used: zpow_zero, ne_eq, 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
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₃g : f =ᶠ[𝓝 x] g
h₂ :
  ∀ᶠ (z : 𝕜) in 𝓝[≠] x,
    f 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) ⋯ 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:
(h₃g.filter_mono nhdsWithin_le_nhds).symm.trans h₂

Premises used: Filter.EventuallyEq.filter_mono, Filter.EventuallyEq.trans, nhdsWithin_le_nhds, 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 z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
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₃g : f =ᶠ[𝓝 x] g
h₂ :
  ∀ᶠ (z : 𝕜) in 𝓝[≠] x,
    f 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) ⋯ 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:
exact (h₃g.filter_mono nhdsWithin_le_nhds).symm.trans h₂

Premises used: Filter.EventuallyEq.filter_mono, Filter.EventuallyEq.trans, nhdsWithin_le_nhds, 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 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) ⋯

Tactic:
have : g =ᶠ[𝓝 x]
              Classical.choose ((meromorphicOrderAt_eq_int_iff h₀f.meromorphicAt).1 h₃f) := by
            obtain ⟨h₀, h₁, h₂⟩ := Classical.choose_spec
              ((meromorphicOrderAt_eq_int_iff h₀f.meromorphicAt).1 h₃f)
            rw [← h₁g.continuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE h₀.continuousAt]
            rw [hn] at h₃g
            simp only [zpow_zero, one_smul, ne_eq] at h₃g h₂
            exact (h₃g.filter_mono nhdsWithin_le_nhds).symm.trans h₂
-- 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_1 : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
this :
  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) ⋯
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 =
    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 =
    g x

Tactic:
simp only [Function.update_self]

Premises used: 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 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_1 : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
this :
  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) ⋯
⊢ 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

Tactic:
Filter.EventuallyEq.eq_of_nhds this.symm

Premises used: Filter.EventuallyEq.eq_of_nhds, 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 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_1 : meromorphicOrderAt f x = (↑n : WithTop ℤ)
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
this :
  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) ⋯
⊢ 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

Tactic:
exact Filter.EventuallyEq.eq_of_nhds this.symm

Premises used: Filter.EventuallyEq.eq_of_nhds, 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 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
neg :
  (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
⊢ (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:
rw [eq_comm]

Premises used: eq_comm
-- 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
neg : HPow.hPow (α := 𝕜) 0 n = 0 ∨ g x = 0
⊢ (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

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

Premises used: sub_self, Pi.smul_apply', reduceDIte, Pi.pow_apply, Function.update_self, smul_eq_zero
-- 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
neg : HPow.hPow (α := 𝕜) 0 n = 0
⊢ HPow.hPow (α := 𝕜) 0 n = 0 ∨ g x = 0

Tactic:
left
-- 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
neg : n ≠ 0
⊢ HPow.hPow (α := 𝕜) 0 n = 0

Tactic:
apply zero_zpow n

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 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
neg : ∀ (hn : n = 0), False
⊢ n ≠ 0

Tactic:
by_contra 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
⊢ meromorphicOrderAt f x = (↑0 : WithTop ℤ)

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

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

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

Tactic:
tauto
-- 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
⊢ toMeromorphicNFAt f x z = f z

Tactic:
(hf.meromorphicAt.eqOn_compl_singleton_toMeromorphicNFAt hz).symm

Premises used: MeromorphicNFAt.meromorphicAt, MeromorphicAt.eqOn_compl_singleton_toMeromorphicNFAt, 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 : MeromorphicNFAt f x
z : 𝕜
hz : ¬z = x
⊢ toMeromorphicNFAt f x z = f z

Tactic:
exact (hf.meromorphicAt.eqOn_compl_singleton_toMeromorphicNFAt hz).symm

Premises used: MeromorphicNFAt.meromorphicAt, MeromorphicAt.eqOn_compl_singleton_toMeromorphicNFAt, 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
U : Set 𝕜
hf : MeromorphicNFOn f U
⊢ MeromorphicOn f U

Tactic:
fun _ hz ↦ (hf hz).meromorphicAt

Premises used: MeromorphicOn, 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
U : Set 𝕜
h₁f : MeromorphicNFOn f U
mp : LE.le (α := Function.locallyFinsuppWithin U ℤ) 0 (MeromorphicOn.divisor f U) → AnalyticOnNhd 𝕜 f U
mpr : AnalyticOnNhd 𝕜 f U → LE.le (α := Function.locallyFinsuppWithin U ℤ) 0 (MeromorphicOn.divisor f U)
⊢ LE.le (α := Function.locallyFinsuppWithin U ℤ) 0 (MeromorphicOn.divisor f U) ↔ AnalyticOnNhd 𝕜 f U

Tactic:
constructor
-- 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
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h : LE.le (α := Function.locallyFinsuppWithin U ℤ) 0 (MeromorphicOn.divisor f U)
x : 𝕜
hx : x ∈ U
mp : 0 ≤ meromorphicOrderAt f x
⊢ AnalyticAt 𝕜 f x

Tactic:
rw [← (h₁f hx).meromorphicOrderAt_nonneg_iff_analyticAt]

Premises used: MeromorphicNFAt.meromorphicOrderAt_nonneg_iff_analyticAt
-- 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
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h : LE.le (α := Function.locallyFinsuppWithin U ℤ) 0 (MeromorphicOn.divisor f U)
x : 𝕜
hx : x ∈ U
⊢ LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) x : ℤ)

Tactic:
have := h 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
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h : LE.le (α := Function.locallyFinsuppWithin U ℤ) 0 (MeromorphicOn.divisor f U)
x : 𝕜
hx : x ∈ U
this : LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) x : ℤ)
⊢ 0 ≤ meromorphicOrderAt f x

Tactic:
simp only [Function.locallyFinsuppWithin.coe_zero, Pi.zero_apply, h₁f.meromorphicOn, hx,
      MeromorphicOn.divisor_apply, untop₀_nonneg] at this

Premises used: WithTop.untop₀_nonneg, Pi.zero_apply, MeromorphicOn.divisor_apply, MeromorphicNFOn.meromorphicOn, Function.locallyFinsuppWithin.coe_zero
-- 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
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h : LE.le (α := Function.locallyFinsuppWithin U ℤ) 0 (MeromorphicOn.divisor f U)
x : 𝕜
hx : x ∈ U
this : 0 ≤ meromorphicOrderAt f x
⊢ 0 ≤ meromorphicOrderAt f x

Tactic:
assumption
-- 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
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h : AnalyticOnNhd 𝕜 f U
x : 𝕜
pos :
  ∀ (hx : x ∈ U),
    LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) x : ℤ)
neg :
  ∀ (hx : x ∉ U),
    LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) x : ℤ)
⊢ LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) x : ℤ)

Tactic:
by_cases hx : x ∈ U
-- 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
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h : AnalyticOnNhd 𝕜 f U
x : 𝕜
hx : x ∈ U
pos : 0 ≤ meromorphicOrderAt f x
⊢ LE.le (α := (fun (a : 𝕜) ↦ ℤ) x) ((0 : (a : 𝕜) → ℤ) x : ℤ) ((MeromorphicOn.divisor f U : (a : 𝕜) → ℤ) x : ℤ)

Tactic:
simp only [Function.locallyFinsuppWithin.coe_zero, Pi.zero_apply, h₁f.meromorphicOn, hx,
        MeromorphicOn.divisor_apply, untop₀_nonneg]

Premises used: WithTop.untop₀_nonneg, Pi.zero_apply, MeromorphicOn.divisor_apply, MeromorphicNFOn.meromorphicOn, Function.locallyFinsuppWithin.coe_zero
-- 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
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h : AnalyticOnNhd 𝕜 f U
x : 𝕜
hx : x ∈ U
⊢ 0 ≤ meromorphicOrderAt f x

Tactic:
(h₁f hx).meromorphicOrderAt_nonneg_iff_analyticAt.2 (h x hx)

Premises used: Iff.mpr, MeromorphicNFAt.meromorphicOrderAt_nonneg_iff_analyticAt