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 : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x = 0
⊢ ∃ (c : E), c ≠ 0 ∧ Tendsto f (𝓝[≠] x) (𝓝 c)
have 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)
Tactic: rcases (meromorphicOrderAt_eq_int_iff hf).1 ho 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 : 𝕜
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)
have refine : Tendsto f (𝓝[≠] x) (𝓝 (g x))
Tactic: refine ⟨g x, gx, ?_⟩
-- 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 : 𝕜
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
⊢ Tendsto f (𝓝[≠] x) (𝓝 (g x))
have apply : g =ᶠ[𝓝[≠] x] f
Tactic: apply g_an.continuousAt.continuousWithinAt.tendsto.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 : 𝕜
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
⊢ g =ᶠ[𝓝[≠] x] f
have 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
Tactic: filter_upwards [hg] with y hy using by simp [hy]
-- 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 : 𝕜
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
⊢ g =ᶠ[𝓝[≠] x] f
have h₁ : ∀ (a : 𝕜), f a = HPow.hPow (β := ℤ) (a - x) 0 • g a → g a = f a
Tactic: filter_upwards [hg] with y hy using by simp [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 : 0 < meromorphicOrderAt f x
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)
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 : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
h'o : meromorphicOrderAt f x = ⊤
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)
have top : (fun (x : 𝕜) ↦ 0) =ᶠ[𝓝[≠] x] f
Tactic: apply tendsto_const_nhds.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 : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
h'o : meromorphicOrderAt f x = ⊤
⊢ (fun (x : 𝕜) ↦ 0) =ᶠ[𝓝[≠] x] f
have 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
Tactic: filter_upwards [meromorphicOrderAt_eq_top_iff.1 h'o] with y hy using hy.symm
-- 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 : 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
⊢ (fun (x : 𝕜) ↦ 0) =ᶠ[𝓝[≠] x] f
have h₁ : ∀ (a : 𝕜), f a = 0 → 0 = f a
Tactic: filter_upwards [meromorphicOrderAt_eq_top_iff.1 h'o] with y hy using hy.symm
-- 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 : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
n : ℤ
h'o : meromorphicOrderAt f x = (↑n : WithTop ℤ)
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)
have 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)
Tactic: rcases (meromorphicOrderAt_eq_int_iff hf).1 h'o 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 : 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
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)
have 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)
Tactic: lift n to ℕ using by simpa [h'o] using ho.le
Cleared hypotheses: n, h'o, hg
-- 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 : 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
have this : 0 < n
Tactic: have : 0 < n := by simpa [h'o] using ho
-- 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 : 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
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)
have this : 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']
-- 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 : 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
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)
have coe : Tendsto f (𝓝[≠] x) (𝓝 ((x - x) ^ n • g x))
Tactic: rw [this]
-- 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 : 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
⊢ Tendsto f (𝓝[≠] x) (𝓝 ((x - x) ^ n • g x))
have this₁ : 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
-- 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 : 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
⊢ Tendsto f (𝓝[≠] x) (𝓝 ((x - x) ^ n • g x))
have coe : (fun (z : 𝕜) ↦ (z - x) ^ n • g z) =ᶠ[𝓝[≠] x] f
Tactic: apply this.continuousWithinAt.tendsto.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 : 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
⊢ (fun (z : 𝕜) ↦ (z - x) ^ n • g z) =ᶠ[𝓝[≠] x] f
have 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
Tactic: filter_upwards [hg] with y hy using by simp [hy]
-- 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 : 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
⊢ (fun (z : 𝕜) ↦ (z - x) ^ n • g z) =ᶠ[𝓝[≠] x] f
have h₁ : ∀ (a : 𝕜), f a = HPow.hPow (β := ℤ) (a - x) (↑n : ℤ) • g a → (a - x) ^ n • g a = f a
Tactic: filter_upwards [hg] with y hy using by simp [hy]
-- 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 : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)
have cases : ∀ (x_1 : WithTop ℤ) (h'o : meromorphicOrderAt f x = x_1), 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]
-- 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 : 𝕜
hf : MeromorphicAt f x
ho : 0 ≤ meromorphicOrderAt f x
⊢ ∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)
have inl : ∀ (ho : 0 = meromorphicOrderAt f x), ∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)
Tactic: rcases ho.eq_or_lt with ho | 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 : 𝕜
hf : MeromorphicAt f x
ho : 0 ≤ meromorphicOrderAt f x
inl : ∀ (ho : 0 = meromorphicOrderAt f x), ∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ ∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)
have inr : ∀ (ho : 0 < meromorphicOrderAt f x), ∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)
Tactic: rcases ho.eq_or_lt with ho | 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 : 𝕜
hf : MeromorphicAt f x
ho_1 : 0 ≤ meromorphicOrderAt f x
ho : 0 = meromorphicOrderAt f x
⊢ ∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)
have inl : ∀ (c : E) (hc : 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⟩
-- 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 : 𝕜
hf : MeromorphicAt f x
⊢ Tendsto f (𝓝[≠] x) (Bornology.cobounded E) ↔ meromorphicOrderAt f x < 0
have inl : ∀ (ho : 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
-- 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 : 𝕜
hf : MeromorphicAt f x
inl : ∀ (ho : meromorphicOrderAt f x < 0), Tendsto f (𝓝[≠] x) (Bornology.cobounded E) ↔ meromorphicOrderAt f x < 0
⊢ Tendsto f (𝓝[≠] x) (Bornology.cobounded E) ↔ meromorphicOrderAt f x < 0
have inr : ∀ (ho : 0 ≤ meromorphicOrderAt f x), Tendsto f (𝓝[≠] x) (Bornology.cobounded E) ↔ meromorphicOrderAt f x < 0
Tactic: rcases lt_or_ge (meromorphicOrderAt f x) 0 with ho | 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 : 𝕜
hf : MeromorphicAt f x
ho : 0 ≤ meromorphicOrderAt f x
⊢ Tendsto f (𝓝[≠] x) (Bornology.cobounded E) ↔ meromorphicOrderAt f x < 0
have inr : ¬Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
Tactic: simp only [lt_iff_not_ge, ho, not_true_eq_false, iff_false, ← 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 : 𝕜
hf : MeromorphicAt f x
ho : 0 ≤ meromorphicOrderAt f x
⊢ ¬Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
have inr : ∀ (c : E) (hc : Tendsto f (𝓝[≠] x) (𝓝 c)), ¬Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
Tactic: obtain ⟨c, hc⟩ := tendsto_nhds_of_meromorphicOrderAt_nonneg hf 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 : 𝕜
hf : MeromorphicAt f x
⊢ (∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ 0 ≤ meromorphicOrderAt f x
have inl : ∀ (ho : meromorphicOrderAt f x < 0), (∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ 0 ≤ meromorphicOrderAt f x
Tactic: rcases lt_or_ge (meromorphicOrderAt f x) 0 with ho | 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 : 𝕜
hf : MeromorphicAt f x
inl : ∀ (ho : meromorphicOrderAt f x < 0), (∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ 0 ≤ meromorphicOrderAt f x
⊢ (∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ 0 ≤ meromorphicOrderAt f x
have inr : ∀ (ho : 0 ≤ meromorphicOrderAt f x), (∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ 0 ≤ meromorphicOrderAt f x
Tactic: rcases lt_or_ge (meromorphicOrderAt f x) 0 with ho | 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 : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x < 0
⊢ (∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ 0 ≤ meromorphicOrderAt f x
have inl : ∀ (x_1 : E), ¬Tendsto f (𝓝[≠] x) (𝓝 x_1)
Tactic: simp only [← not_lt, ho, not_true_eq_false, iff_false, not_exists]
-- 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 : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x < 0
c : E
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ False
have inl : Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
Tactic: apply not_tendsto_atTop_of_tendsto_nhds hc.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 : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x < 0
c : E
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
have inl : Tendsto f (𝓝[≠] x) (Bornology.cobounded E)
Tactic: rw [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 : 𝕜
hf : MeromorphicAt f x
⊢ (∃ (c : E), c ≠ 0 ∧ Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ meromorphicOrderAt f x = 0
have inl : ∀ (ho : meromorphicOrderAt f x = 0), (∃ (c : E), c ≠ 0 ∧ Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ meromorphicOrderAt f x = 0
Tactic: rcases eq_or_ne (meromorphicOrderAt f x) 0 with ho | 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 : 𝕜
hf : MeromorphicAt f x
inl : ∀ (ho : meromorphicOrderAt f x = 0), (∃ (c : E), c ≠ 0 ∧ Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ meromorphicOrderAt f x = 0
⊢ (∃ (c : E), c ≠ 0 ∧ Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ meromorphicOrderAt f x = 0
have inr : ∀ (ho : meromorphicOrderAt f x ≠ 0), (∃ (c : E), c ≠ 0 ∧ Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ meromorphicOrderAt f x = 0
Tactic: rcases eq_or_ne (meromorphicOrderAt f x) 0 with ho | 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 : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x ≠ 0
⊢ (∃ (c : E), c ≠ 0 ∧ Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ meromorphicOrderAt f x = 0
have inr : ∀ (x_1 : E), ¬x_1 = 0 → ¬Tendsto f (𝓝[≠] x) (𝓝 x_1)
Tactic: simp only [ne_eq, ho, iff_false, not_exists, not_and]
-- 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 : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x ≠ 0
c : E
c_ne : ¬c = 0
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ False
have inr : ∀ (ho : meromorphicOrderAt f x < 0), False
Tactic: rcases ho.lt_or_gt with ho | 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 : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x ≠ 0
c : E
c_ne : ¬c = 0
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
inr : ∀ (ho : meromorphicOrderAt f x < 0), False
⊢ False
have inr₁ : ∀ (ho : 0 < meromorphicOrderAt f x), False
Tactic: rcases ho.lt_or_gt with ho | 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 : 𝕜
hf : MeromorphicAt f x
ho_1 : meromorphicOrderAt f x ≠ 0
c : E
c_ne : ¬c = 0
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
ho : meromorphicOrderAt f x < 0
⊢ False
have inr : Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
Tactic: apply not_tendsto_atTop_of_tendsto_nhds hc.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 : 𝕜
hf : MeromorphicAt f x
ho_1 : meromorphicOrderAt f x ≠ 0
c : E
c_ne : ¬c = 0
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
ho : meromorphicOrderAt f x < 0
⊢ Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖f x‖) (𝓝[≠] x) atTop
have inr : Tendsto f (𝓝[≠] x) (Bornology.cobounded E)
Tactic: rw [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 : 𝕜
hf : MeromorphicAt f x
ho_1 : meromorphicOrderAt f x ≠ 0
c : E
c_ne : ¬c = 0
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
ho : 0 < meromorphicOrderAt f x
⊢ False
have inr : c = 0
Tactic: apply c_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 : 𝕜
hf : MeromorphicAt f x
⊢ Tendsto f (𝓝[≠] x) (𝓝 0) ↔ 0 < meromorphicOrderAt f x
have inl : ∀ (ho : 0 < meromorphicOrderAt f x), Tendsto f (𝓝[≠] x) (𝓝 0) ↔ 0 < meromorphicOrderAt f x
Tactic: rcases lt_or_ge 0 (meromorphicOrderAt f x) with ho | 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 : 𝕜
hf : MeromorphicAt f x
inl : ∀ (ho : 0 < meromorphicOrderAt f x), Tendsto f (𝓝[≠] x) (𝓝 0) ↔ 0 < meromorphicOrderAt f x
⊢ Tendsto f (𝓝[≠] x) (𝓝 0) ↔ 0 < meromorphicOrderAt f x
have inr : ∀ (ho : meromorphicOrderAt f x ≤ 0), Tendsto f (𝓝[≠] x) (𝓝 0) ↔ 0 < meromorphicOrderAt f x
Tactic: rcases lt_or_ge 0 (meromorphicOrderAt f x) with ho | 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 : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x ≤ 0
⊢ Tendsto f (𝓝[≠] x) (𝓝 0) ↔ 0 < meromorphicOrderAt f x
have inr : ¬Tendsto f (𝓝[≠] x) (𝓝 0)
Tactic: simp only [← not_le, ho, not_true_eq_false, iff_false]
-- 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 : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x ≤ 0
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
⊢ False
have inr : ∀ (ho : meromorphicOrderAt f x = 0), False
Tactic: rcases ho.eq_or_lt with ho | ho