awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.Order
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
hn : analyticOrderAt f x = ⊤
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0

Tactic:
exact (analyticOrderAt_eq_top.mp hn).filter_mono nhdsWithin_le_nhds

Premises used: Filter.Eventually.filter_mono, analyticOrderAt_eq_top, nhdsWithin_le_nhds, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Order
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
a : ℕ
hn : analyticOrderAt f x = (↑a : ℕ∞)
coe : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ a • g z
⊢ meromorphicOrderAt f x = ENat.map Nat.cast (↑a : ℕ∞)

Tactic:
simp_rw [ENat.map_coe, meromorphicOrderAt_eq_int_iff hf.meromorphicAt, zpow_natCast]

Premises used: zpow_natCast, meromorphicOrderAt_eq_int_iff, ENat.map_coe, AnalyticAt.meromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Order
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
a : ℕ
hn : analyticOrderAt f x = (↑a : ℕ∞)
coe :
  ∀ (g : 𝕜 → E) (h1 : AnalyticAt 𝕜 g x) (h2 : g x ≠ 0) (h3 : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ a • g z),
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ a • g z
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ a • g z

Tactic:
rcases hf.analyticOrderAt_eq_natCast.mp hn with ⟨g, h1, h2, h3⟩

Premises used: AnalyticAt.analyticOrderAt_eq_natCast, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Order
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
a : ℕ
hn : analyticOrderAt f x = (↑a : ℕ∞)
g : 𝕜 → E
h1 : AnalyticAt 𝕜 g x
h2 : g x ≠ 0
h3 : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ a • g z
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ a • g z

Tactic:
⟨g, h1, h2, h3.filter_mono nhdsWithin_le_nhds⟩

Premises used: Filter.Eventually.filter_mono, nhdsWithin_le_nhds, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Meromorphic.Order
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
a : ℕ
hn : analyticOrderAt f x = (↑a : ℕ∞)
g : 𝕜 → E
h1 : AnalyticAt 𝕜 g x
h2 : g x ≠ 0
h3 : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ a • g z
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ a • g z

Tactic:
exact ⟨g, h1, h2, h3.filter_mono nhdsWithin_le_nhds⟩
-- Module: Mathlib.Analysis.Meromorphic.Order
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
⊢ 0 ≤ meromorphicOrderAt f x

Tactic:
simp [hf.meromorphicOrderAt_eq]

Premises used: AnalyticAt.meromorphicOrderAt_eq
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ContinuousAt f x
ho : meromorphicOrderAt f x = ⊤
⊢ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x : 𝕜) ↦ 0) x

Tactic:
have : AnalyticAt 𝕜 (fun _ ↦ (0 : E)) x := analyticAt_const
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ContinuousAt f x
ho : meromorphicOrderAt f x = ⊤
this : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x : 𝕜) ↦ 0) x
top : (fun (x : 𝕜) ↦ 0) =ᶠ[𝓝 x] f
⊢ AnalyticAt 𝕜 f x

Tactic:
apply this.congr

Premises used: AnalyticAt.congr
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ContinuousAt f x
ho : meromorphicOrderAt f x = ⊤
this : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x : 𝕜) ↦ 0) x
top : (fun (x : 𝕜) ↦ 0) =ᶠ[𝓝[≠] x] f
⊢ (fun (x : 𝕜) ↦ 0) =ᶠ[𝓝 x] f

Tactic:
rw [← ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE continuousAt_const h']

Premises used: continuousAt_const, ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ContinuousAt f x
ho : meromorphicOrderAt f x = ⊤
this : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x : 𝕜) ↦ 0) x
y : 𝕜
hy : f y = 0
⊢ 0 = f y

Tactic:
simp [hy]
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ContinuousAt f x
ho : meromorphicOrderAt f x = ⊤
this : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x : 𝕜) ↦ 0) x
h₁ :
  ∀ (a : 𝕜),
    Membership.mem (γ := Set 𝕜)
      {x : 𝕜 |
        Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (z : 𝕜) ↦ f z = 0) x} x →
          Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (x : 𝕜) ↦ (fun (x : 𝕜) ↦ (0 : E)) x = f x) x} x}
      a
h₂ h₃ : ∀ (y : 𝕜) (hy : f y = 0), 0 = f y
⊢ (fun (x : 𝕜) ↦ 0) =ᶠ[𝓝[≠] x] f

Tactic:
filter_upwards [meromorphicOrderAt_eq_top_iff.1 ho] with y hy using by simp [hy]

Premises used: meromorphicOrderAt_eq_top_iff, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ContinuousAt f x
n : ℤ
ho : meromorphicOrderAt f x = (↑n : WithTop ℤ)
coe :
  ∀ (g : 𝕜 → E) (g_an : AnalyticAt 𝕜 g x) (gx : g x ≠ 0) (hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z),
    AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 f x

Tactic:
rcases (meromorphicOrderAt_eq_int_iff h).1 ho with ⟨g, g_an, gx, hg⟩

Premises used: meromorphicOrderAt_eq_int_iff, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ContinuousAt f x
n : ℤ
ho : meromorphicOrderAt f x = (↑n : WithTop ℤ)
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
apply : ∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ 0 ≤ meromorphicOrderAt f x

Tactic:
apply (tendsto_nhds_iff_meromorphicOrderAt_nonneg h).1

Premises used: tendsto_nhds_iff_meromorphicOrderAt_nonneg, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ContinuousAt f x
n : ℤ
ho : meromorphicOrderAt f x = (↑n : WithTop ℤ)
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ ∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)

Tactic:
⟨f x, h'.continuousWithinAt.tendsto⟩

Premises used: ContinuousAt.continuousWithinAt, Exists.intro, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ContinuousAt f x
n : ℤ
ho : meromorphicOrderAt f x = (↑n : WithTop ℤ)
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ ∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)

Tactic:
exact ⟨f x, h'.continuousWithinAt.tendsto⟩
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ContinuousAt f x
n : ℤ
ho : meromorphicOrderAt f x = (↑n : WithTop ℤ)
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ 0 ≤ meromorphicOrderAt f x

Tactic:
have : 0 ≤ meromorphicOrderAt f x := by
      apply (tendsto_nhds_iff_meromorphicOrderAt_nonneg h).1
      exact ⟨f x, h'.continuousWithinAt.tendsto⟩
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ContinuousAt f x
n : ℤ
ho : meromorphicOrderAt f x = (↑n : WithTop ℤ)
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
this : 0 ≤ meromorphicOrderAt f x
⊢ 0 ≤ n

Tactic:
simpa [ho] using this
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ContinuousAt f x
n : ℤ
ho : meromorphicOrderAt f x = (↑n : WithTop ℤ)
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
this : 0 ≤ meromorphicOrderAt f x
coe :
  ∀ (n : ℕ) (ho : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ))
    (hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z), AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 f x

Tactic:
lift n to ℕ using by simpa [ho] using this
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ContinuousAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
this : 0 ≤ meromorphicOrderAt f x
n : ℕ
ho : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
⊢ ContinuousAt.{u_1, u_2} (Y := E) (fun (x_1 : 𝕜) ↦ (x_1 - x) ^ n • g x_1) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ContinuousAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
this : 0 ≤ meromorphicOrderAt f x
n : ℕ
ho : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
apply : (fun (x_1 : 𝕜) ↦ (x_1 - x) ^ n • g x_1) =ᶠ[𝓝[≠] x] f
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ n • g z = f z

Tactic:
apply (ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE (by fun_prop) h').1

Premises used: Iff.mp, ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ContinuousAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
this : 0 ≤ meromorphicOrderAt f x
n : ℕ
ho : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
z : 𝕜
hz : f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
⊢ (z - x) ^ n • g z = f z

Tactic:
simpa using hz.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ContinuousAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
this : 0 ≤ meromorphicOrderAt f x
n : ℕ
ho : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
h₁ :
  ∀ (a : 𝕜),
    Membership.mem (γ := Set 𝕜)
      {x_1 : 𝕜 |
        Membership.mem (γ := Set 𝕜) {x_2 : 𝕜 | (fun (z : 𝕜) ↦ f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z) x_2}
            x_1 →
          Membership.mem (γ := Set 𝕜)
            {x_2 : 𝕜 | (fun (x_3 : 𝕜) ↦ (fun (x_4 : 𝕜) ↦ (x_4 - x) ^ n • g x_4) x_3 = f x_3) x_2} x_1}
      a
h₂ h₃ : ∀ (z : 𝕜) (hz : f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z), (z - x) ^ n • g z = f z
⊢ (fun (x_1 : 𝕜) ↦ (x_1 - x) ^ n • g x_1) =ᶠ[𝓝[≠] x] f

Tactic:
filter_upwards [hg] with z hz using by simpa using hz.symm
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ContinuousAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
this : 0 ≤ meromorphicOrderAt f x
n : ℕ
ho : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ n • g z = f z

Tactic:
have A : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ n • g z = f z := by
      apply (ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE (by fun_prop) h').1
      filter_upwards [hg] with z hz using by simpa using hz.symm
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ContinuousAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
this : 0 ≤ meromorphicOrderAt f x
n : ℕ
ho : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
A : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ n • g z = f z
⊢ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x_1 : 𝕜) ↦ (x_1 - x) ^ n • g x_1) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ContinuousAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
this : 0 ≤ meromorphicOrderAt f x
n : ℕ
ho : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
A : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ n • g z = f z
⊢ AnalyticAt 𝕜 f x

Tactic:
exact AnalyticAt.congr (by fun_prop) A

Premises used: AnalyticAt.congr
-- Module: Mathlib.Analysis.Meromorphic.Order
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' : ContinuousAt f x
cases : ∀ (x_1 : WithTop ℤ) (ho : meromorphicOrderAt f x = x_1), AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 f x

Tactic:
cases ho : meromorphicOrderAt f x with
  | top =>
    /- If the order is infinite, then `f` vanishes on a pointed neighborhood of `x`. By continuity,
    it also vanishes at `x`.-/
    have : AnalyticAt 𝕜 (fun _ ↦ (0 : E)) x := analyticAt_const
    apply this.congr
    rw [← ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE continuousAt_const h']
    filter_upwards [meromorphicOrderAt_eq_top_iff.1 ho] with y hy using by simp [hy]
  | coe n =>
    /- If the order is finite, then the order has to be nonnegative, as otherwise the norm of `f`
    would tend to infinity at `x`. Then the local expression of `f` coming from its meromorphicity
    shows that it coincides with an analytic function close to `x`, except maybe at `x`. By
    continuity of `f`, the two functions also coincide at `x`. -/
    rcases (meromorphicOrderAt_eq_int_iff h).1 ho with ⟨g, g_an, gx, hg⟩
    have : 0 ≤ meromorphicOrderAt f x := by
      apply (tendsto_nhds_iff_meromorphicOrderAt_nonneg h).1
      exact ⟨f x, h'.continuousWithinAt.tendsto⟩
    lift n to ℕ using by simpa [ho] using this
    have A : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ n • g z = f z := by
      apply (ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE (by fun_prop) h').1
      filter_upwards [hg] with z hz using by simpa using hz.symm
    exact AnalyticAt.congr (by fun_prop) A

Premises used: meromorphicOrderAt, continuousAt_const, ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : 0 < meromorphicOrderAt f x
hf : f x = 0
⊢ AnalyticAt 𝕜 f x

Tactic:
(meromorphicAt_of_meromorphicOrderAt_ne_zero h.ne').analyticAt ?_

Premises used: MeromorphicAt.analyticAt, LT.lt.ne', meromorphicAt_of_meromorphicOrderAt_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : 0 < meromorphicOrderAt f x
hf : f x = 0
refine : ContinuousAt f x
⊢ AnalyticAt 𝕜 f x

Tactic:
refine (meromorphicAt_of_meromorphicOrderAt_ne_zero h.ne').analyticAt ?_

Premises used: MeromorphicAt.analyticAt, LT.lt.ne', meromorphicAt_of_meromorphicOrderAt_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : 0 < meromorphicOrderAt f x
hf : f x = 0
rw : Tendsto f (𝓝[≠] x) (𝓝 0)
⊢ ContinuousAt f x

Tactic:
rw [continuousAt_iff_punctured_nhds, hf]

Premises used: continuousAt_iff_punctured_nhds
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : 0 < meromorphicOrderAt f x
hf : f x = 0
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)

Tactic:
tendsto_zero_of_meromorphicOrderAt_pos h

Premises used: tendsto_zero_of_meromorphicOrderAt_pos
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : 0 < meromorphicOrderAt f x
hf : f x = 0
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)

Tactic:
exact tendsto_zero_of_meromorphicOrderAt_pos h

Premises used: tendsto_zero_of_meromorphicOrderAt_pos
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
z₀ : 𝕜
e : E
inst_3 : Decidable (e = 0)
pos : ∀ (he : e = 0), meromorphicOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) z₀ = ⊤
neg : ∀ (he : ¬e = 0), meromorphicOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) z₀ = 0
⊢ meromorphicOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) z₀ = if e = 0 then ⊤ else 0

Tactic:
split_ifs with he
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
z₀ : 𝕜
e : E
inst_3 : Decidable (e = 0)
he : e = 0
⊢ meromorphicOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) z₀ = ⊤

Tactic:
simp [he, meromorphicOrderAt_eq_top_iff]

Premises used: meromorphicOrderAt_eq_top_iff
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
z₀ : 𝕜
e : E
inst_3 : Decidable (e = 0)
he : ¬e = 0
⊢ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x : 𝕜) ↦ e) z₀

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
z₀ : 𝕜
e : E
inst_3 : Decidable (e = 0)
he : ¬e = 0
⊢ Ne.{u_2 + 1} (α := E) ((fun (x : 𝕜) ↦ e) z₀) 0 ∧
    ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, e = HSMul.hSMul (β := E) (HPow.hPow (β := ℤ) (z - z₀) 0) ((fun (x : 𝕜) ↦ e) z)

Tactic:
simpa
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
z₀ : 𝕜
e : E
inst_3 : Decidable (e = 0)
he : ¬e = 0
⊢ meromorphicOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) z₀ = 0

Tactic:
exact (meromorphicOrderAt_eq_int_iff (.const e z₀)).2 ⟨fun _ ↦ e, by fun_prop, by simpa⟩

Premises used: Iff.mpr, MeromorphicAt.const, meromorphicOrderAt_eq_int_iff, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
⊢ meromorphicOrderAt.{u_1, u_1} (𝕜 := 𝕜) id 0 = 1

Tactic:
simp [analyticAt_id.meromorphicOrderAt_eq]

Premises used: AnalyticAt.meromorphicOrderAt_eq, analyticAt_id
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z₀ : 𝕜
n : ℤ
inst_1 : Decidable (Eq.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0)
⊢ meromorphicOrderAt (E := 𝕜) (↑n : 𝕜 → 𝕜) z₀ = if Eq.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0 then ⊤ else 0

Tactic:
meromorphicOrderAt_const z₀ (n : 𝕜)

Premises used: Int.cast, meromorphicOrderAt_const
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z₀ : 𝕜
n : ℕ
inst_1 : Decidable (Eq.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0)
⊢ meromorphicOrderAt (E := 𝕜) (↑n : 𝕜 → 𝕜) z₀ = if Eq.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0 then ⊤ else 0

Tactic:
meromorphicOrderAt_const z₀ (n : 𝕜)

Premises used: meromorphicOrderAt_const, Nat.cast
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z₀ : 𝕜
n : ℕ
inst_1 : Decidable (Eq.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0)
⊢ meromorphicOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ (↑n : 𝕜)) z₀ = if Eq.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0 then ⊤ else 0

Tactic:
meromorphicOrderAt_const z₀ (n : 𝕜)

Premises used: meromorphicOrderAt_const, Nat.cast
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z₀ : 𝕜
n : ℕ
inst_1 : Decidable (Eq.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0)
h : ∀ (x : 𝕜), Eq.{u_1 + 1} (α := 𝕜) ((OfNat.ofNat n : 𝕜 → 𝕜) x) (↑n : 𝕜)
⊢ meromorphicOrderAt (E := 𝕜) (OfNat.ofNat n) z₀ = if Eq.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0 then ⊤ else 0

Tactic:
convert! meromorphicOrderAt_const z₀ (n : 𝕜)

Premises used: meromorphicOrderAt_const, Nat.cast
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z₀ : 𝕜
n : ℕ
inst_1 : Decidable (Eq.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0)
x : 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) (OfNat.ofNat n x) (↑n : 𝕜)

Tactic:
simp [Semiring.toGrindSemiring_ofNat 𝕜 n]

Premises used: Semiring.toGrindSemiring_ofNat
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
⊢ MeromorphicAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
rw :
  ∃ (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g x ∧
      g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n z = (z - x) ^ n • g z
⊢ meromorphicOrderAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n) x = (↑n : WithTop ℤ)

Tactic:
rw [meromorphicOrderAt_eq_int_iff (by fun_prop)]

Premises used: meromorphicOrderAt_eq_int_iff
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
⊢ AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ 1) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x,
    HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n z =
      HSMul.hSMul (β := 𝕜) ((z - x) ^ n) ((fun (z : 𝕜) ↦ (1 : 𝕜)) z)

Tactic:
aesop
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
⊢ ∃ (g : 𝕜 → 𝕜),
    AnalyticAt 𝕜 g x ∧
      g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n z = (z - x) ^ n • g z

Tactic:
exact ⟨fun z ↦ 1, by fun_prop, one_ne_zero, by aesop⟩
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
⊢ meromorphicOrderAt (HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) (↑n : ℤ)) x = (↑(↑n : ℤ) : WithTop ℤ)

Tactic:
meromorphicOrderAt_zpow_id_sub_const

Premises used: meromorphicOrderAt_zpow_id_sub_const
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
h :
  HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n =
    HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) (↑n : ℤ)
⊢ meromorphicOrderAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n) x = (↑n : WithTop ℤ)

Tactic:
convert! meromorphicOrderAt_zpow_id_sub_const

Premises used: meromorphicOrderAt_zpow_id_sub_const