awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (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₂ : ¬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
⊢ Tendsto g (𝓝[≠] x) (𝓝 (meromorphicTrailingCoeffAt f x))
have neg : Tendsto g (𝓝[≠] x) (𝓝 (g x))
Tactic: rw [h₁g.meromorphicTrailingCoeffAt_of_eq_nhdsNE h₃g]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (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₂ : meromorphicOrderAt f x ≠ ⊤
⊢ meromorphicTrailingCoeffAt f x ≠ 0
have obtain : ∀ (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), meromorphicTrailingCoeffAt f x ≠ 0
Tactic: obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_ne_top_iff h₁).1 h₂
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x e : 𝕜
⊢ meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ e) x = e
have pos : ∀ (he : e = 0), meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ e) x = e
Tactic: by_cases he : e = 0
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x e : 𝕜
pos : ∀ (he : e = 0), meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ e) x = e
⊢ meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ e) x = e
have neg : ∀ (he : ¬e = 0), meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ e) x = e
Tactic: by_cases he : e = 0
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x e : 𝕜
he : e = 0
⊢ meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ e) x = e
have pos : Eq (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ 0) x) 0
Tactic: rw [he]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x e : 𝕜
he : e = 0
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ 0) x) 0
have pos : meromorphicOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ 0) x = ⊤
Tactic: apply MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x e : 𝕜
he : e = 0
⊢ meromorphicOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ 0) x = ⊤
have pos : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [meromorphicOrderAt_eq_top_iff]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : DecidableEq 𝕜
x y : 𝕜
⊢ meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x = if x = y then 1 else x - y
have pos : ∀ (h : x = y), meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x = if x = y then 1 else x - y
Tactic: by_cases h : x = y
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : DecidableEq 𝕜
x y : 𝕜
pos : ∀ (h : x = y), meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x = if x = y then 1 else x - y
⊢ meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x = if x = y then 1 else x - y
have neg : ∀ (h : ¬x = y), meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x = if x = y then 1 else x - y
Tactic: by_cases h : x = y
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : DecidableEq 𝕜
x y : 𝕜
h : x = y
⊢ meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x = if x = y then 1 else x - y
have pos : Eq (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) y) 1
Tactic: simp_all only [sub_self, ite_true]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : DecidableEq 𝕜
x y : 𝕜
h : x = y
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) y) 1
have pos : (𝓝[≠] y).EventuallyEq (β := 𝕜) (fun (x : 𝕜) ↦ x - y) fun (z : 𝕜) ↦ HSMul.hSMul (β := 𝕜) (HPow.hPow (β := ℤ) (z - y) 1) 1
Tactic: apply AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE (n := 1) (by fun_prop)
      (by apply one_ne_zero)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : DecidableEq 𝕜
x y : 𝕜
h : ¬x = y
⊢ meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x = if x = y then 1 else x - y
have neg : meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x = x - y
Tactic: simp_all only [ite_false]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : DecidableEq 𝕜
x y : 𝕜
h : ¬x = y
⊢ meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x = x - y
have neg : x - y ≠ 0
Tactic: apply AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero (by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
h : f₁ =ᶠ[𝓝[≠] x] f₂
⊢ meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
have pos : ∀ (h₁ : ¬MeromorphicAt f₁ x), meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
Tactic: by_cases h₁ : ¬MeromorphicAt f₁ x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
h : f₁ =ᶠ[𝓝[≠] x] f₂
pos : ∀ (h₁ : ¬MeromorphicAt f₁ x), meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
⊢ meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
have neg : ∀ (h₁ : ¬¬MeromorphicAt f₁ x), meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
Tactic: by_cases h₁ : ¬MeromorphicAt f₁ x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
h : f₁ =ᶠ[𝓝[≠] x] f₂
h₁ : ¬¬MeromorphicAt f₁ x
⊢ meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
have h₂ : MeromorphicAt f₁ x
Tactic: rw [not_not] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
h : f₁ =ᶠ[𝓝[≠] x] f₂
h₁ : MeromorphicAt f₁ x
⊢ meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
have pos : ∀ (h₂ : meromorphicOrderAt f₁ x = ⊤), meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
Tactic: by_cases h₂ : meromorphicOrderAt f₁ x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
h : f₁ =ᶠ[𝓝[≠] x] f₂
h₁ : MeromorphicAt f₁ x
pos : ∀ (h₂ : meromorphicOrderAt f₁ x = ⊤), meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
⊢ meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
have neg : ∀ (h₂ : ¬meromorphicOrderAt f₁ x = ⊤), meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
Tactic: by_cases h₂ : meromorphicOrderAt f₁ x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
h : f₁ =ᶠ[𝓝[≠] x] f₂
h₁ : MeromorphicAt f₁ x
h₂ : ¬meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
have neg : ∀ (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),
  meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
Tactic: obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_ne_top_iff h₁).1 h₂
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
h : f₁ =ᶠ[𝓝[≠] x] f₂
h₁ : 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
⊢ meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
have neg : g x = meromorphicTrailingCoeffAt f₂ x
Tactic: rw [h₁g.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE h₂g h₃g,
    h₁g.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE h₂g (h.symm.trans h₃g)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
h : f₁ =ᶠ[𝓝[≠] x] f₂
h₁ : 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
neg : g x = meromorphicTrailingCoeffAt f₂ x
⊢ meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
have neg₁ : g x = g x
Tactic: rw [h₁g.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE h₂g h₃g,
    h₁g.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE h₂g (h.symm.trans h₃g)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
⊢ meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x
have pos : ∀ (h₁ : ¬MeromorphicAt f x), meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x
Tactic: by_cases h₁ : ¬ MeromorphicAt f x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
pos : ∀ (h₁ : ¬MeromorphicAt f x), meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x
⊢ meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x
have neg : ∀ (h₁ : ¬¬MeromorphicAt f x), meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x
Tactic: by_cases h₁ : ¬ MeromorphicAt f x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : ¬¬MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x
have h₂ : MeromorphicAt f x
Tactic: rw [not_not] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x
have pos : ∀ (h₂ : meromorphicOrderAt f x = ⊤), meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x
Tactic: by_cases h₂ : meromorphicOrderAt f x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
pos : ∀ (h₂ : meromorphicOrderAt f x = ⊤), meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x
⊢ meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x
have neg : ∀ (h₂ : ¬meromorphicOrderAt f x = ⊤), meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x
Tactic: by_cases h₂ : meromorphicOrderAt f x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
⊢ meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x
have neg : ∀ (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),
  meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x
Tactic: obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_ne_top_iff h₁).1 h₂
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : 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
⊢ meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x
have neg : meromorphicTrailingCoeffAt (-f) x = -g x
Tactic: rw [h₁g.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE h₂g h₃g]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : 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
⊢ meromorphicTrailingCoeffAt (-f) x = -g x
have neg : (-g) x = -g x
Tactic: rw [AnalyticAt.meromorphicTrailingCoeffAt_of_eq_nhdsNE (g := -g)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : 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
neg : (-g) x = -g x
⊢ meromorphicTrailingCoeffAt (-f) x = -g x
have neg₁ : AnalyticAt 𝕜 (-g) x
Tactic: rw [AnalyticAt.meromorphicTrailingCoeffAt_of_eq_nhdsNE (g := -g)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : 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
neg : (-g) x = -g x
neg₁ : AnalyticAt 𝕜 (-g) x
⊢ meromorphicTrailingCoeffAt (-f) x = -g x
have neg₂ : -f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt (-f) x).untop₀ • (-g) z
Tactic: rw [AnalyticAt.meromorphicTrailingCoeffAt_of_eq_nhdsNE (g := -g)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : 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
⊢ -f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt (-f) x).untop₀ • (-g) z
have h : ∀ (a : 𝕜) (ha : f a = (a - x) ^ (meromorphicOrderAt f x).untop₀ • g a),
  (-f) a = (a - x) ^ (meromorphicOrderAt (-f) x).untop₀ • (-g) a
Tactic: filter_upwards [h₃g] with a ha
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x
have pos : ∀ (hf₁ : ¬MeromorphicAt f₁ x), meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x
Tactic: by_cases! hf₁ : ¬MeromorphicAt f₁ x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
pos : ∀ (hf₁ : ¬MeromorphicAt f₁ x), meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x
have neg : ∀ (hf₁ : MeromorphicAt f₁ x), meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x
Tactic: by_cases! hf₁ : ¬MeromorphicAt f₁ x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : ¬MeromorphicAt f₁ x
⊢ ¬MeromorphicAt (f₁ + f₂) x
have rwa : ¬MeromorphicAt (f₂ + f₁) x
Tactic: rwa [add_comm, hf₂.meromorphicAt_add_iff_meromorphicAt₁]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : ¬MeromorphicAt f₁ x
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x
have this : ¬MeromorphicAt (f₁ + f₂) x
Tactic: have : ¬MeromorphicAt (f₁ + f₂) x := by
      rwa [add_comm, hf₂.meromorphicAt_add_iff_meromorphicAt₁]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x
have pos : ∀ (h₁f₂ : meromorphicOrderAt f₂ x = ⊤), meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x
Tactic: by_cases h₁f₂ : meromorphicOrderAt f₂ x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
pos : ∀ (h₁f₂ : meromorphicOrderAt f₂ x = ⊤), meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x
have neg : ∀ (h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤), meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x
Tactic: by_cases h₁f₂ : meromorphicOrderAt f₂ x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
h₁f₂ : meromorphicOrderAt f₂ x = ⊤
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x
have pos : f₁ + f₂ =ᶠ[𝓝[≠] x] f₁
Tactic: apply meromorphicTrailingCoeffAt_congr_nhdsNE
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
h₁f₂ : meromorphicOrderAt f₂ x = ⊤
⊢ f₁ + f₂ =ᶠ[𝓝[≠] x] f₁
have h₁ : ∀ (a : 𝕜), f₂ a = 0 → (f₁ + f₂) a = f₁ a
Tactic: filter_upwards [meromorphicOrderAt_eq_top_iff.1 h₁f₂]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x
have neg : ∀ (n₂ : ℤ) (hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x) (h : meromorphicOrderAt f₁ x < (↑n₂ : WithTop ℤ)),
  meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x
Tactic: lift meromorphicOrderAt f₂ x to ℤ using h₁f₂ with n₂ hn₂
Cleared hypotheses: h, h₁f₂
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
h : meromorphicOrderAt f₁ x < (↑n₂ : WithTop ℤ)
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt 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),
  meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x
Tactic: obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (meromorphicOrderAt_eq_int_iff hf₂).1 hn₂.symm
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
h : 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
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x
have neg : ∀ (n₁ : ℤ) (hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x) (h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)),
  meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x
Tactic: lift meromorphicOrderAt f₁ x to ℤ using (by aesop) with n₁ hn₁
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
hf₁ : MeromorphicAt f₁ x
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
h : (↑n₁ : WithTop ℤ) < (↑n₂ : WithTop ℤ)
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt 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),
  meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x
Tactic: obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (meromorphicOrderAt_eq_int_iff hf₁).1 hn₁.symm