awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
have 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
Tactic: rw [eventually_nhdsWithin_iff]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ ∀ᶠ (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
have 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
Tactic: filter_upwards [hg_eq] with z hg_eq hz
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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_1 :
  ∀ᶠ (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 : 𝕜
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
have h₁ : HPow.hPow (β := ℤ) (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 =
  HPow.hPow (β := ℤ) (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) :
        ℤ) •
    (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: 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]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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_1 :
  ∀ᶠ (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 : 𝕜
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
h₁ :
  HPow.hPow (β := ℤ) (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 =
    HPow.hPow (β := ℤ) (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) :
          ℤ) •
      (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
rwa : ℤ
⊢ 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
have h₂ : HPow.hPow (β := ℤ) (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 =
  (HPow.hPow (β := ℤ) (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) :
          ℤ) *
      (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: 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]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
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
⊢ 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
have 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
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]
Cleared hypotheses: hg_eq
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ meromorphicOrderAt f x ≠ ⊤ ↔ ∀ᶠ (x : 𝕜) in 𝓝[≠] x, f x ≠ 0
have mp : meromorphicOrderAt f x ≠ ⊤ → ∀ᶠ (x : 𝕜) in 𝓝[≠] x, f x ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ meromorphicOrderAt f x ≠ ⊤ ↔ ∀ᶠ (x : 𝕜) in 𝓝[≠] x, f x ≠ 0
have mpr : (∀ᶠ (x : 𝕜) in 𝓝[≠] x, f x ≠ 0) → meromorphicOrderAt f x ≠ ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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 ≠ ⊤
⊢ ∀ᶠ (x : 𝕜) in 𝓝[≠] x, f x ≠ 0
have 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
Tactic: obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_ne_top_iff hf).1 h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ ∀ᶠ (x : 𝕜) in 𝓝[≠] x, f x ≠ 0
have h₁ : ∀ (a : 𝕜),
  f a = (a - x) ^ (meromorphicOrderAt f x).untop₀ • g a → Membership.mem (γ := Set 𝕜) {x}ᶜ a → g a ≠ 0 → f a ≠ 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)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
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
⊢ Tendsto f (𝓝[≠] x) (Bornology.cobounded E)
have hf : MeromorphicAt f x
Tactic: have hf : MeromorphicAt f x := meromorphicAt_of_meromorphicOrderAt_ne_zero ho.ne
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ Tendsto f (𝓝[≠] x) (Bornology.cobounded E)
have simp : Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
Tactic: simp only [← tendsto_norm_atTop_iff_cobounded]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
have obtain : ∀ (m : ℤ) (hm : (↑m : WithTop ℤ) = meromorphicOrderAt f x), Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
Tactic: obtain ⟨m, hm⟩ := WithTop.ne_top_iff_exists.mp ho.ne_top
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
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
⊢ Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
have m_neg : m < 0
Tactic: have m_neg : m < 0 := by simpa [← hm] using ho
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
have 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
Tactic: rcases (meromorphicOrderAt_eq_int_iff hf).1 hm.symm with ⟨g, g_an, gx, hg⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
have simp : Tendsto (β := ℝ) (fun (z : 𝕜) ↦ ‖(z - x) ^ m‖ * ‖g z‖) (𝓝[≠] x) atTop
Tactic: simp only [norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
have apply : Tendsto (β := ℝ) (fun (x_1 : 𝕜) ↦ ‖(x_1 - x) ^ m‖) (𝓝[≠] x) atTop
Tactic: apply Filter.Tendsto.atTop_mul_pos (C := ‖g x‖) (by simp [gx]) _
      g_an.continuousAt.continuousWithinAt.tendsto.norm
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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)
have refine_1 : Tendsto (β := 𝕜) (fun (z : 𝕜) ↦ z - x) (𝓝[≠] x) (𝓝 0)
Tactic: refine tendsto_nhdsWithin_iff.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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)
⊢ Tendsto (β := 𝕜) (fun (z : 𝕜) ↦ z - x) (𝓝[≠] x) (𝓝[≠] 0)
have refine_2 : ∀ᶠ (n : 𝕜) in 𝓝[≠] x, Membership.mem (γ := Set 𝕜) {0}ᶜ (n - x)
Tactic: refine tendsto_nhdsWithin_iff.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
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)
have this : ContinuousWithinAt (Y := 𝕜) (fun (z : 𝕜) ↦ z - x) {x}ᶜ x
Tactic: have : ContinuousWithinAt (fun z ↦ z - x) {x}ᶜ x := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ ∀ᶠ (n : 𝕜) in 𝓝[≠] x, Membership.mem (γ := Set 𝕜) {0}ᶜ (n - x)
have h : ∀ (y : 𝕜) (hy : Membership.mem (γ := Set 𝕜) {x}ᶜ y), Membership.mem (γ := Set 𝕜) {0}ᶜ (y - x)
Tactic: filter_upwards [self_mem_nhdsWithin] with y hy
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
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 (x_1 : 𝕜) ↦ ‖(x_1 - x) ^ m‖) (𝓝[≠] x) atTop
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
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 (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
have A : 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
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
have apply : (𝓝[≠] x).EventuallyEq (β := ℝ) (fun (z : 𝕜) ↦ ‖(z - x) ^ m • g z‖) fun (x : 𝕜) ↦ ‖f x‖
Tactic: apply A.congr'
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ (𝓝[≠] x).EventuallyEq (β := ℝ) (fun (z : 𝕜) ↦ ‖(z - x) ^ m • g z‖) fun (x : 𝕜) ↦ ‖f x‖
have 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
Tactic: filter_upwards [hg] with z hz using by simp [hz]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ (𝓝[≠] x).EventuallyEq (β := ℝ) (fun (z : 𝕜) ↦ ‖(z - x) ^ m • g z‖) fun (x : 𝕜) ↦ ‖f x‖
have h₁ : ∀ (a : 𝕜), f a = (a - x) ^ m • g a → ‖(a - x) ^ m • g a‖ = ‖f a‖
Tactic: filter_upwards [hg] with z hz using by simp [hz]