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 : 𝕜
ho : meromorphicOrderAt f x < 0
hf : MeromorphicAt f x
m : ℤ
hm : (↑m : WithTop ℤ) = meromorphicOrderAt f x
m_neg : m < 0
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • g z
this : Tendsto (β := 𝕜) (fun (z : 𝕜) ↦ z - x) (𝓝[≠] x) (𝓝[≠] 0)
⊢ Tendsto (β := ℝ) (fun (x_1 : 𝕜) ↦ ‖(x_1 - x) ^ m‖) (𝓝[≠] x) atTop

Tactic:
exact (tendsto_norm_cobounded_atTop.comp (tendsto_zpow_nhdsNE_zero_cobounded m_neg)).comp this

Premises used: tendsto_norm_cobounded_atTop, Filter.Tendsto.comp
-- 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 : 𝕜
ho : meromorphicOrderAt f x < 0
hf : MeromorphicAt f x
m : ℤ
hm : (↑m : WithTop ℤ) = meromorphicOrderAt f x
m_neg : m < 0
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • g z
⊢ Tendsto (β := ℝ) (fun (z : 𝕜) ↦ ‖(z - x) ^ m • g z‖) (𝓝[≠] x) atTop

Tactic:
have A : Tendsto (fun z ↦ ‖(z - x) ^ m • g z‖) (𝓝[≠] x) atTop := by
    simp only [norm_smul]
    apply Filter.Tendsto.atTop_mul_pos (C := ‖g x‖) (by simp [gx]) _
      g_an.continuousAt.continuousWithinAt.tendsto.norm
    have : Tendsto (fun z ↦ z - x) (𝓝[≠] x) (𝓝[≠] 0) := by
      refine tendsto_nhdsWithin_iff.2 ⟨?_, ?_⟩
      · have : ContinuousWithinAt (fun z ↦ z - x) {x}ᶜ x := by fun_prop
        simpa using this.tendsto
      · filter_upwards [self_mem_nhdsWithin] with y hy
        simpa [sub_eq_zero] using hy
    exact (tendsto_norm_cobounded_atTop.comp (tendsto_zpow_nhdsNE_zero_cobounded m_neg)).comp 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 : 𝕜
ho : meromorphicOrderAt f x < 0
hf : MeromorphicAt f x
m : ℤ
hm : (↑m : WithTop ℤ) = meromorphicOrderAt f x
m_neg : m < 0
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • g z
A : Tendsto (β := ℝ) (fun (z : 𝕜) ↦ ‖(z - x) ^ m • g z‖) (𝓝[≠] x) atTop
apply : (𝓝[≠] x).EventuallyEq (β := ℝ) (fun (z : 𝕜) ↦ ‖(z - x) ^ m • g z‖) fun (x : 𝕜) ↦ ‖f x‖
⊢ Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop

Tactic:
apply A.congr'

Premises used: Filter.Tendsto.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 : 𝕜
ho : meromorphicOrderAt f x < 0
hf : MeromorphicAt f x
m : ℤ
hm : (↑m : WithTop ℤ) = meromorphicOrderAt f x
m_neg : m < 0
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • g z
A : Tendsto (β := ℝ) (fun (z : 𝕜) ↦ ‖(z - x) ^ m • g z‖) (𝓝[≠] x) atTop
z : 𝕜
hz : f z = (z - x) ^ m • g z
⊢ ‖(z - x) ^ m • g z‖ = ‖f z‖

Tactic:
simp [hz]
-- 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 : 𝕜
ho : meromorphicOrderAt f x < 0
hf : MeromorphicAt f x
m : ℤ
hm : (↑m : WithTop ℤ) = meromorphicOrderAt f x
m_neg : m < 0
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • g z
A : Tendsto (β := ℝ) (fun (z : 𝕜) ↦ ‖(z - x) ^ m • g z‖) (𝓝[≠] x) atTop
h :
  ∀ (a : 𝕜),
    Membership.mem (γ := Set 𝕜)
      {x_1 : 𝕜 |
        Membership.mem (γ := Set 𝕜) {x_2 : 𝕜 | (fun (z : 𝕜) ↦ f z = (z - x) ^ m • g z) x_2} x_1 →
          Membership.mem (γ := Set 𝕜)
            {x_2 : 𝕜 |
              (fun (x_3 : 𝕜) ↦ Eq (α := ℝ) ((fun (z : 𝕜) ↦ ‖(z - x) ^ m • g z‖) x_3) ((fun (x : 𝕜) ↦ ‖f x‖) x_3)) x_2}
            x_1}
      a
h₁ h₂ : ∀ (z : 𝕜) (hz : f z = (z - x) ^ m • g z), ‖(z - x) ^ m • g z‖ = ‖f z‖
⊢ (𝓝[≠] x).EventuallyEq (β := ℝ) (fun (z : 𝕜) ↦ ‖(z - x) ^ m • g z‖) fun (x : 𝕜) ↦ ‖f x‖

Tactic:
filter_upwards [hg] with z hz using by simp [hz]
-- 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 : MeromorphicAt f x
ho : meromorphicOrderAt f x = 0
rcases :
  ∀ (g : 𝕜 → E) (g_an : AnalyticAt 𝕜 g x) (gx : g x ≠ 0)
    (hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • g z), ∃ (c : E), c ≠ 0 ∧ Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ ∃ (c : E), c ≠ 0 ∧ Tendsto f (𝓝[≠] x) (𝓝 c)

Tactic:
rcases (meromorphicOrderAt_eq_int_iff hf).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 : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x = 0
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • g z
⊢ ∃ (c : E), c ≠ 0 ∧ Tendsto f (𝓝[≠] x) (𝓝 c)

Tactic:
⟨g x, gx, ?_⟩

Premises used: 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 : MeromorphicAt f x
ho : meromorphicOrderAt f x = 0
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • g z
refine : Tendsto f (𝓝[≠] x) (𝓝 (g x))
⊢ ∃ (c : E), c ≠ 0 ∧ Tendsto f (𝓝[≠] x) (𝓝 c)

Tactic:
refine ⟨g x, gx, ?_⟩
-- 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 : MeromorphicAt f x
ho : meromorphicOrderAt f x = 0
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • g z
apply : g =ᶠ[𝓝[≠] x] f
⊢ Tendsto f (𝓝[≠] x) (𝓝 (g x))

Tactic:
apply g_an.continuousAt.continuousWithinAt.tendsto.congr'

Premises used: ContinuousAt.continuousWithinAt, AnalyticAt.continuousAt, Filter.Tendsto.congr', 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 : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x = 0
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • g z
y : 𝕜
hy : f y = HPow.hPow (β := ℤ) (y - x) 0 • g y
⊢ g y = 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 : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x = 0
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • g z
h :
  ∀ (a : 𝕜),
    Membership.mem (γ := Set 𝕜)
      {x_1 : 𝕜 |
        Membership.mem (γ := Set 𝕜) {x_2 : 𝕜 | (fun (z : 𝕜) ↦ f z = HPow.hPow (β := ℤ) (z - x) 0 • g z) x_2} x_1 →
          Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (x : 𝕜) ↦ g x = f x) x} x_1}
      a
h₁ h₂ : ∀ (y : 𝕜) (hy : f y = HPow.hPow (β := ℤ) (y - x) 0 • g y), g y = f y
⊢ g =ᶠ[𝓝[≠] x] f

Tactic:
filter_upwards [hg] with y hy using by 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 : 𝕜
ho : 0 < meromorphicOrderAt f x
⊢ MeromorphicAt f x

Tactic:
have hf : MeromorphicAt f x := meromorphicAt_of_meromorphicOrderAt_ne_zero ho.ne'
-- 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 : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
h'o : meromorphicOrderAt f x = ⊤
top : (fun (x : 𝕜) ↦ 0) =ᶠ[𝓝[≠] x] f
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)

Tactic:
apply tendsto_const_nhds.congr'

Premises used: tendsto_const_nhds, Filter.Tendsto.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 : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
h'o : meromorphicOrderAt f x = ⊤
y : 𝕜
hy : f y = 0
⊢ 0 = f y

Tactic:
hy.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 : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
h'o : meromorphicOrderAt f 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 h'o] with y hy using hy.symm

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 : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
n : ℤ
h'o : 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),
    Tendsto f (𝓝[≠] x) (𝓝 0)
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)

Tactic:
rcases (meromorphicOrderAt_eq_int_iff hf).1 h'o 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 : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
n : ℤ
h'o : 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 ≤ n

Tactic:
simpa [h'o] using ho.le

Premises used: LT.lt.le
-- 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 : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
n : ℤ
h'o : 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
coe :
  ∀ (n : ℕ) (h'o : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ))
    (hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z), Tendsto f (𝓝[≠] x) (𝓝 0)
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)

Tactic:
lift n to ℕ using by simpa [h'o] using ho.le
-- 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 : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
n : ℕ
h'o : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
⊢ 0 < n

Tactic:
simpa [h'o] using ho
-- 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 : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
n : ℕ
h'o : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
⊢ 0 < n

Tactic:
have : 0 < n := by simpa [h'o] using ho
-- 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 : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
n : ℕ
h'o : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
this : 0 < n
⊢ 0 = (x - x) ^ n • g x

Tactic:
simp [zero_pow_eq_zero.2 this.ne']

Premises used: Iff.mpr, LT.lt.ne', zero_pow_eq_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 : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
n : ℕ
h'o : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
⊢ 0 = (x - x) ^ n • g x

Tactic:
have : (0 : E) = (x - x) ^ n • g x := by
      have : 0 < n := by simpa [h'o] using ho
      simp [zero_pow_eq_zero.2 this.ne']
-- 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 : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
n : ℕ
h'o : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
this : 0 = (x - x) ^ n • g x
coe : Tendsto f (𝓝[≠] x) (𝓝 ((x - x) ^ n • g x))
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)

Tactic:
rw [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 : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
n : ℕ
h'o : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
this : 0 = (x - x) ^ n • g x
⊢ ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) 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 : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
n : ℕ
h'o : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
this : 0 = (x - x) ^ n • g x
⊢ ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x

Tactic:
have : ContinuousAt (fun z ↦ (z - x) ^ n • g z) x := by 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 : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
n : ℕ
h'o : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
this_1 : 0 = (x - x) ^ n • g x
this : ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
coe : (fun (z : 𝕜) ↦ (z - x) ^ n • g z) =ᶠ[𝓝[≠] x] f
⊢ Tendsto f (𝓝[≠] x) (𝓝 ((x - x) ^ n • g x))

Tactic:
apply this.continuousWithinAt.tendsto.congr'

Premises used: ContinuousAt.continuousWithinAt, Filter.Tendsto.congr', 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 : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
n : ℕ
h'o : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
this_1 : 0 = (x - x) ^ n • g x
this : ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
y : 𝕜
hy : f y = HPow.hPow (β := ℤ) (y - x) (↑n : ℤ) • g y
⊢ (y - x) ^ n • g y = 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 : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
n : ℕ
h'o : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
this_1 : 0 = (x - x) ^ n • g x
this : ContinuousAt.{u_1, u_2} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
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 (z : 𝕜) ↦ (z - x) ^ n • g z) x_3 = f x_3) x_2}
            x_1}
      a
h₁ h₂ : ∀ (y : 𝕜) (hy : f y = HPow.hPow (β := ℤ) (y - x) (↑n : ℤ) • g y), (y - x) ^ n • g y = f y
⊢ (fun (z : 𝕜) ↦ (z - x) ^ n • g z) =ᶠ[𝓝[≠] x] f

Tactic:
filter_upwards [hg] with y hy using by 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 : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
cases : ∀ (x_1 : WithTop ℤ) (h'o : meromorphicOrderAt f x = x_1), Tendsto f (𝓝[≠] x) (𝓝 0)
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)

Tactic:
cases h'o : meromorphicOrderAt f x with
  | top =>
    apply tendsto_const_nhds.congr'
    filter_upwards [meromorphicOrderAt_eq_top_iff.1 h'o] with y hy using hy.symm
  | coe n =>
    rcases (meromorphicOrderAt_eq_int_iff hf).1 h'o with ⟨g, g_an, gx, hg⟩
    lift n to ℕ using by simpa [h'o] using ho.le
    have : (0 : E) = (x - x) ^ n • g x := by
      have : 0 < n := by simpa [h'o] using ho
      simp [zero_pow_eq_zero.2 this.ne']
    rw [this]
    have : ContinuousAt (fun z ↦ (z - x) ^ n • g z) x := by fun_prop
    apply this.continuousWithinAt.tendsto.congr'
    filter_upwards [hg] with y hy using by simp [hy]

Premises used: tendsto_const_nhds, meromorphicOrderAt, Filter.Tendsto.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 : 𝕜
hf : MeromorphicAt f x
ho : 0 ≤ meromorphicOrderAt f x
inl : ∀ (ho : 0 = meromorphicOrderAt f x), ∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)
inr : ∀ (ho : 0 < meromorphicOrderAt f x), ∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ ∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)

Tactic:
rcases ho.eq_or_lt with ho | ho

Premises used: LE.le.eq_or_lt
-- 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 : MeromorphicAt f x
ho_1 : 0 ≤ meromorphicOrderAt f x
ho : 0 = meromorphicOrderAt f x
inl : ∀ (c : E) (hc : Tendsto f (𝓝[≠] x) (𝓝 c)), ∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ ∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)

Tactic:
rcases tendsto_ne_zero_of_meromorphicOrderAt_eq_zero hf ho.symm with ⟨c, -, hc⟩

Premises used: tendsto_ne_zero_of_meromorphicOrderAt_eq_zero, 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 : 𝕜
hf : MeromorphicAt f x
ho_1 : 0 ≤ meromorphicOrderAt f x
ho : 0 = meromorphicOrderAt f x
c : E
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ ∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)

Tactic:
⟨c, hc⟩

Premises used: 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 : MeromorphicAt f x
ho_1 : 0 ≤ meromorphicOrderAt f x
ho : 0 = meromorphicOrderAt f x
c : E
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ ∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)

Tactic:
exact ⟨c, hc⟩
-- 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 : MeromorphicAt f x
ho_1 : 0 ≤ meromorphicOrderAt f x
ho : 0 < meromorphicOrderAt f x
⊢ ∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)

Tactic:
⟨0, tendsto_zero_of_meromorphicOrderAt_pos ho⟩

Premises used: tendsto_zero_of_meromorphicOrderAt_pos, Exists.intro, OfNat.ofNat
-- 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 : MeromorphicAt f x
ho_1 : 0 ≤ meromorphicOrderAt f x
ho : 0 < meromorphicOrderAt f x
⊢ ∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)

Tactic:
exact ⟨0, tendsto_zero_of_meromorphicOrderAt_pos ho⟩
-- 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 : MeromorphicAt f x
inl : ∀ (ho : meromorphicOrderAt f x < 0), Tendsto f (𝓝[≠] x) (Bornology.cobounded E) ↔ meromorphicOrderAt f x < 0
inr : ∀ (ho : 0 ≤ meromorphicOrderAt f x), Tendsto f (𝓝[≠] x) (Bornology.cobounded E) ↔ meromorphicOrderAt f x < 0
⊢ Tendsto f (𝓝[≠] x) (Bornology.cobounded E) ↔ meromorphicOrderAt f x < 0

Tactic:
rcases lt_or_ge (meromorphicOrderAt f x) 0 with ho | ho

Premises used: meromorphicOrderAt, lt_or_ge, OfNat.ofNat
-- 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 : MeromorphicAt f x
ho : meromorphicOrderAt f x < 0
⊢ Tendsto f (𝓝[≠] x) (Bornology.cobounded E) ↔ meromorphicOrderAt f x < 0

Tactic:
simp [ho, tendsto_cobounded_of_meromorphicOrderAt_neg]

Premises used: tendsto_cobounded_of_meromorphicOrderAt_neg
-- 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 : MeromorphicAt f x
ho : 0 ≤ meromorphicOrderAt f x
inr : ¬Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
⊢ Tendsto f (𝓝[≠] x) (Bornology.cobounded E) ↔ meromorphicOrderAt f x < 0

Tactic:
simp only [lt_iff_not_ge, ho, not_true_eq_false, iff_false, ← tendsto_norm_atTop_iff_cobounded]

Premises used: lt_iff_not_ge, iff_false, not_true_eq_false, tendsto_norm_atTop_iff_cobounded
-- 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 : MeromorphicAt f x
ho : 0 ≤ meromorphicOrderAt f x
inr : ∀ (c : E) (hc : Tendsto f (𝓝[≠] x) (𝓝 c)), ¬Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
⊢ ¬Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop

Tactic:
obtain ⟨c, hc⟩ := tendsto_nhds_of_meromorphicOrderAt_nonneg hf ho

Premises used: tendsto_nhds_of_meromorphicOrderAt_nonneg
-- 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 : MeromorphicAt f x
ho : 0 ≤ meromorphicOrderAt f x
c : E
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ ¬Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop

Tactic:
not_tendsto_atTop_of_tendsto_nhds hc.norm

Premises used: Filter.Tendsto.norm, not_tendsto_atTop_of_tendsto_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 : MeromorphicAt f x
ho : 0 ≤ meromorphicOrderAt f x
c : E
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ ¬Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop

Tactic:
exact not_tendsto_atTop_of_tendsto_nhds hc.norm

Premises used: Filter.Tendsto.norm, not_tendsto_atTop_of_tendsto_nhds