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 : 𝕜
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
hf : MeromorphicAt f x
⊢ meromorphicOrderAt f x = (↑n : WithTop ℤ)

Tactic:
have : meromorphicOrderAt f x = n := by
        rw [meromorphicOrderAt_eq_int_iff hf]
        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 : 𝕜
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
hf : MeromorphicAt f x
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
pos : ∀ (hn : 0 ≤ n), AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
neg : ∀ (hn : n < 0), AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0

Tactic:
by_cases! hn : 0 ≤ n
-- 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 : 𝕜
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
hf : MeromorphicAt f x
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
hn : 0 ≤ n
pos : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f 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 : 𝕜
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
hf : MeromorphicAt f x
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
hn : 0 ≤ n
pos : AnalyticAt 𝕜 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x
⊢ AnalyticAt 𝕜 f x

Tactic:
rw [analyticAt_congr h₃g]

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 : 𝕜
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
hf : MeromorphicAt f x
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
hn : 0 ≤ n
⊢ AnalyticAt 𝕜 (F := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - 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 : 𝕜
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
hf : MeromorphicAt f x
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
hn : 0 ≤ n
⊢ AnalyticAt 𝕜 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x

Tactic:
apply (AnalyticAt.zpow_nonneg (by fun_prop) hn).smul h₁g

Premises used: AnalyticAt.smul, AnalyticAt.zpow_nonneg
-- 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 : 𝕜
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
hf : MeromorphicAt f x
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
hn : n < 0
neg : MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0

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 : 𝕜
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
hf : MeromorphicAt f x
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
hn : n < 0
right : meromorphicOrderAt f x < 0 ∧ f x = 0
⊢ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0

Tactic:
use 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 : 𝕜
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
hf : MeromorphicAt f x
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
hn : n < 0
⊢ meromorphicOrderAt f x < 0 ∧ f x = 0

Tactic:
simp [this, WithTop.coe_lt_zero.2 hn, h₃g.eq_of_nhds,
          zero_zpow n hn.ne]

Premises used: Iff.mpr, zero_zpow, Filter.EventuallyEq.eq_of_nhds, LT.lt.ne, WithTop.coe_lt_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 : 𝕜
h : AnalyticAt 𝕜 f x
pos : ∀ (h₂f : analyticOrderAt f x = ⊤), MeromorphicNFAt f x
neg : ∀ (h₂f : ¬analyticOrderAt f x = ⊤), MeromorphicNFAt f x
⊢ MeromorphicNFAt f x

Tactic:
by_cases h₂f : analyticOrderAt f x = ⊤

Premises used: analyticOrderAt
-- 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 : 𝕜
h : AnalyticAt 𝕜 f x
h₂f : analyticOrderAt f x = ⊤
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x, f z = 0

Tactic:
rw [analyticOrderAt_eq_top] at h₂f

Premises used: analyticOrderAt_eq_top
-- 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 : 𝕜
h : AnalyticAt 𝕜 f x
h₂f : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = 0
pos pos₁ :
  ¬f =ᶠ[𝓝 x] 0 →
    ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ MeromorphicNFAt f x

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 : 𝕜
h : AnalyticAt 𝕜 f x
h₂f : ¬analyticOrderAt f x = ⊤
neg :
  ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ MeromorphicNFAt f 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 : 𝕜
h : AnalyticAt 𝕜 f x
h₂f : ¬analyticOrderAt f x = ⊤
h₁ :
  ∃ (g : 𝕜 → E),
    AnalyticAt 𝕜 g x ∧
      g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) (↑(analyticOrderNatAt f x) : ℤ) • g
⊢ ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g

Tactic:
use analyticOrderNatAt f x

Premises used: analyticOrderNatAt
-- 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 : 𝕜
h : AnalyticAt 𝕜 f x
h₂f : ¬analyticOrderAt f x = ⊤
⊢ analyticOrderAt f x ≠ ⊤

Tactic:
have : analyticOrderAt f x ≠ ⊤ := 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 : 𝕜
h : AnalyticAt 𝕜 f x
h₂f : ¬analyticOrderAt f x = ⊤
this : analyticOrderAt f x ≠ ⊤
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (analyticOrderAt f x).toNat • g z

Tactic:
rw [← ENat.coe_toNat_eq_self, eq_comm, h.analyticOrderAt_eq_natCast] at this

Premises used: AnalyticAt.analyticOrderAt_eq_natCast, eq_comm, ENat.coe_toNat_eq_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 : 𝕜
h : AnalyticAt 𝕜 f x
h₂f : ¬analyticOrderAt f x = ⊤
this : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (analyticOrderAt f x).toNat • g z
h₁ :
  ∀ (g : 𝕜 → E) (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0)
    (h₃g : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (analyticOrderAt f x).toNat • g z),
    ∃ (g : 𝕜 → E),
      AnalyticAt 𝕜 g x ∧
        g x ≠ 0 ∧
          f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) (↑(analyticOrderNatAt f x) : ℤ) • g
⊢ ∃ (g : 𝕜 → E),
    AnalyticAt 𝕜 g x ∧
      g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) (↑(analyticOrderNatAt f x) : ℤ) • g

Tactic:
obtain ⟨g, h₁g, h₂g, h₃g⟩ := 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 : 𝕜
h : AnalyticAt 𝕜 f x
h₂f : ¬analyticOrderAt f x = ⊤
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (analyticOrderAt f x).toNat • g z
right : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) (↑(analyticOrderNatAt f x) : ℤ) • g
⊢ ∃ (g : 𝕜 → E),
    AnalyticAt 𝕜 g x ∧
      g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) (↑(analyticOrderNatAt f x) : ℤ) • g

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 : 𝕜
h : AnalyticAt 𝕜 f x
h₂f : ¬analyticOrderAt f x = ⊤
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (analyticOrderAt f x).toNat • g z
⊢ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) (↑(analyticOrderNatAt f x) : ℤ) • g

Tactic:
simpa
-- 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 : 𝕜
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x < 0
h₃ : f x = 0
mpr :
  ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ MeromorphicNFAt f 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 : 𝕜
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x < 0
h₃ : f x = 0
⊢ meromorphicOrderAt f x ≠ ⊤

Tactic:
LT.lt.ne_top h₂

Premises used: LT.lt.ne_top
-- 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 : 𝕜
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x < 0
h₃ : f x = 0
mpr :
  ∀ (n : ℤ) (hn : (↑n : WithTop ℤ) = meromorphicOrderAt f x)
    (meromorphicNFAt_iff_analyticAt_or :
      MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ (↑n : WithTop ℤ) < 0 ∧ f x = 0)
    (h₂ : (↑n : WithTop ℤ) < 0),
    ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g

Tactic:
lift meromorphicOrderAt f x to ℤ using LT.lt.ne_top h₂ with n hn

Premises used: LT.lt.ne_top, 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 : 𝕜
h₁ : MeromorphicAt f x
h₃ : f x = 0
n : ℤ
hn : (↑n : WithTop ℤ) = meromorphicOrderAt f x
meromorphicNFAt_iff_analyticAt_or :
  MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ (↑n : WithTop ℤ) < 0 ∧ f x = 0
h₂ : (↑n : WithTop ℤ) < 0
mpr :
  ∀ (g : 𝕜 → E) (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0) (h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z),
    ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g

Tactic:
obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_eq_int_iff h₁).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 : 𝕜
h₁ : MeromorphicAt f x
h₃ : f x = 0
n : ℤ
hn : (↑n : WithTop ℤ) = meromorphicOrderAt f x
meromorphicNFAt_iff_analyticAt_or :
  MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ (↑n : WithTop ℤ) < 0 ∧ f x = 0
h₂ : (↑n : WithTop ℤ) < 0
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 : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 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 : 𝕜
h₁ : MeromorphicAt f x
h₃ : f x = 0
n : ℤ
hn : (↑n : WithTop ℤ) = meromorphicOrderAt f x
meromorphicNFAt_iff_analyticAt_or :
  MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ (↑n : WithTop ℤ) < 0 ∧ f x = 0
h₂ : (↑n : WithTop ℤ) < 0
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 :
  ∀ (a : 𝕜),
    (Membership.mem (γ := Set 𝕜) {x}ᶜ a → f a = (a - x) ^ n • g a) →
      f a = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) a
⊢ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g

Tactic:
filter_upwards [eventually_nhdsWithin_iff.1 h₃g]

Premises used: eventually_nhdsWithin_iff, 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 : 𝕜
h₁ : MeromorphicAt f x
h₃ : f x = 0
n : ℤ
hn : (↑n : WithTop ℤ) = meromorphicOrderAt f x
meromorphicNFAt_iff_analyticAt_or :
  MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ (↑n : WithTop ℤ) < 0 ∧ f x = 0
h₂ : (↑n : WithTop ℤ) < 0
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = (z - x) ^ n • g z
pos : ∀ (h₁z : z = x), f z = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) z
neg : ∀ (h₁z : ¬z = x), f z = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) z
⊢ f z = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) z

Tactic:
by_cases h₁z : 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 : 𝕜
h₁ : MeromorphicAt f x
h₃ : f x = 0
n : ℤ
hn : (↑n : WithTop ℤ) = meromorphicOrderAt f x
meromorphicNFAt_iff_analyticAt_or :
  MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ (↑n : WithTop ℤ) < 0 ∧ f x = 0
h₂ : (↑n : WithTop ℤ) < 0
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = (z - x) ^ n • g z
h₁z : z = x
pos : f x = HPow.hPow (α := 𝕜) 0 n • g x
⊢ f z = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) z

Tactic:
simp only [h₁z, Pi.smul_apply', Pi.pow_apply, sub_self]

Premises used: sub_self, Pi.smul_apply', 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 : 𝕜
h₁ : MeromorphicAt f x
h₃ : f x = 0
n : ℤ
hn : (↑n : WithTop ℤ) = meromorphicOrderAt f x
meromorphicNFAt_iff_analyticAt_or :
  MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ (↑n : WithTop ℤ) < 0 ∧ f x = 0
h₂ : (↑n : WithTop ℤ) < 0
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = (z - x) ^ n • g z
h₁z : z = x
pos : 0 = HPow.hPow (α := 𝕜) 0 n • g x
⊢ f x = HPow.hPow (α := 𝕜) 0 n • g x

Tactic:
rw [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 : 𝕜
h₁ : MeromorphicAt f x
h₃ : f x = 0
n : ℤ
hn : (↑n : WithTop ℤ) = meromorphicOrderAt f x
meromorphicNFAt_iff_analyticAt_or :
  MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ (↑n : WithTop ℤ) < 0 ∧ f x = 0
h₂ : (↑n : WithTop ℤ) < 0
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = (z - x) ^ n • g z
h₁z : z = x
apply : n ≠ 0
⊢ 0 = HPow.hPow (α := 𝕜) 0 n • g x

Tactic:
apply (smul_eq_zero_of_left (zero_zpow n _) (g x)).symm

Premises used: zero_zpow, smul_eq_zero_of_left, 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 : 𝕜
h₁ : MeromorphicAt f x
h₃ : f x = 0
n : ℤ
hn : (↑n : WithTop ℤ) = meromorphicOrderAt f x
meromorphicNFAt_iff_analyticAt_or :
  MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ (↑n : WithTop ℤ) < 0 ∧ f x = 0
h₂ : (↑n : WithTop ℤ) < 0
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = (z - x) ^ n • g z
h₁z : z = x
by_contra : ∀ (hCon : n = 0), False
⊢ n ≠ 0

Tactic:
by_contra hCon
-- 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 : 𝕜
h₁ : MeromorphicAt f x
h₃ : f x = 0
n : ℤ
hn : (↑n : WithTop ℤ) = meromorphicOrderAt f x
meromorphicNFAt_iff_analyticAt_or :
  MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ (↑n : WithTop ℤ) < 0 ∧ f x = 0
h₂ : (↑n : WithTop ℤ) < 0
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = (z - x) ^ n • g z
h₁z : z = x
hCon : n = 0
⊢ False

Tactic:
simp [hCon] at 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 : 𝕜
h₁ : MeromorphicAt f x
h₃ : f x = 0
n : ℤ
hn : (↑n : WithTop ℤ) = meromorphicOrderAt f x
meromorphicNFAt_iff_analyticAt_or :
  MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ (↑n : WithTop ℤ) < 0 ∧ f x = 0
h₂ : (↑n : WithTop ℤ) < 0
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = (z - x) ^ n • g z
h₁z : ¬z = x
⊢ f z = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) z

Tactic:
hz h₁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 : 𝕜
h₁ : MeromorphicAt f x
h₃ : f x = 0
n : ℤ
hn : (↑n : WithTop ℤ) = meromorphicOrderAt f x
meromorphicNFAt_iff_analyticAt_or :
  MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ (↑n : WithTop ℤ) < 0 ∧ f x = 0
h₂ : (↑n : WithTop ℤ) < 0
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = (z - x) ^ n • g z
h₁z : ¬z = x
⊢ f z = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) z

Tactic:
exact hz h₁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
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0

Tactic:
rw [meromorphicNFAt_iff_analyticAt_or] at hf

Premises used: meromorphicNFAt_iff_analyticAt_or
-- 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 : AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
inl : ∀ (h : AnalyticAt 𝕜 f x), MeromorphicAt f x
inr : ∀ (h : MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0), MeromorphicAt f x
⊢ MeromorphicAt f x

Tactic:
rcases hf with h | 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 : 𝕜
h : AnalyticAt 𝕜 f x
⊢ MeromorphicAt f x

Tactic:
h.meromorphicAt

Premises used: AnalyticAt.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 : 𝕜
h : AnalyticAt 𝕜 f x
⊢ MeromorphicAt f x

Tactic:
exact h.meromorphicAt

Premises used: AnalyticAt.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 : 𝕜
h : MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
⊢ MeromorphicAt f x

Tactic:
obtain ⟨hf, _⟩ := 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 : 𝕜
h : MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
hf : MeromorphicAt f x
⊢ meromorphicOrderAt f x < 0 ∧ f x = 0

Tactic:
obtain ⟨hf, _⟩ := 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 : 𝕜
hf : MeromorphicAt f x
right : meromorphicOrderAt f x < 0 ∧ f x = 0
⊢ MeromorphicAt f x

Tactic:
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 : MeromorphicAt f x
right : meromorphicOrderAt f x < 0 ∧ f x = 0
⊢ MeromorphicAt f x

Tactic:
exact 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
mp : 0 ≤ meromorphicOrderAt f x → AnalyticAt 𝕜 f x
mpr : AnalyticAt 𝕜 f x → 0 ≤ meromorphicOrderAt f x
⊢ 0 ≤ meromorphicOrderAt f x ↔ AnalyticAt 𝕜 f x

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
x : 𝕜
hf : MeromorphicNFAt f x
h₂f : 0 ≤ meromorphicOrderAt f x
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0

Tactic:
rw [meromorphicNFAt_iff_analyticAt_or] at hf

Premises used: meromorphicNFAt_iff_analyticAt_or
-- 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₂f : 0 ≤ meromorphicOrderAt f x
hf₁ : AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
⊢ 0 ≤ meromorphicOrderAt f x

Tactic:
rw [meromorphicNFAt_iff_analyticAt_or] at hf

Premises used: meromorphicNFAt_iff_analyticAt_or