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 g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₁f : MeromorphicAt f x
h₃ : meromorphicOrderAt f x = ⊤
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ g z
⊢ 0 =ᶠ[𝓝 x] g
have pos : 0 =ᶠ[𝓝[≠] x] g
Tactic: rw [← ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE (by fun_prop) (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
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
h₃ : ¬meromorphicOrderAt f x = ⊤
⊢ (if h₁ : MeromorphicAt f x then
      if h₂ : meromorphicOrderAt f x = ⊤ then 0
      else
        ⋯.choose (p := fun (g : 𝕜 → E) ↦
          AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) x
    else 0) =
    g x
have neg : sorry.choose (p := fun (g : 𝕜 → E) ↦
    AnalyticAt 𝕜 g x ∧ ¬g x = 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) x =
  g x
Tactic: simp only [h₁f, reduceDIte, h₃, ne_eq]
-- 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
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
h₃ : ¬meromorphicOrderAt f x = ⊤
⊢ ⋯.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ ¬g x = 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) x =
    g x
have h'₁ : AnalyticAt 𝕜
  (sorry.choose (p := fun (g : 𝕜 → E) ↦
    AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z))
  x
Tactic: obtain ⟨h'₁, h'₂, h'₃⟩ := ((meromorphicOrderAt_ne_top_iff h₁f).1 h₃).choose_spec
-- 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
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
h₃ : ¬meromorphicOrderAt f x = ⊤
h'₁ :
  AnalyticAt 𝕜
    (⋯.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z))
    x
⊢ ⋯.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ ¬g x = 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) x =
    g x
have h'₂ : sorry.choose (p := fun (g : 𝕜 → E) ↦
    AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) x ≠
  0
Tactic: obtain ⟨h'₁, h'₂, h'₃⟩ := ((meromorphicOrderAt_ne_top_iff h₁f).1 h₃).choose_spec
-- 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
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
h₃ : ¬meromorphicOrderAt f x = ⊤
h'₁ :
  AnalyticAt 𝕜
    (⋯.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z))
    x
h'₂ :
  ⋯.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) x ≠
    0
⊢ ⋯.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ ¬g x = 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) x =
    g x
have h'₃ : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦
  (z - x) ^ (meromorphicOrderAt f x).untop₀ •
    sorry.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) z
Tactic: obtain ⟨h'₁, h'₂, h'₃⟩ := ((meromorphicOrderAt_ne_top_iff h₁f).1 h₃).choose_spec
-- 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 g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
h₃ : ¬meromorphicOrderAt f x = ⊤
h'₁ :
  AnalyticAt 𝕜
    (⋯.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z))
    x
h'₂ :
  ⋯.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) x ≠
    0
h'₃ :
  f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦
    (z - x) ^ (meromorphicOrderAt f x).untop₀ •
      ⋯.choose (p := fun (g : 𝕜 → E) ↦
        AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) z
⊢ ⋯.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ ¬g x = 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) x =
    g x
have neg : sorry.choose (p := fun (g : 𝕜 → E) ↦
    AnalyticAt 𝕜 g x ∧ ¬g x = 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) =ᶠ[𝓝 x]
  g
Tactic: apply Filter.EventuallyEq.eq_of_nhds
-- 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 g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
h₃ : ¬meromorphicOrderAt f x = ⊤
h'₁ :
  AnalyticAt 𝕜
    (⋯.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z))
    x
h'₂ :
  ⋯.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) x ≠
    0
h'₃ :
  f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦
    (z - x) ^ (meromorphicOrderAt f x).untop₀ •
      ⋯.choose (p := fun (g : 𝕜 → E) ↦
        AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) z
⊢ ⋯.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ ¬g x = 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) =ᶠ[𝓝 x]
    g
have neg : sorry.choose (p := fun (g : 𝕜 → E) ↦
    AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) =ᶠ[𝓝[≠] x]
  g
Tactic: rw [← h'₁.continuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE h₁g.continuousAt]
-- 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 g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
h₃ : ¬meromorphicOrderAt f x = ⊤
h'₁ :
  AnalyticAt 𝕜
    (⋯.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z))
    x
h'₂ :
  ⋯.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) x ≠
    0
h'₃ :
  f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦
    (z - x) ^ (meromorphicOrderAt f x).untop₀ •
      ⋯.choose (p := fun (g : 𝕜 → E) ↦
        AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) z
⊢ ⋯.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧
        g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) =ᶠ[𝓝[≠] x]
    g
have h₁ : ∀ (y : 𝕜) (h₁y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y)
  (h₂y :
    f y =
      (y - x) ^ (meromorphicOrderAt f x).untop₀ •
        sorry.choose (p := fun (g : 𝕜 → E) ↦
          AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) y)
  (h₃y : Membership.mem (γ := Set 𝕜) {x}ᶜ y),
  sorry.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) y =
    g y
Tactic: filter_upwards [h, h'₃, self_mem_nhdsWithin] with y h₁y h₂y h₃y
-- 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 g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
h₃ : ¬meromorphicOrderAt f x = ⊤
h'₁ :
  AnalyticAt 𝕜
    (⋯.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z))
    x
h'₂ :
  ⋯.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) x ≠
    0
h'₃ :
  f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦
    (z - x) ^ (meromorphicOrderAt f x).untop₀ •
      ⋯.choose (p := fun (g : 𝕜 → E) ↦
        AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) z
y : 𝕜
h₁y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
h₂y :
  f y =
    (y - x) ^ (meromorphicOrderAt f x).untop₀ •
      ⋯.choose (p := fun (g : 𝕜 → E) ↦
        AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) y
h₃y : Membership.mem (γ := Set 𝕜) {x}ᶜ y
⊢ ⋯.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) y =
    g y
have h₁ : sorry.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) y -
    g y =
  0
Tactic: rw [← sub_eq_zero]
-- 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 g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
h₃ : ¬meromorphicOrderAt f x = ⊤
h'₁ :
  AnalyticAt 𝕜
    (⋯.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z))
    x
h'₂ :
  ⋯.choose (p := fun (g : 𝕜 → E) ↦
      AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) x ≠
    0
h'₃ :
  f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦
    (z - x) ^ (meromorphicOrderAt f x).untop₀ •
      ⋯.choose (p := fun (g : 𝕜 → E) ↦
        AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) z
y : 𝕜
h₁y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
h₂y :
  f y =
    (y - x) ^ (meromorphicOrderAt f x).untop₀ •
      ⋯.choose (p := fun (g : 𝕜 → E) ↦
        AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) y
h₃y : Membership.mem (γ := Set 𝕜) {x}ᶜ y
⊢ ⋯.choose (p := fun (g : 𝕜 → E) ↦
        AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) y -
      g y =
    0
have h₁ : ∀
  (h₁y :
    (y - x) ^ (meromorphicOrderAt f x).untop₀ •
        (sorry.choose (p := fun (g : 𝕜 → E) ↦
            AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) y -
          g y) =
      0)
  (h₂y :
    f y =
      (y - x) ^ (meromorphicOrderAt f x).untop₀ •
        sorry.choose (p := fun (g : 𝕜 → E) ↦
          AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) y)
  (h₃y : Membership.mem (γ := Set 𝕜) {x}ᶜ y), (y - x) ^ (meromorphicOrderAt f x).untop₀ ≠ 0
Tactic: rwa [h₂y, ← sub_eq_zero, ← smul_sub, smul_eq_zero_iff_right] at h₁y
Cleared hypotheses: h₁y, h₂y, h₃y
-- 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 g : 𝕜 → E
x : 𝕜
n : ℤ
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ n • g z
⊢ MeromorphicAt f x
have rw : MeromorphicAt.{u_1, u_2} (E := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
Tactic: rw [MeromorphicAt.meromorphicAt_congr h]
-- 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
f g : 𝕜 → E
x : 𝕜
n : ℤ
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ n • g z
⊢ meromorphicTrailingCoeffAt f x = g x
have h₄ : MeromorphicAt f x
Tactic: have h₄ : MeromorphicAt f x := by
    rw [MeromorphicAt.meromorphicAt_congr h]
    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
f g : 𝕜 → E
x : 𝕜
n : ℤ
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ n • g z
h₄ : MeromorphicAt f x
⊢ meromorphicOrderAt f x = (↑n : WithTop ℤ)
have simp : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ¬g x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
Tactic: simp only [meromorphicOrderAt_eq_int_iff h₄, ne_eq]
-- 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 g : 𝕜 → E
x : 𝕜
n : ℤ
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ n • g z
h₄ : MeromorphicAt f x
⊢ ∃ (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.TrailingCoefficient (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
n : ℤ
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ n • g z
h₄ : MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt f x = g x
have this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
Tactic: have : meromorphicOrderAt f x = n := by
    simp only [meromorphicOrderAt_eq_int_iff h₄, ne_eq]
    use g, h₁g, h₂g
    exact 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
f : 𝕜 → E
x : 𝕜
h₁ : AnalyticAt 𝕜 f x
h₂ : f x ≠ 0
⊢ meromorphicTrailingCoeffAt f x = f x
have rw : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ HPow.hPow (β := ℤ) (z - x) 0 • f z
Tactic: rw [h₁.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE (n := 0) 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
f : 𝕜 → E
x : 𝕜
h₁ : AnalyticAt 𝕜 f x
h₂ : f x ≠ 0
⊢ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ HPow.hPow (β := ℤ) (z - x) 0 • f z
have h : ∀ (a : 𝕜), f a = HPow.hPow (β := ℤ) (a - x) 0 • f a
Tactic: filter_upwards
-- 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
⊢ Tendsto (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-(meromorphicOrderAt f x).untop₀) • f) (𝓝[≠] x)
    (𝓝 (meromorphicTrailingCoeffAt f x))
have pos : ∀ (h₂ : meromorphicOrderAt f x = ⊤),
  Tendsto (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-(meromorphicOrderAt f x).untop₀) • 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
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
pos :
  ∀ (h₂ : meromorphicOrderAt f x = ⊤),
    Tendsto (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-(meromorphicOrderAt f x).untop₀) • f) (𝓝[≠] x)
      (𝓝 (meromorphicTrailingCoeffAt f x))
⊢ Tendsto (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-(meromorphicOrderAt f x).untop₀) • f) (𝓝[≠] x)
    (𝓝 (meromorphicTrailingCoeffAt f x))
have neg : ∀ (h₂ : ¬meromorphicOrderAt f x = ⊤),
  Tendsto (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-(meromorphicOrderAt f x).untop₀) • 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
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
⊢ Tendsto (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-(meromorphicOrderAt f x).untop₀) • f) (𝓝[≠] x)
    (𝓝 (meromorphicTrailingCoeffAt f x))
have pos : Tendsto f (𝓝[≠] x) (𝓝 0)
Tactic: simp_all only [WithTop.untop₀_top, neg_zero, zpow_zero, one_smul,
      meromorphicTrailingCoeffAt_of_order_eq_top]
-- 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 = ⊤
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)
have pos : 0 =ᶠ[𝓝[≠] x] f
Tactic: apply Tendsto.congr' (f₁ := 0)
-- 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 = ⊤
pos : 0 =ᶠ[𝓝[≠] x] f
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)
have pos₁ : Tendsto.{u_1, u_2} (β := E) 0 (𝓝[≠] x) (𝓝 0)
Tactic: apply Tendsto.congr' (f₁ := 0)
-- 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 = ⊤
⊢ 0 =ᶠ[𝓝[≠] x] f
have h₁ : ∀ (y : 𝕜) (hy : f y = 0), 0 y = f y
Tactic: filter_upwards [meromorphicOrderAt_eq_top_iff.1 h₂] with y hy
-- 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 = ⊤
⊢ Tendsto (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-(meromorphicOrderAt f x).untop₀) • 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),
  Tendsto (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-(meromorphicOrderAt f x).untop₀) • 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
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 (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-(meromorphicOrderAt f x).untop₀) • f) (𝓝[≠] x)
    (𝓝 (meromorphicTrailingCoeffAt f x))
have neg : g =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-(meromorphicOrderAt f x).untop₀) • f
Tactic: apply Tendsto.congr' (f₁ := 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 = ⊤
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] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-(meromorphicOrderAt f x).untop₀) • f
⊢ Tendsto (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-(meromorphicOrderAt f x).untop₀) • f) (𝓝[≠] x)
    (𝓝 (meromorphicTrailingCoeffAt f x))
have neg₁ : Tendsto g (𝓝[≠] x) (𝓝 (meromorphicTrailingCoeffAt f x))
Tactic: apply Tendsto.congr' (f₁ := 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 = ⊤
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
⊢ g =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-(meromorphicOrderAt f x).untop₀) • f
have h₁ : ∀ (y : 𝕜) (h₁y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y) (h₂y : Membership.mem (γ := Set 𝕜) {x}ᶜ y),
  g y = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-(meromorphicOrderAt f x).untop₀) • f) y
Tactic: filter_upwards [h₃g, self_mem_nhdsWithin] with y h₁y h₂y
-- 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
y : 𝕜
h₁y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
h₂y : Membership.mem (γ := Set 𝕜) {x}ᶜ y
⊢ g y = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-(meromorphicOrderAt f x).untop₀) • f) y
have h₁ : y - x ≠ 0 ∨
  -(meromorphicOrderAt f x).untop₀ + (meromorphicOrderAt f x).untop₀ ≠ 0 ∨
    -(meromorphicOrderAt f x).untop₀ = 0 ∧ (meromorphicOrderAt f x).untop₀ = 0
Tactic: rw [zpow_neg, Pi.smul_apply', Pi.inv_apply, Pi.pow_apply, h₁y, ← smul_assoc, smul_eq_mul,
      ← zpow_neg, ← zpow_add', neg_add_cancel, zpow_zero, one_smul]
-- 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
y : 𝕜
h₁y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
h₂y : Membership.mem (γ := Set 𝕜) {x}ᶜ y
⊢ y - x ≠ 0 ∨
    -(meromorphicOrderAt f x).untop₀ + (meromorphicOrderAt f x).untop₀ ≠ 0 ∨
      -(meromorphicOrderAt f x).untop₀ = 0 ∧ (meromorphicOrderAt f x).untop₀ = 0
have h₁ : y - x ≠ 0
Tactic: left