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 : 𝕜
n : ℤ
hf : MeromorphicAt f x
h_1 :
  ¬analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
            f z)
        x =
      ⊤
m : ℕ
h :
  (↑m : ℕ∞) =
    analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x
neg :
  ∀ (g : 𝕜 → E) (hg_an : AnalyticAt 𝕜 g x) (hg_ne : g x ≠ 0)
    (hg_eq :
      ∀ᶠ (z : 𝕜) in 𝓝 x,
        (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
            f z =
          (z - x) ^ m • g z),
    HSub.hSub (α := ℤ) (↑m : ℤ)
          (↑(Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) ⋯) :
            ℤ) =
        n ↔
      ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ HSub.hSub (α := ℤ) (↑m : ℤ)
        (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              ⋯) :
          ℤ) =
      n ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
obtain ⟨g, hg_an, hg_ne, hg_eq⟩ := hf.choose_spec.analyticOrderAt_eq_natCast.mp h.symm

Premises used: Exists.choose_spec, AnalyticAt.analyticOrderAt_eq_natCast, Iff.mp, 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 : 𝕜
n : ℤ
hf : MeromorphicAt f x
h_1 :
  ¬analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
            f z)
        x =
      ⊤
m : ℕ
h :
  (↑m : ℕ∞) =
    analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq :
  ∀ᶠ (z : 𝕜) in 𝓝 x,
    (z - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f z =
      (z - x) ^ m • g z
rw :
  ∀ᶠ (x_1 : 𝕜) in 𝓝 x,
    Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 →
      f x_1 =
        (x_1 - x) ^
            HSub.hSub (α := ℤ) (↑m : ℤ)
              (↑(Exists.choose (p := fun (n : ℕ) ↦
                    AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf) :
                ℤ) •
          g x_1
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x,
    f z =
      (z - x) ^
          HSub.hSub (α := ℤ) (↑m : ℤ)
            (↑(Exists.choose (p := fun (n : ℕ) ↦
                  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf) :
              ℤ) •
        g z

Tactic:
rw [eventually_nhdsWithin_iff]

Premises used: eventually_nhdsWithin_iff
-- 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 : 𝕜
n : ℤ
hf : MeromorphicAt f x
h_1 :
  ¬analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
            f z)
        x =
      ⊤
m : ℕ
h :
  (↑m : ℕ∞) =
    analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq :
  ∀ᶠ (z : 𝕜) in 𝓝 x,
    (z - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f z =
      (z - x) ^ m • g z
h₁ :
  ∀ (z : 𝕜)
    (hg_eq :
      (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z =
        (z - x) ^ m • g z)
    (hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z),
    f z =
      (z - x) ^
          HSub.hSub (α := ℤ) (↑m : ℤ)
            (↑(Exists.choose (p := fun (n : ℕ) ↦
                  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf) :
              ℤ) •
        g z
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x,
    Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 →
      f x_1 =
        (x_1 - x) ^
            HSub.hSub (α := ℤ) (↑m : ℤ)
              (↑(Exists.choose (p := fun (n : ℕ) ↦
                    AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf) :
                ℤ) •
          g x_1

Tactic:
filter_upwards [hg_eq] with z hg_eq 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 : 𝕜
n : ℤ
hf : MeromorphicAt f x
h_1 :
  ¬analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
            f z)
        x =
      ⊤
m : ℕ
h :
  (↑m : ℕ∞) =
    analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq :
  ∀ᶠ (z : 𝕜) in 𝓝 x,
    (z - x) ^
          Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
            hf •
        f z =
      (z - x) ^ m • g z
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x,
    f z =
      (z - x) ^
          HSub.hSub (α := ℤ) (↑m : ℤ)
            (↑(Exists.choose (p := fun (n : ℕ) ↦
                  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf) :
              ℤ) •
        g z

Tactic:
replace hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ (↑m - ↑hf.choose : ℤ) • g z := by
      rw [eventually_nhdsWithin_iff]
      filter_upwards [hg_eq] with z hg_eq hz
      rwa [← smul_right_inj <| zpow_ne_zero _ (sub_ne_zero.mpr hz), ← mul_smul,
        ← zpow_add₀ (sub_ne_zero.mpr hz), ← add_sub_assoc, add_sub_cancel_left, zpow_natCast,
        zpow_natCast]
-- 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 : 𝕜
n : ℤ
hf : MeromorphicAt f x
h_1 :
  ¬analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
            f z)
        x =
      ⊤
m : ℕ
h :
  (↑m : ℕ∞) =
    analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq :
  ∀ᶠ (z : 𝕜) in 𝓝[≠] x,
    f z =
      (z - x) ^
          HSub.hSub (α := ℤ) (↑m : ℤ)
            (↑(Exists.choose (p := fun (n : ℕ) ↦
                  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf) :
              ℤ) •
        g z
⊢ HSub.hSub (α := ℤ) (↑m : ℤ)
        (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              ⋯) :
          ℤ) =
      n ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
⟨fun h ↦ ⟨g, hg_an, hg_ne, h ▸ hg_eq⟩,
      AnalyticAt.unique_eventuallyEq_zpow_smul_nonzero ⟨g, hg_an, hg_ne, hg_eq⟩⟩

Premises used: Eq.rec, And.intro, Iff.intro, Exists.intro, AnalyticAt.unique_eventuallyEq_zpow_smul_nonzero
-- 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 : 𝕜
n : ℤ
hf : MeromorphicAt f x
h_1 :
  ¬analyticOrderAt.{u_1, u_2} (E := E)
        (fun (z : 𝕜) ↦
          (z - x) ^
              Exists.choose (p := fun (n : ℕ) ↦
                AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf •
            f z)
        x =
      ⊤
m : ℕ
h :
  (↑m : ℕ∞) =
    analyticOrderAt.{u_1, u_2} (E := E)
      (fun (z : 𝕜) ↦
        (z - x) ^
            Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              hf •
          f z)
      x
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq :
  ∀ᶠ (z : 𝕜) in 𝓝[≠] x,
    f z =
      (z - x) ^
          HSub.hSub (α := ℤ) (↑m : ℤ)
            (↑(Exists.choose (p := fun (n : ℕ) ↦
                  AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x) hf) :
              ℤ) •
        g z
⊢ HSub.hSub (α := ℤ) (↑m : ℤ)
        (↑(Exists.choose (p := fun (n : ℕ) ↦ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x)
              ⋯) :
          ℤ) =
      n ↔
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
exact ⟨fun h ↦ ⟨g, hg_an, hg_ne, h ▸ hg_eq⟩,
      AnalyticAt.unique_eventuallyEq_zpow_smul_nonzero ⟨g, hg_an, hg_ne, hg_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
z₀ : 𝕜
hf : MeromorphicAt f z₀
⊢ meromorphicOrderAt f z₀ ≠ ⊤ ↔
    ∃ (g : 𝕜 → E),
      AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ f =ᶠ[𝓝[≠] z₀] fun (z : 𝕜) ↦ (z - z₀) ^ (meromorphicOrderAt f z₀).untop₀ • g z

Tactic:
⟨fun h ↦ (meromorphicOrderAt_eq_int_iff hf).1 (WithTop.coe_untop₀_of_ne_top h).symm,
    fun h ↦ Option.ne_none_iff_exists'.2
      ⟨(meromorphicOrderAt f z₀).untopD 0, (meromorphicOrderAt_eq_int_iff hf).2 h⟩⟩

Premises used: Iff.mpr, Option.ne_none_iff_exists', meromorphicOrderAt, meromorphicOrderAt_eq_int_iff, WithTop.coe_untop₀_of_ne_top, Iff.intro, Exists.intro, Iff.mp, WithTop.untopD, OfNat.ofNat, 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
x : 𝕜
f : 𝕜 → E
hf : MeromorphicAt f x
mp : meromorphicOrderAt f x ≠ ⊤ → ∀ᶠ (x : 𝕜) in 𝓝[≠] x, f x ≠ 0
mpr : (∀ᶠ (x : 𝕜) in 𝓝[≠] x, f x ≠ 0) → meromorphicOrderAt f x ≠ ⊤
⊢ meromorphicOrderAt f x ≠ ⊤ ↔ ∀ᶠ (x : 𝕜) in 𝓝[≠] x, f x ≠ 0

Tactic:
constructor
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
hf : MeromorphicAt f x
h : meromorphicOrderAt f x ≠ ⊤
mp :
  ∀ (g : 𝕜 → E) (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0)
    (h₃g : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z), ∀ᶠ (x : 𝕜) in 𝓝[≠] x, f x ≠ 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝[≠] x, f x ≠ 0

Tactic:
obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_ne_top_iff hf).1 h

Premises used: meromorphicOrderAt_ne_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
x : 𝕜
f : 𝕜 → E
hf : MeromorphicAt f x
h : meromorphicOrderAt f x ≠ ⊤
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁ :
  ∀ (a : 𝕜),
    f a = (a - x) ^ (meromorphicOrderAt f x).untop₀ • g a → Membership.mem (γ := Set 𝕜) {x}ᶜ a → g a ≠ 0 → f a ≠ 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝[≠] x, f x ≠ 0

Tactic:
filter_upwards [h₃g, self_mem_nhdsWithin, eventually_nhdsWithin_of_eventually_nhds
      ((h₁g.continuousAt.ne_iff_eventually_ne continuousAt_const).mp h₂g)]

Premises used: ContinuousAt.ne_iff_eventually_ne, continuousAt_const, eventually_nhdsWithin_of_eventually_nhds, self_mem_nhdsWithin, Iff.mp, AnalyticAt.continuousAt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
hf : MeromorphicAt f x
h : meromorphicOrderAt f x ≠ ⊤
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ ∀ (a : 𝕜),
    f a = (a - x) ^ (meromorphicOrderAt f x).untop₀ • g a → Membership.mem (γ := Set 𝕜) {x}ᶜ a → g a ≠ 0 → f a ≠ 0

Tactic:
simp_all [zpow_ne_zero, sub_ne_zero]

Premises used: sub_ne_zero, zpow_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
x : 𝕜
f : 𝕜 → E
hf : MeromorphicAt f x
⊢ (∀ᶠ (x : 𝕜) in 𝓝[≠] x, f x ≠ 0) → meromorphicOrderAt f x ≠ ⊤

Tactic:
simp_all [meromorphicOrderAt_eq_top_iff, Eventually.frequently]

Premises used: meromorphicOrderAt_eq_top_iff, Filter.Eventually.frequently
-- 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
⊢ 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 : meromorphicOrderAt f x < 0
hf : MeromorphicAt f x
simp : Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
⊢ Tendsto f (𝓝[≠] x) (Bornology.cobounded E)

Tactic:
simp only [← tendsto_norm_atTop_iff_cobounded]

Premises used: 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 : 𝕜
ho : meromorphicOrderAt f x < 0
hf : MeromorphicAt f x
obtain :
  ∀ (m : ℤ) (hm : (↑m : WithTop ℤ) = meromorphicOrderAt f x), Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
⊢ Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop

Tactic:
obtain ⟨m, hm⟩ := WithTop.ne_top_iff_exists.mp ho.ne_top

Premises used: LT.lt.ne_top, WithTop.ne_top_iff_exists, 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 : meromorphicOrderAt f x < 0
hf : MeromorphicAt f x
m : ℤ
hm : (↑m : WithTop ℤ) = meromorphicOrderAt f x
⊢ m < 0

Tactic:
simpa [← hm] 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 : meromorphicOrderAt f x < 0
hf : MeromorphicAt f x
m : ℤ
hm : (↑m : WithTop ℤ) = meromorphicOrderAt f x
⊢ m < 0

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

Tactic:
rcases (meromorphicOrderAt_eq_int_iff hf).1 hm.symm with ⟨g, g_an, gx, hg⟩

Premises used: meromorphicOrderAt_eq_int_iff, Iff.mp, 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 : 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
simp : Tendsto (β := ℝ) (fun (z : 𝕜) ↦ ‖(z - x) ^ m‖ * ‖g z‖) (𝓝[≠] x) atTop
⊢ Tendsto (β := ℝ) (fun (z : 𝕜) ↦ ‖(z - x) ^ m • g z‖) (𝓝[≠] x) atTop

Tactic:
simp only [norm_smul]

Premises used: norm_smul
-- 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
⊢ 0 < ‖g x‖

Tactic:
simp [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 : 𝕜
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
apply : Tendsto (β := ℝ) (fun (x_1 : 𝕜) ↦ ‖(x_1 - x) ^ m‖) (𝓝[≠] x) atTop
⊢ Tendsto (β := ℝ) (fun (z : 𝕜) ↦ ‖(z - x) ^ m‖ * ‖g z‖) (𝓝[≠] x) atTop

Tactic:
apply Filter.Tendsto.atTop_mul_pos (C := ‖g x‖) (by simp [gx]) _
      g_an.continuousAt.continuousWithinAt.tendsto.norm

Premises used: ContinuousAt.continuousWithinAt, Filter.Tendsto.norm, Filter.Tendsto.atTop_mul_pos, AnalyticAt.continuousAt, 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 : 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) (𝓝[≠] x) (𝓝[≠] 0)

Tactic:
tendsto_nhdsWithin_iff.2 ⟨?_, ?_⟩

Premises used: Iff.mpr, tendsto_nhdsWithin_iff, And.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 : 𝕜
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
refine_1 : Tendsto (β := 𝕜) (fun (z : 𝕜) ↦ z - x) (𝓝[≠] x) (𝓝 0)
refine_2 : ∀ᶠ (n : 𝕜) in 𝓝[≠] x, Membership.mem (γ := Set 𝕜) {0}ᶜ (n - x)
⊢ Tendsto (β := 𝕜) (fun (z : 𝕜) ↦ z - x) (𝓝[≠] x) (𝓝[≠] 0)

Tactic:
refine tendsto_nhdsWithin_iff.2 ⟨?_, ?_⟩

Premises used: Iff.mpr, tendsto_nhdsWithin_iff, And.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 : 𝕜
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
⊢ ContinuousWithinAt (Y := 𝕜) (fun (z : 𝕜) ↦ z - x) {x}ᶜ 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 : 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
⊢ ContinuousWithinAt (Y := 𝕜) (fun (z : 𝕜) ↦ z - x) {x}ᶜ x

Tactic:
have : ContinuousWithinAt (fun z ↦ z - x) {x}ᶜ 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 : 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 : ContinuousWithinAt (Y := 𝕜) (fun (z : 𝕜) ↦ z - x) {x}ᶜ x
⊢ Tendsto (β := 𝕜) (fun (z : 𝕜) ↦ z - x) (𝓝[≠] x) (𝓝 0)

Tactic:
simpa using this.tendsto

Premises used: 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 : 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
h : ∀ (y : 𝕜) (hy : Membership.mem (γ := Set 𝕜) {x}ᶜ y), Membership.mem (γ := Set 𝕜) {0}ᶜ (y - x)
⊢ ∀ᶠ (n : 𝕜) in 𝓝[≠] x, Membership.mem (γ := Set 𝕜) {0}ᶜ (n - x)

Tactic:
filter_upwards [self_mem_nhdsWithin] with y hy

Premises used: self_mem_nhdsWithin
-- 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
y : 𝕜
hy : Membership.mem (γ := Set 𝕜) {x}ᶜ y
⊢ Membership.mem (γ := Set 𝕜) {0}ᶜ (y - x)

Tactic:
simpa [sub_eq_zero] using hy

Premises used: sub_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 : 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) (𝓝[≠] x) (𝓝[≠] 0)

Tactic:
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
-- 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:
(tendsto_norm_cobounded_atTop.comp (tendsto_zpow_nhdsNE_zero_cobounded m_neg)).comp this

Premises used: tendsto_norm_cobounded_atTop, Filter.Tendsto.comp