awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
h₁f : ∀ (i : ι), MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | f σ x = 0}
pos : ∀ (h₃f : Function.HasFiniteMulSupport f), MeromorphicNFAt (E := 𝕜) (∏ᶠ (i : ι), f i) x
neg : ∀ (h₃f : ¬Function.HasFiniteMulSupport f), MeromorphicNFAt (E := 𝕜) (∏ᶠ (i : ι), f i) x
⊢ MeromorphicNFAt (E := 𝕜) (∏ᶠ (i : ι), f i) x

Tactic:
by_cases h₃f : Function.HasFiniteMulSupport f

Premises used: Function.HasFiniteMulSupport
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
h₁f : ∀ (i : ι), MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | f σ x = 0}
h₃f : Function.HasFiniteMulSupport f
pos : MeromorphicNFAt (E := 𝕜) (∏ i ∈ Set.Finite.toFinset (s := Function.mulSupport f) h₃f, f i) x
⊢ MeromorphicNFAt (E := 𝕜) (∏ᶠ (i : ι), f i) x

Tactic:
simp_rw [finprod_eq_prod f h₃f]

Premises used: finprod_eq_prod
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
h₁f : ∀ (i : ι), MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | f σ x = 0}
h₃f : Function.HasFiniteMulSupport f
⊢ ∀ i ∈ Set.Finite.toFinset (s := Function.mulSupport f) h₃f, MeromorphicNFAt (f i) x

Tactic:
aesop
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
h₁f : ∀ (i : ι), MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | f σ x = 0}
h₃f : Function.HasFiniteMulSupport f
x_1 : ι
h : Membership.mem (γ := Set ι) {σ : ι | σ ∈ Set.Finite.toFinset (s := Function.mulSupport f) h₃f ∧ f σ x = 0} x_1
x_2 : ι
h_1 : Membership.mem (γ := Set ι) {σ : ι | σ ∈ Set.Finite.toFinset (s := Function.mulSupport f) h₃f ∧ f σ x = 0} x_2
⊢ x_1 = x_2

Tactic:
aesop
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
h₁f : ∀ (i : ι), MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | f σ x = 0}
h₃f : Function.HasFiniteMulSupport f
⊢ MeromorphicNFAt (E := 𝕜) (∏ i ∈ Set.Finite.toFinset (s := Function.mulSupport f) h₃f, f i) x

Tactic:
exact meromorphicNFAt_prod (by aesop) (fun _ _ _ _ ↦ by aesop)

Premises used: meromorphicNFAt_prod
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
h₁f : ∀ (i : ι), MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | f σ x = 0}
h₃f : ¬Function.HasFiniteMulSupport f
⊢ MeromorphicNFAt (E := 𝕜) (∏ᶠ (i : ι), f i) x

Tactic:
finprod_of_not_hasFiniteMulSupport h₃f ▸ analyticAt_const.meromorphicNFAt

Premises used: Eq.rec, finprod_of_not_hasFiniteMulSupport, analyticAt_const, AnalyticAt.meromorphicNFAt, Eq.symm
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
h₁f : ∀ (i : ι), MeromorphicNFAt (f i) x
h₂f : Set.Subsingleton.{u_3} (α := ι) {σ : ι | f σ x = 0}
h₃f : ¬Function.HasFiniteMulSupport f
⊢ MeromorphicNFAt (E := 𝕜) (∏ᶠ (i : ι), f i) x

Tactic:
exact finprod_of_not_hasFiniteMulSupport h₃f ▸ analyticAt_const.meromorphicNFAt
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hf : MeromorphicNFAt f x
pos : ∀ (hn : n = 0), MeromorphicNFAt (f ^ n) x
neg : ∀ (hn : ¬n = 0), MeromorphicNFAt (f ^ n) x
⊢ MeromorphicNFAt (f ^ n) x

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hf : MeromorphicNFAt f x
hn : n = 0
pos : MeromorphicNFAt (E := 𝕜) 1 x
⊢ MeromorphicNFAt (f ^ n) x

Tactic:
simp_all only [zpow_zero]

Premises used: zpow_zero
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hf : MeromorphicNFAt f x
hn : n = 0
pos : AnalyticAt 𝕜 (F := 𝕜) 1 x
⊢ MeromorphicNFAt (E := 𝕜) 1 x

Tactic:
apply AnalyticAt.meromorphicNFAt

Premises used: AnalyticAt.meromorphicNFAt
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hf : MeromorphicNFAt f x
hn : n = 0
⊢ AnalyticAt 𝕜 (F := 𝕜) 1 x

Tactic:
apply analyticAt_const

Premises used: analyticAt_const
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hf : MeromorphicNFAt f x
hn : ¬n = 0
neg : ∀ (hf : f =ᶠ[𝓝 x] 0), MeromorphicNFAt (f ^ n) x
neg₁ :
  ∀
    (hf :
      ∃ (n : ℤ) (g : 𝕜 → 𝕜),
        AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g),
    MeromorphicNFAt (f ^ n) x
⊢ MeromorphicNFAt (f ^ n) x

Tactic:
rcases hf with hf | hf
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
hf : f =ᶠ[𝓝 x] 0
neg : f ^ n =ᶠ[𝓝 x] 0
⊢ MeromorphicNFAt (f ^ n) x

Tactic:
left
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
hf : f =ᶠ[𝓝 x] 0
h : ∀ (z : 𝕜) (hz : f z = 0 z), (f ^ n) z = 0 z
⊢ f ^ n =ᶠ[𝓝 x] 0

Tactic:
filter_upwards [hf] with z hz
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
hf : f =ᶠ[𝓝 x] 0
z : 𝕜
hz : f z = 0 z
⊢ (f ^ n) z = 0 z

Tactic:
simp_all only [Pi.zero_apply, Pi.pow_apply, zero_zpow n hn]

Premises used: zero_zpow, Pi.zero_apply, Pi.pow_apply
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
hf :
  ∃ (n : ℤ) (g : 𝕜 → 𝕜), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
neg :
  ∀ (m : ℤ) (g : 𝕜 → 𝕜) (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0)
    (h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) m • g), MeromorphicNFAt (f ^ n) x
⊢ MeromorphicNFAt (f ^ n) x

Tactic:
obtain ⟨m, g, h₁g, h₂g, h₃g⟩ := hf
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
m : ℤ
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) m • g
neg :
  ∃ (n_1 : ℤ) (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f ^ n =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n_1 • g
⊢ MeromorphicNFAt (f ^ n) x

Tactic:
right
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
m : ℤ
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) m • g
right : (g ^ n) x ≠ 0 ∧ f ^ n =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n * m) • g ^ n
⊢ ∃ (n_1 : ℤ) (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f ^ n =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n_1 • g

Tactic:
use n * m, g ^ n, h₁g.zpow h₂g

Premises used: AnalyticAt.zpow
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
m : ℤ
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) m • g
right : (g ^ n) x ≠ 0
right₁ : f ^ n =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n * m) • g ^ n
⊢ (g ^ n) x ≠ 0 ∧ f ^ n =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n * m) • g ^ n

Tactic:
constructor
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
m : ℤ
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) m • g
right : g x ^ n ≠ 0
⊢ (g ^ n) x ≠ 0

Tactic:
rw [Pi.pow_apply]

Premises used: Pi.pow_apply
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
m : ℤ
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) m • g
⊢ g x ^ n ≠ 0

Tactic:
zpow_ne_zero n h₂g

Premises used: zpow_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
m : ℤ
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) m • g
⊢ g x ^ n ≠ 0

Tactic:
exact zpow_ne_zero n h₂g

Premises used: zpow_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
m : ℤ
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) m • g
h :
  ∀ (z : 𝕜) (hz : f z = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) m • g) z),
    (f ^ n) z = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n * m) • g ^ n) z
⊢ f ^ n =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n * m) • g ^ n

Tactic:
filter_upwards [h₃g] with z hz
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
m : ℤ
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) m • g
z : 𝕜
hz : f z = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) m • g) z
⊢ (f ^ n) z = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (n * m) • g ^ n) z

Tactic:
simp [hz, mul_zpow, (zpow_mul' (z - x) n m).symm]

Premises used: zpow_mul', HSub.hSub, mul_zpow, Eq.symm
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicNFAt f x
inl : ∀ (h : f =ᶠ[𝓝 x] 0), MeromorphicNFAt f⁻¹ x
inr :
  ∀ (n : ℤ) (g : 𝕜 → 𝕜) (h₁ : AnalyticAt 𝕜 g x) (h₂ : g x ≠ 0)
    (h₃ : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g), MeromorphicNFAt f⁻¹ x
⊢ MeromorphicNFAt f⁻¹ x

Tactic:
rcases hf with h | ⟨n, g, h₁, h₂, h₃⟩
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h : f =ᶠ[𝓝 x] 0
inl : f⁻¹ =ᶠ[𝓝 x] 0
⊢ MeromorphicNFAt f⁻¹ x

Tactic:
left
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h : f =ᶠ[𝓝 x] 0
h₁ : ∀ (x : 𝕜) (hx : f x = 0 x), f⁻¹ x = 0 x
⊢ f⁻¹ =ᶠ[𝓝 x] 0

Tactic:
filter_upwards [h] with x hx
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x_1 : 𝕜
f : 𝕜 → 𝕜
h : f =ᶠ[𝓝 x_1] 0
x : 𝕜
hx : f x = 0 x
⊢ f⁻¹ x = 0 x

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
n : ℤ
g : 𝕜 → 𝕜
h₁ : AnalyticAt 𝕜 g x
h₂ : g x ≠ 0
h₃ : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
inr :
  ∃ (n : ℤ) (g : 𝕜 → 𝕜), 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 𝕜
x : 𝕜
f : 𝕜 → 𝕜
n : ℤ
g : 𝕜 → 𝕜
h₁ : AnalyticAt 𝕜 g x
h₂ : g x ≠ 0
h₃ : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ g⁻¹ x ≠ 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
n : ℤ
g : 𝕜 → 𝕜
h₁ : AnalyticAt 𝕜 g x
h₂ : g x ≠ 0
h₃ : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
right : f⁻¹ =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-n) • g⁻¹
⊢ ∃ (n : ℤ) (g : 𝕜 → 𝕜), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f⁻¹ =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g

Tactic:
use -n, g⁻¹, h₁.inv h₂, (by simp_all)

Premises used: AnalyticAt.inv
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
n : ℤ
g : 𝕜 → 𝕜
h₁ : AnalyticAt 𝕜 g x
h₂ : g x ≠ 0
h₃ : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
h :
  ∀ (y : 𝕜) (hy : f y = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) y),
    f⁻¹ y = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-n) • g⁻¹) y
⊢ f⁻¹ =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-n) • g⁻¹

Tactic:
filter_upwards [h₃] with y hy
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
n : ℤ
g : 𝕜 → 𝕜
h₁ : AnalyticAt 𝕜 g x
h₂ : g x ≠ 0
h₃ : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
y : 𝕜
hy : f y = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) y
h : (g y)⁻¹ * ((y - x) ^ n)⁻¹ = ((y - x) ^ n)⁻¹ * (g y)⁻¹
⊢ f⁻¹ y = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-n) • g⁻¹) y

Tactic:
simp only [Pi.inv_apply, hy, Pi.smul_apply', Pi.pow_apply, smul_eq_mul, mul_inv_rev, zpow_neg]

Premises used: Pi.smul_apply', Pi.pow_apply, zpow_neg, mul_inv_rev, smul_eq_mul, Pi.inv_apply
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
n : ℤ
g : 𝕜 → 𝕜
h₁ : AnalyticAt 𝕜 g x
h₂ : g x ≠ 0
h₃ : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
y : 𝕜
hy : f y = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) y
⊢ (g y)⁻¹ * ((y - x) ^ n)⁻¹ = ((y - x) ^ n)⁻¹ * (g y)⁻¹

Tactic:
ring
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
x : 𝕜
hf : AnalyticAt 𝕜 f x
hg : MeromorphicNFAt g x
hor : g x ≠ 0 ∨ f x ≠ 0
rw : MeromorphicNFAt (f * g⁻¹) x
⊢ MeromorphicNFAt (f / g) x

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
x : 𝕜
hf : AnalyticAt 𝕜 f x
hg : MeromorphicNFAt g x
hor : g x ≠ 0 ∨ f x ≠ 0
inl : ∀ (hgne : g x ≠ 0), MeromorphicNFAt (f * g⁻¹) x
inr : ∀ (hfne : f x ≠ 0), MeromorphicNFAt (f * g⁻¹) x
⊢ MeromorphicNFAt (f * g⁻¹) x

Tactic:
rcases hor with hgne | hfne
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
x : 𝕜
hf : AnalyticAt 𝕜 f x
hg : MeromorphicNFAt g x
hgne : g x ≠ 0
⊢ MeromorphicNFAt f x

Tactic:
have hf := hf.meromorphicNFAt
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
x : 𝕜
hf_1 : AnalyticAt 𝕜 f x
hg : MeromorphicNFAt g x
hgne : g x ≠ 0
hf : MeromorphicNFAt f x
⊢ AnalyticAt 𝕜 g x

Tactic:
grind [meromorphicNFAt_iff_analyticAt_or]

Premises used: meromorphicNFAt_iff_analyticAt_or
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
x : 𝕜
hf_1 : AnalyticAt 𝕜 f x
hg : MeromorphicNFAt g x
hgne : g x ≠ 0
hf : MeromorphicNFAt f x
⊢ AnalyticAt 𝕜 g x

Tactic:
have hgAnalytic : AnalyticAt 𝕜 g x := by grind [meromorphicNFAt_iff_analyticAt_or]
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
x : 𝕜
hf_1 : AnalyticAt 𝕜 f x
hg : MeromorphicNFAt g x
hgne : g x ≠ 0
hf : MeromorphicNFAt f x
hgAnalytic : AnalyticAt 𝕜 g x
⊢ AnalyticAt 𝕜 g⁻¹ x

Tactic:
have hgInvAnalytic : AnalyticAt 𝕜 g⁻¹ x := hgAnalytic.inv hgne
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
x : 𝕜
hf_1 : AnalyticAt 𝕜 f x
hg : MeromorphicNFAt g x
hgne : g x ≠ 0
hf : MeromorphicNFAt f x
hgAnalytic : AnalyticAt 𝕜 g x
hgInvAnalytic : AnalyticAt 𝕜 g⁻¹ x
inl inl₁ inl₂ inl₃ :
  ∀ (hf : MeromorphicNFAt (f * g⁻¹) x) (hgAnalytic : AnalyticAt 𝕜 g x) (hgInvAnalytic : AnalyticAt 𝕜 g⁻¹ x),
    MeromorphicNFAt (f * g⁻¹) x
⊢ MeromorphicNFAt (f * g⁻¹) x

Tactic:
rwa [← meromorphicNFAt_mul_iff_left hgInvAnalytic (inv_ne_zero hgne)] at hf

Premises used: meromorphicNFAt_mul_iff_left, inv_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
x : 𝕜
hf : AnalyticAt 𝕜 f x
hg : MeromorphicNFAt g x
hfne : f x ≠ 0
⊢ MeromorphicNFAt (f * g⁻¹) x

Tactic:
grind [meromorphicNFAt_mul_iff_right, hg.inv]

Premises used: meromorphicNFAt_mul_iff_right, MeromorphicNFAt.inv
-- 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
g : 𝕜 → 𝕜
x : 𝕜
U : Set 𝕜
pos : (hf : MeromorphicAt f x) → 𝕜 → E
neg : (hf : ¬MeromorphicAt f x) → 𝕜 → E
⊢ 𝕜 → E

Tactic:
by_cases hf : MeromorphicAt f x

Premises used: 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
g : 𝕜 → 𝕜
x : 𝕜
U : Set 𝕜
hf : MeromorphicAt f x
pos : E
⊢ 𝕜 → E

Tactic:
apply Function.update f x

Premises used: Function.update
-- 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
g : 𝕜 → 𝕜
x : 𝕜
U : Set 𝕜
hf : MeromorphicAt f x
pos : (h₁f : meromorphicOrderAt f x = (↑0 : WithTop ℤ)) → E
neg : (h₁f : ¬meromorphicOrderAt f x = (↑0 : WithTop ℤ)) → E
⊢ E

Tactic:
by_cases h₁f : meromorphicOrderAt f x = (0 : ℤ)

Premises used: meromorphicOrderAt, OfNat.ofNat
-- 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
g : 𝕜 → 𝕜
x : 𝕜
U : Set 𝕜
hf : MeromorphicAt f x
h₁f : meromorphicOrderAt f x = (↑0 : WithTop ℤ)
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • g z

Tactic:
rw [meromorphicOrderAt_eq_int_iff hf] at h₁f

Premises used: meromorphicOrderAt_eq_int_iff
-- 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
g : 𝕜 → 𝕜
x : 𝕜
U : Set 𝕜
hf : MeromorphicAt f x
h₁f : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • g z
⊢ E

Tactic:
exact (Classical.choose h₁f) x

Premises used: Classical.choose
-- 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
g : 𝕜 → 𝕜
x : 𝕜
U : Set 𝕜
hf : MeromorphicAt f x
h₁f : ¬meromorphicOrderAt f x = (↑0 : WithTop ℤ)
⊢ E

Tactic:
exact 0
-- 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
g : 𝕜 → 𝕜
x : 𝕜
U : Set 𝕜
hf : MeromorphicAt f x
pos : E
pos₁ : (h₁f : meromorphicOrderAt f x = (↑0 : WithTop ℤ)) → E
neg neg₁ : (h₁f : ¬meromorphicOrderAt f x = (↑0 : WithTop ℤ)) → E
⊢ 𝕜 → E

Tactic:
classical -- do not complain about decidability issues in Function.update
    apply Function.update f x
    by_cases h₁f : meromorphicOrderAt f x = (0 : ℤ)
    · rw [meromorphicOrderAt_eq_int_iff hf] at h₁f
      exact (Classical.choose h₁f) x
    · exact 0

Premises used: meromorphicOrderAt, meromorphicOrderAt_eq_int_iff, OfNat.ofNat
-- 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
g : 𝕜 → 𝕜
x : 𝕜
U : Set 𝕜
hf : ¬MeromorphicAt f x
⊢ 𝕜 → E

Tactic:
exact 0
-- 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
x_1 : 𝕜
h : Membership.mem (γ := Set 𝕜) {x}ᶜ x_1
⊢ f x_1 = toMeromorphicNFAt f x x_1

Tactic:
simp_all [toMeromorphicNFAt]

Premises used: 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
⊢ toMeromorphicNFAt f x = 0

Tactic:
simp [toMeromorphicNFAt, hf]

Premises used: 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
⊢ f =ᶠ[𝓝[≠] x] toMeromorphicNFAt f x

Tactic:
eventually_nhdsWithin_of_forall (fun _ hz ↦ hf.eqOn_compl_singleton_toMeromorphicNFAt hz)

Premises used: Filter.EventuallyEq, MeromorphicAt.eqOn_compl_singleton_toMeromorphicNFAt, eventually_nhdsWithin_of_forall
-- 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 : 𝕜
pos : ∀ (hf : MeromorphicAt f x), MeromorphicNFAt (toMeromorphicNFAt f x) x
neg : ∀ (hf : ¬MeromorphicAt f x), MeromorphicNFAt (toMeromorphicNFAt f x) x
⊢ MeromorphicNFAt (toMeromorphicNFAt f x) x

Tactic:
by_cases hf : MeromorphicAt f x

Premises used: 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 : 𝕜
hf : MeromorphicAt f x
pos : ∀ (h₂f : meromorphicOrderAt f x = ⊤), MeromorphicNFAt (toMeromorphicNFAt f x) x
neg : ∀ (h₂f : ¬meromorphicOrderAt f x = ⊤), MeromorphicNFAt (toMeromorphicNFAt f x) x
⊢ MeromorphicNFAt (toMeromorphicNFAt f x) x

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

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
h₂f : meromorphicOrderAt f x = ⊤
h₁ : toMeromorphicNFAt f x =ᶠ[𝓝[≠] x] 0
h₂ : toMeromorphicNFAt f x x = 0 x
⊢ toMeromorphicNFAt f x =ᶠ[𝓝 x] 0

Tactic:
apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE

Premises used: eventuallyEq_nhds_of_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
h₂f : meromorphicOrderAt f x = ⊤
⊢ toMeromorphicNFAt f x =ᶠ[𝓝[≠] x] 0

Tactic:
hf.eq_nhdsNE_toMeromorphicNFAt.symm.trans (meromorphicOrderAt_eq_top_iff.1 h₂f)

Premises used: Filter.EventuallyEq.trans, MeromorphicAt.eq_nhdsNE_toMeromorphicNFAt, meromorphicOrderAt_eq_top_iff, Iff.mp, 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
h₂f : meromorphicOrderAt f x = ⊤
⊢ toMeromorphicNFAt f x =ᶠ[𝓝[≠] x] 0

Tactic:
exact hf.eq_nhdsNE_toMeromorphicNFAt.symm.trans (meromorphicOrderAt_eq_top_iff.1 h₂f)

Premises used: Filter.EventuallyEq.trans, MeromorphicAt.eq_nhdsNE_toMeromorphicNFAt, meromorphicOrderAt_eq_top_iff, Iff.mp, 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
h₂f : meromorphicOrderAt f x = ⊤
⊢ toMeromorphicNFAt f x x = 0 x

Tactic:
simp [h₂f, toMeromorphicNFAt, hf]

Premises used: 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
h₂f : meromorphicOrderAt f x = ⊤
⊢ toMeromorphicNFAt f x =ᶠ[𝓝 x] 0

Tactic:
have : toMeromorphicNFAt f x =ᶠ[𝓝 x] 0 := by
        apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE
        · exact hf.eq_nhdsNE_toMeromorphicNFAt.symm.trans (meromorphicOrderAt_eq_top_iff.1 h₂f)
        · simp [h₂f, toMeromorphicNFAt, hf]