awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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 = ⊤
pos : ∀ (h : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ g z), 0 = g x
⊢ meromorphicTrailingCoeffAt f x = g x

Tactic:
simp only [h₃, WithTop.untop₀_top, zpow_zero, one_smul,
      MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top] at ⊢ h

Premises used: zpow_zero, WithTop.untop₀_top, MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top, one_smul
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
pos : 0 =ᶠ[𝓝 x] g
⊢ 0 = g x

Tactic:
apply EventuallyEq.eq_of_nhds (f := 0)

Premises used: Filter.EventuallyEq.eq_of_nhds
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
⊢ ContinuousAt.{u_1, u_2} (Y := E) 0 x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
⊢ ContinuousAt g x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
pos : 0 =ᶠ[𝓝[≠] x] g
⊢ 0 =ᶠ[𝓝 x] g

Tactic:
rw [← ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE (by fun_prop) (by fun_prop)]

Premises used: ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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

Tactic:
apply (h.symm.trans (meromorphicOrderAt_eq_top_iff.1 h₃)).symm

Premises used: Filter.EventuallyEq.trans, meromorphicOrderAt_eq_top_iff, Iff.mp, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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 = ⊤
neg :
  ⋯.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
⊢ (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

Tactic:
simp only [h₁f, reduceDIte, h₃, ne_eq]

Premises used: reduceDIte, ne_eq
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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 = ⊤
⊢ 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

Tactic:
obtain ⟨h'₁, h'₂, h'₃⟩ := ((meromorphicOrderAt_ne_top_iff h₁f).1 h₃).choose_spec

Premises used: Exists.choose_spec, meromorphicOrderAt_ne_top_iff, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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 ≠
    0

Tactic:
obtain ⟨h'₁, h'₂, h'₃⟩ := ((meromorphicOrderAt_ne_top_iff h₁f).1 h₃).choose_spec

Premises used: Exists.choose_spec, meromorphicOrderAt_ne_top_iff, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
⊢ 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

Tactic:
obtain ⟨h'₁, h'₂, h'₃⟩ := ((meromorphicOrderAt_ne_top_iff h₁f).1 h₃).choose_spec

Premises used: Exists.choose_spec, meromorphicOrderAt_ne_top_iff, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
neg :
  ⋯.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
⊢ ⋯.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:
apply Filter.EventuallyEq.eq_of_nhds

Premises used: Filter.EventuallyEq.eq_of_nhds
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
neg :
  ⋯.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
⊢ ⋯.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]

Premises used: AnalyticAt.continuousAt, ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
h₁ :
  ∀ (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
⊢ ⋯.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:
filter_upwards [h, h'₃, self_mem_nhdsWithin] with y h₁y h₂y h₃y

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
h₁ :
  ⋯.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
⊢ ⋯.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:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
h₁ :
  ∀
    (h₁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 -
            g y) =
        0)
    (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), (y - x) ^ (meromorphicOrderAt f x).untop₀ ≠ 0
⊢ ⋯.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:
rwa [h₂y, ← sub_eq_zero, ← smul_sub, smul_eq_zero_iff_right] at h₁y

Premises used: sub_eq_zero, smul_eq_zero_iff_right, smul_sub
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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 :
  (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 -
        g y) =
    0
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
⊢ (y - x) ^ (meromorphicOrderAt f x).untop₀ ≠ 0

Tactic:
simp_all [zpow_ne_zero, sub_ne_zero]

Premises used: sub_ne_zero, zpow_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
rw : MeromorphicAt.{u_1, u_2} (E := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
⊢ MeromorphicAt f x

Tactic:
rw [MeromorphicAt.meromorphicAt_congr h]

Premises used: MeromorphicAt.meromorphicAt_congr
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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.{u_1, u_2} (E := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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

Tactic:
have h₄ : MeromorphicAt f x := by
    rw [MeromorphicAt.meromorphicAt_congr h]
    fun_prop
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
simp : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ¬g x = 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ meromorphicOrderAt f x = (↑n : WithTop ℤ)

Tactic:
simp only [meromorphicOrderAt_eq_int_iff h₄, ne_eq]

Premises used: meromorphicOrderAt_eq_int_iff, ne_eq
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
right : ∀ᶠ (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

Tactic:
use g, h₁g, h₂g
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
h

Premises used: Filter.EventuallyEq
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
exact h
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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 ℤ)

Tactic:
have : meromorphicOrderAt f x = n := by
    simp only [meromorphicOrderAt_eq_int_iff h₄, ne_eq]
    use g, h₁g, h₂g
    exact h
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
this : meromorphicOrderAt f x = (↑n : WithTop ℤ)
⊢ meromorphicTrailingCoeffAt f x = g x

Tactic:
simp_all [meromorphicTrailingCoeffAt_of_eq_nhdsNE h₁g]

Premises used: AnalyticAt.meromorphicTrailingCoeffAt_of_eq_nhdsNE
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
rw : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ HPow.hPow (β := ℤ) (z - x) 0 • f z
⊢ meromorphicTrailingCoeffAt f x = f x

Tactic:
rw [h₁.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE (n := 0) h₂]

Premises used: AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
h : ∀ (a : 𝕜), f a = HPow.hPow (β := ℤ) (a - x) 0 • f a
⊢ f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ HPow.hPow (β := ℤ) (z - x) 0 • f z

Tactic:
filter_upwards
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
⊢ ∀ (a : 𝕜), f a = HPow.hPow (β := ℤ) (a - x) 0 • f a

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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))
neg :
  ∀ (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))

Tactic:
by_cases h₂ : meromorphicOrderAt f x = ⊤

Premises used: meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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 : Tendsto f (𝓝[≠] x) (𝓝 0)
⊢ Tendsto (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-(meromorphicOrderAt f x).untop₀) • f) (𝓝[≠] x)
    (𝓝 (meromorphicTrailingCoeffAt f x))

Tactic:
simp_all only [WithTop.untop₀_top, neg_zero, zpow_zero, one_smul,
      meromorphicTrailingCoeffAt_of_order_eq_top]

Premises used: zpow_zero, WithTop.untop₀_top, MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top, one_smul, neg_zero
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
pos₁ : Tendsto.{u_1, u_2} (β := E) 0 (𝓝[≠] x) (𝓝 0)
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)

Tactic:
apply Tendsto.congr' (f₁ := 0)

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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 = ⊤
h₁ : ∀ (y : 𝕜) (hy : f y = 0), 0 y = f y
⊢ 0 =ᶠ[𝓝[≠] x] f

Tactic:
filter_upwards [meromorphicOrderAt_eq_top_iff.1 h₂] with y hy

Premises used: meromorphicOrderAt_eq_top_iff, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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 = ⊤
y : 𝕜
hy : f y = 0
⊢ 0 y = f y

Tactic:
simp_all