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
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
inr : ∀ (ho : meromorphicOrderAt f x = 0), False
⊢ False
have inr₁ : ∀ (ho : meromorphicOrderAt f x < 0), False
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 : meromorphicOrderAt f x ≤ 0
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
ho : meromorphicOrderAt f x = 0
⊢ False
have inr : ∀ (c : E) (c_ne : c ≠ 0) (h'c : Tendsto f (𝓝[≠] x) (𝓝 c)), False
Tactic: obtain ⟨c, c_ne, h'c⟩ := tendsto_ne_zero_of_meromorphicOrderAt_eq_zero 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
ho_1 : meromorphicOrderAt f x ≤ 0
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
ho : meromorphicOrderAt f x = 0
c : E
c_ne : c ≠ 0
h'c : Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ 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
ho_1 : meromorphicOrderAt f x ≤ 0
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
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
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
have pos : ∀ (hf₁ : MeromorphicAt f₁ x), meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
Tactic: by_cases hf₁ : MeromorphicAt f₁ x
-- 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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
pos : ∀ (hf₁ : MeromorphicAt f₁ x), meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
have neg : ∀ (hf₁ : ¬MeromorphicAt f₁ x), meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
Tactic: by_cases hf₁ : MeromorphicAt f₁ x
-- 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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : ¬MeromorphicAt f₁ x
⊢ ¬MeromorphicAt f₂ x
have contrapose : ∀ (hf₁ : MeromorphicAt f₂ x), MeromorphicAt f₁ x
Tactic: contrapose hf₁
Cleared hypotheses: hf₁
-- 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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : ¬MeromorphicAt f₁ x
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
have this : ¬MeromorphicAt f₂ x
Tactic: have : ¬ MeromorphicAt f₂ x := by
      contrapose hf₁
      exact hf₁.congr hf₁₂.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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
have pos : ∀ (h₁f₁ : meromorphicOrderAt f₁ x = ⊤), meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
Tactic: by_cases h₁f₁ : meromorphicOrderAt f₁ x = ⊤
-- 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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
pos : ∀ (h₁f₁ : meromorphicOrderAt f₁ x = ⊤), meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
have neg : ∀ (h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤), meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
Tactic: by_cases h₁f₁ : meromorphicOrderAt f₁ x = ⊤
-- 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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
h₁f₁ : meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
have pos : meromorphicOrderAt f₂ x = ⊤
Tactic: rw [h₁f₁, eq_comm]
-- 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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
h₁f₁ : meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicOrderAt f₂ x = ⊤
have pos : ∀ (h₁f₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = 0), ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = 0
Tactic: rw [meromorphicOrderAt_eq_top_iff] at h₁f₁ ⊢
Cleared hypotheses: h₁f₁
-- 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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
have neg : ∀ (n : ℤ) (hn : meromorphicOrderAt f₁ x = (↑n : WithTop ℤ)), meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
Tactic: obtain ⟨n, hn : meromorphicOrderAt f₁ x = n⟩ := Option.ne_none_iff_exists'.mp h₁f₁
-- 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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
n : ℤ
hn : meromorphicOrderAt f₁ x = (↑n : WithTop ℤ)
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
have neg : ∀ (g : 𝕜 → E) (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0) (h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n • g z),
  meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
Tactic: obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_eq_int_iff hf₁).1 hn
-- 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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
n : ℤ
hn : meromorphicOrderAt f₁ x = (↑n : WithTop ℤ)
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n • g z
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
have neg : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n • g z
Tactic: rw [hn, eq_comm, meromorphicOrderAt_eq_int_iff (hf₁.congr hf₁₂)]
-- 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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
n : ℤ
hn : meromorphicOrderAt f₁ x = (↑n : WithTop ℤ)
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n • g z
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n • g z
have right : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n • g z
Tactic: use g, h₁g, h₂g
-- 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 : AnalyticAt 𝕜 f x
⊢ meromorphicOrderAt f x = ENat.map Nat.cast (analyticOrderAt f x)
have top : ∀ (hn : analyticOrderAt f x = ⊤), meromorphicOrderAt f x = ENat.map Nat.cast ⊤
Tactic: cases hn : analyticOrderAt f x
-- 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 : AnalyticAt 𝕜 f x
top : ∀ (hn : analyticOrderAt f x = ⊤), meromorphicOrderAt f x = ENat.map Nat.cast ⊤
⊢ meromorphicOrderAt f x = ENat.map Nat.cast (analyticOrderAt f x)
have coe : ∀ (a : ℕ) (hn : analyticOrderAt f x = (↑a : ℕ∞)), meromorphicOrderAt f x = ENat.map Nat.cast (↑a : ℕ∞)
Tactic: cases hn : analyticOrderAt f x
-- 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 : AnalyticAt 𝕜 f x
hn : analyticOrderAt f x = ⊤
⊢ meromorphicOrderAt f x = ENat.map Nat.cast ⊤
have top : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
Tactic: rw [ENat.map_top, meromorphicOrderAt_eq_top_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 : 𝕜
hf : AnalyticAt 𝕜 f x
a : ℕ
hn : analyticOrderAt f x = (↑a : ℕ∞)
⊢ meromorphicOrderAt f x = ENat.map Nat.cast (↑a : ℕ∞)
have coe : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ a • g z
Tactic: simp_rw [ENat.map_coe, meromorphicOrderAt_eq_int_iff hf.meromorphicAt, 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 : 𝕜
hf : AnalyticAt 𝕜 f x
a : ℕ
hn : analyticOrderAt f x = (↑a : ℕ∞)
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ a • g z
have coe : ∀ (g : 𝕜 → E) (h1 : AnalyticAt 𝕜 g x) (h2 : g x ≠ 0) (h3 : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ a • g z),
  ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ a • g z
Tactic: rcases hf.analyticOrderAt_eq_natCast.mp hn with ⟨g, h1, h2, h3⟩
-- 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 : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
ho : meromorphicOrderAt f x = ⊤
⊢ AnalyticAt 𝕜 f x
have this : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x : 𝕜) ↦ 0) x
Tactic: have : AnalyticAt 𝕜 (fun _ ↦ (0 : E)) x := analyticAt_const
-- 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 : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
ho : meromorphicOrderAt f x = ⊤
this : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x : 𝕜) ↦ 0) x
⊢ AnalyticAt 𝕜 f x
have top : (fun (x : 𝕜) ↦ 0) =ᶠ[𝓝 x] f
Tactic: apply this.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 : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
ho : meromorphicOrderAt f x = ⊤
this : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x : 𝕜) ↦ 0) x
⊢ (fun (x : 𝕜) ↦ 0) =ᶠ[𝓝 x] f
have top : (fun (x : 𝕜) ↦ 0) =ᶠ[𝓝[≠] x] f
Tactic: rw [← ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE continuousAt_const 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
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
ho : meromorphicOrderAt f x = ⊤
this : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x : 𝕜) ↦ 0) x
⊢ (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 ho] 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 : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
ho : meromorphicOrderAt f x = ⊤
this : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x : 𝕜) ↦ 0) x
h₁ :
  ∀ (a : 𝕜),
    Membership.mem (γ := Set 𝕜)
      {x : 𝕜 |
        Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (z : 𝕜) ↦ f z = 0) x} x →
          Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (x : 𝕜) ↦ (fun (x : 𝕜) ↦ (0 : E)) x = f x) x} x}
      a
⊢ (fun (x : 𝕜) ↦ 0) =ᶠ[𝓝[≠] x] f
have h₂ : ∀ (a : 𝕜), f a = 0 → 0 = f a
Tactic: filter_upwards [meromorphicOrderAt_eq_top_iff.1 ho] 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 : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
n : ℤ
ho : meromorphicOrderAt f x = (↑n : WithTop ℤ)
⊢ AnalyticAt 𝕜 f x
have coe : ∀ (g : 𝕜 → E) (g_an : AnalyticAt 𝕜 g x) (gx : g x ≠ 0) (hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z),
  AnalyticAt 𝕜 f x
Tactic: rcases (meromorphicOrderAt_eq_int_iff h).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 : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
n : ℤ
ho : meromorphicOrderAt f x = (↑n : WithTop ℤ)
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ 0 ≤ meromorphicOrderAt f x
have apply : ∃ (c : E), Tendsto f (𝓝[≠] x) (𝓝 c)
Tactic: apply (tendsto_nhds_iff_meromorphicOrderAt_nonneg h).1
-- 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 : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
n : ℤ
ho : meromorphicOrderAt f x = (↑n : WithTop ℤ)
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ AnalyticAt 𝕜 f x
have this : 0 ≤ meromorphicOrderAt f x
Tactic: have : 0 ≤ meromorphicOrderAt f x := by
      apply (tendsto_nhds_iff_meromorphicOrderAt_nonneg h).1
      exact ⟨f x, h'.continuousWithinAt.tendsto⟩
-- 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 : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
n : ℤ
ho : meromorphicOrderAt f x = (↑n : WithTop ℤ)
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
this : 0 ≤ meromorphicOrderAt f x
⊢ AnalyticAt 𝕜 f x
have coe : ∀ (n : ℕ) (ho : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ))
  (hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z), AnalyticAt 𝕜 f x
Tactic: lift n to ℕ using by simpa [ho] using this
Cleared hypotheses: n, ho, 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 : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
this : 0 ≤ meromorphicOrderAt f x
n : ℕ
ho : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
⊢ ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ n • g z = f z
have apply : (fun (x_1 : 𝕜) ↦ (x_1 - x) ^ n • g x_1) =ᶠ[𝓝[≠] x] f
Tactic: apply (ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE (by fun_prop) h').1
-- 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 : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
this : 0 ≤ meromorphicOrderAt f x
n : ℕ
ho : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
⊢ (fun (x_1 : 𝕜) ↦ (x_1 - x) ^ n • g x_1) =ᶠ[𝓝[≠] 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 (x_4 : 𝕜) ↦ (x_4 - x) ^ n • g x_4) x_3 = f x_3) x_2} x_1}
    a
Tactic: filter_upwards [hg] with z hz using by simpa using hz.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 : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
this : 0 ≤ meromorphicOrderAt f x
n : ℕ
ho : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
h₁ :
  ∀ (a : 𝕜),
    Membership.mem (γ := Set 𝕜)
      {x_1 : 𝕜 |
        Membership.mem (γ := Set 𝕜) {x_2 : 𝕜 | (fun (z : 𝕜) ↦ f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z) x_2}
            x_1 →
          Membership.mem (γ := Set 𝕜)
            {x_2 : 𝕜 | (fun (x_3 : 𝕜) ↦ (fun (x_4 : 𝕜) ↦ (x_4 - x) ^ n • g x_4) x_3 = f x_3) x_2} x_1}
      a
⊢ (fun (x_1 : 𝕜) ↦ (x_1 - x) ^ n • g x_1) =ᶠ[𝓝[≠] 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 z hz using by simpa using hz.symm
-- 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 : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
this : 0 ≤ meromorphicOrderAt f x
n : ℕ
ho : meromorphicOrderAt f x = (↑(↑n : ℤ) : WithTop ℤ)
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) (↑n : ℤ) • g z
⊢ AnalyticAt 𝕜 f x
have A : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ n • g z = f z
Tactic: have A : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ n • g z = f z := by
      apply (ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE (by fun_prop) h').1
      filter_upwards [hg] with z hz using by simpa using hz.symm
-- 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 : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
⊢ AnalyticAt 𝕜 f x
have cases : ∀ (x_1 : WithTop ℤ) (ho : meromorphicOrderAt f x = x_1), AnalyticAt 𝕜 f x
Tactic: cases ho : meromorphicOrderAt f x with
  | top =>
    /- If the order is infinite, then `f` vanishes on a pointed neighborhood of `x`. By continuity,
    it also vanishes at `x`.-/
    have : AnalyticAt 𝕜 (fun _ ↦ (0 : E)) x := analyticAt_const
    apply this.congr
    rw [← ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE continuousAt_const h']
    filter_upwards [meromorphicOrderAt_eq_top_iff.1 ho] with y hy using by simp [hy]
  | coe n =>
    /- If the order is finite, then the order has to be nonnegative, as otherwise the norm of `f`
    would tend to infinity at `x`. Then the local expression of `f` coming from its meromorphicity
    shows that it coincides with an analytic function close to `x`, except maybe at `x`. By
    continuity of `f`, the two functions also coincide at `x`. -/
    rcases (meromorphicOrderAt_eq_int_iff h).1 ho with ⟨g, g_an, gx, hg⟩
    have : 0 ≤ meromorphicOrderAt f x := by
      apply (tendsto_nhds_iff_meromorphicOrderAt_nonneg h).1
      exact ⟨f x, h'.continuousWithinAt.tendsto⟩
    lift n to ℕ using by simpa [ho] using this
    have A : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ n • g z = f z := by
      apply (ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE (by fun_prop) h').1
      filter_upwards [hg] with z hz using by simpa using hz.symm
    exact AnalyticAt.congr (by fun_prop) A
-- 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 : 𝕜
h : 0 < meromorphicOrderAt f x
hf : f x = 0
⊢ AnalyticAt 𝕜 f x
have refine : ContinuousAt f x
Tactic: refine (meromorphicAt_of_meromorphicOrderAt_ne_zero h.ne').analyticAt ?_
-- 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 : 𝕜
h : 0 < meromorphicOrderAt f x
hf : f x = 0
⊢ ContinuousAt f x
have rw : Tendsto f (𝓝[≠] x) (𝓝 0)
Tactic: rw [continuousAt_iff_punctured_nhds, hf]
-- 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
z₀ : 𝕜
e : E
inst_3 : Decidable (e = 0)
⊢ meromorphicOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) z₀ = if e = 0 then ⊤ else 0
have pos : ∀ (he : e = 0), meromorphicOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) z₀ = ⊤
Tactic: split_ifs with he
-- 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
z₀ : 𝕜
e : E
inst_3 : Decidable (e = 0)
pos : ∀ (he : e = 0), meromorphicOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) z₀ = ⊤
⊢ meromorphicOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) z₀ = if e = 0 then ⊤ else 0
have neg : ∀ (he : ¬e = 0), meromorphicOrderAt.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ e) z₀ = 0
Tactic: split_ifs with he
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
z₀ : 𝕜
n : ℕ
inst_1 : Decidable (Eq.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0)
⊢ meromorphicOrderAt (E := 𝕜) (OfNat.ofNat n) z₀ = if Eq.{u_1 + 1} (α := 𝕜) (↑n : 𝕜) 0 then ⊤ else 0
have h : ∀ (x : 𝕜), Eq.{u_1 + 1} (α := 𝕜) ((OfNat.ofNat n : 𝕜 → 𝕜) x) (↑n : 𝕜)
Tactic: convert! meromorphicOrderAt_const z₀ (n : 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
⊢ meromorphicOrderAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n) x = (↑n : WithTop ℤ)
have rw : ∃ (g : 𝕜 → 𝕜),
  AnalyticAt 𝕜 g x ∧
    g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n z = (z - x) ^ n • g z
Tactic: rw [meromorphicOrderAt_eq_int_iff (by fun_prop)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
⊢ meromorphicOrderAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n) x = (↑n : WithTop ℤ)
have h : HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n = HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) (↑n : ℤ)
Tactic: convert! meromorphicOrderAt_zpow_id_sub_const