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 : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
⊢ EventuallyEq.{u_1, u_2} (β := E) (𝓝[≠] x) 0 0

Tactic:
rfl
-- 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 = ⊤
⊢ Tendsto.{u_1, u_2} (β := E) 0 (𝓝[≠] x) (𝓝 0)

Tactic:
apply Tendsto.congr' (f₁ := 0) (by rfl) continuousWithinAt_const.tendsto

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 = ⊤
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))
⊢ 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₂

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

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

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 = ⊤
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
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
⊢ g =ᶠ[𝓝[≠] x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-(meromorphicOrderAt f x).untop₀) • f

Tactic:
filter_upwards [h₃g, self_mem_nhdsWithin] with 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 : 𝕜 → 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
h₁ :
  y - x ≠ 0 ∨
    -(meromorphicOrderAt f x).untop₀ + (meromorphicOrderAt f x).untop₀ ≠ 0 ∨
      -(meromorphicOrderAt f x).untop₀ = 0 ∧ (meromorphicOrderAt f x).untop₀ = 0
⊢ g y = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (-(meromorphicOrderAt f x).untop₀) • f) y

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]

Premises used: smul_assoc, zpow_zero, Pi.smul_apply', zpow_add', one_smul, Pi.pow_apply, neg_add_cancel, zpow_neg, smul_eq_mul, Pi.inv_apply
-- 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 = ⊤
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
h₁ : y - x ≠ 0
⊢ y - x ≠ 0 ∨
    -(meromorphicOrderAt f x).untop₀ + (meromorphicOrderAt f x).untop₀ ≠ 0 ∨
      -(meromorphicOrderAt f x).untop₀ = 0 ∧ (meromorphicOrderAt f x).untop₀ = 0

Tactic:
left
-- 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 = ⊤
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

Tactic:
simp_all [sub_ne_zero]

Premises used: sub_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 : 𝕜 → 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 : Tendsto g (𝓝[≠] x) (𝓝 (g x))
⊢ Tendsto g (𝓝[≠] x) (𝓝 (meromorphicTrailingCoeffAt f x))

Tactic:
rw [h₁g.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 : 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) (𝓝 (g x))

Tactic:
apply h₁g.continuousAt.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, AnalyticAt.continuousAt
-- 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 ≠ ⊤
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
⊢ meromorphicTrailingCoeffAt f x ≠ 0

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

Premises used: 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 : 𝕜 → 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
⊢ meromorphicTrailingCoeffAt f x ≠ 0

Tactic:
simpa [h₁g.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE h₂g h₃g] using h₂g

Premises used: AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x e : 𝕜
pos : ∀ (he : e = 0), meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ e) x = e
neg : ∀ (he : ¬e = 0), meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ e) x = e
⊢ meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ e) x = e

Tactic:
by_cases he : e = 0
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x e : 𝕜
he : e = 0
pos : Eq (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ 0) x) 0
⊢ meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ e) x = e

Tactic:
rw [he]
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x e : 𝕜
he : e = 0
pos : meromorphicOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ 0) x = ⊤
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ 0) x) 0

Tactic:
apply MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top

Premises used: MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x e : 𝕜
he : e = 0
pos : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ meromorphicOrderAt (E := 𝕜) (fun (x : 𝕜) ↦ 0) x = ⊤

Tactic:
rw [meromorphicOrderAt_eq_top_iff]

Premises used: meromorphicOrderAt_eq_top_iff
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x e : 𝕜
he : e = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, Eq.{u_1 + 1} (α := 𝕜) 0 0

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x e : 𝕜
he : ¬e = 0
⊢ meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ e) x = e

Tactic:
analyticAt_const.meromorphicTrailingCoeffAt_of_ne_zero he

Premises used: analyticAt_const, AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x e : 𝕜
he : ¬e = 0
⊢ meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ e) x = e

Tactic:
exact analyticAt_const.meromorphicTrailingCoeffAt_of_ne_zero he

Premises used: analyticAt_const, AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
neg : ∀ (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

Tactic:
by_cases h : x = y
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : DecidableEq 𝕜
x y : 𝕜
h : x = y
pos : Eq (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) y) 1
⊢ meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x = if x = y then 1 else x - y

Tactic:
simp_all only [sub_self, ite_true]

Premises used: sub_self, ite_true
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : DecidableEq 𝕜
x y : 𝕜
h : x = y
⊢ AnalyticAt 𝕜 (F := 𝕜) (fun {y : 𝕜} ↦ 1) y

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : DecidableEq 𝕜
x y : 𝕜
h : x = y
⊢ Ne.{u_1 + 1} (α := 𝕜) 1 0

Tactic:
apply one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : DecidableEq 𝕜
x y : 𝕜
h : x = y
pos :
  (𝓝[≠] y).EventuallyEq (β := 𝕜) (fun (x : 𝕜) ↦ x - y) fun (z : 𝕜) ↦
    HSMul.hSMul (β := 𝕜) (HPow.hPow (β := ℤ) (z - y) 1) 1
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) y) 1

Tactic:
apply AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE (n := 1) (by fun_prop)
      (by apply one_ne_zero)

Premises used: AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : DecidableEq 𝕜
x y : 𝕜
h : x = y
⊢ (𝓝[≠] y).EventuallyEq (β := 𝕜) (fun (x : 𝕜) ↦ x - y) fun (z : 𝕜) ↦
    HSMul.hSMul (β := 𝕜) (HPow.hPow (β := ℤ) (z - y) 1) 1

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : DecidableEq 𝕜
x y : 𝕜
h : ¬x = y
neg : meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x = x - y
⊢ meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x = if x = y then 1 else x - y

Tactic:
simp_all only [ite_false]

Premises used: ite_false
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : DecidableEq 𝕜
x y : 𝕜
h : ¬x = y
⊢ AnalyticAt 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ x - y) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : DecidableEq 𝕜
x y : 𝕜
h : ¬x = y
neg : x - y ≠ 0
⊢ meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x = x - y

Tactic:
apply AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero (by fun_prop)

Premises used: AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : DecidableEq 𝕜
x y : 𝕜
h : ¬x = y
⊢ x - y ≠ 0

Tactic:
simp_all [sub_ne_zero]

Premises used: sub_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
x : 𝕜
f₁ f₂ : 𝕜 → E
h : f₁ =ᶠ[𝓝[≠] x] f₂
pos : ∀ (h₁ : ¬MeromorphicAt f₁ x), meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
neg : ∀ (h₁ : ¬¬MeromorphicAt f₁ x), meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
⊢ meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x

Tactic:
by_cases h₁ : ¬MeromorphicAt f₁ x

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

Tactic:
simp [h₁, (MeromorphicAt.meromorphicAt_congr h).not.1 h₁]

Premises used: Iff.not, MeromorphicAt.meromorphicAt_congr, 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
x : 𝕜
f₁ f₂ : 𝕜 → E
h : f₁ =ᶠ[𝓝[≠] x] f₂
h₁ : ¬¬MeromorphicAt f₁ x
⊢ MeromorphicAt f₁ x

Tactic:
rw [not_not] at h₁

Premises used: Classical.not_not
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
neg : ∀ (h₂ : ¬meromorphicOrderAt f₁ x = ⊤), meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
⊢ meromorphicTrailingCoeffAt 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
x : 𝕜
f₁ f₂ : 𝕜 → E
h : f₁ =ᶠ[𝓝[≠] x] f₂
h₁ : MeromorphicAt f₁ x
h₂ : meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x

Tactic:
simp_all [meromorphicOrderAt_congr h]

Premises used: meromorphicOrderAt_congr
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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 = ⊤
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
⊢ meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x

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

Premises used: 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
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
neg₁ neg₂ : g x = g x
⊢ meromorphicTrailingCoeffAt f₁ 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)]

Premises used: Filter.EventuallyEq.trans, Filter.EventuallyEq.symm, 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
x : 𝕜
f : 𝕜 → E
pos : ∀ (h₁ : ¬MeromorphicAt f x), meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x
neg : ∀ (h₁ : ¬¬MeromorphicAt f x), meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x
⊢ meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x

Tactic:
by_cases h₁ : ¬ MeromorphicAt f x

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

Tactic:
aesop
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
⊢ MeromorphicAt f x

Tactic:
rw [not_not] at h₁

Premises used: Classical.not_not
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
neg : ∀ (h₂ : ¬meromorphicOrderAt f x = ⊤), meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x
⊢ meromorphicTrailingCoeffAt (-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
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
⊢ meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x

Tactic:
simp_all [← meromorphicOrderAt_neg]

Premises used: meromorphicOrderAt_neg
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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 = ⊤
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
⊢ meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x

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

Premises used: 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
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 : meromorphicTrailingCoeffAt (-f) x = -g x
⊢ meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x

Tactic:
rw [h₁g.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE h₂g h₃g]

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
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
neg₂ : -f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt (-f) x).untop₀ • (-g) z
⊢ meromorphicTrailingCoeffAt (-f) x = -g x

Tactic:
rw [AnalyticAt.meromorphicTrailingCoeffAt_of_eq_nhdsNE (g := -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
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
⊢ (-g) x = -g x

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
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
⊢ AnalyticAt 𝕜 (-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
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
h :
  ∀ (a : 𝕜) (ha : f a = (a - x) ^ (meromorphicOrderAt f x).untop₀ • g a),
    (-f) a = (a - x) ^ (meromorphicOrderAt (-f) x).untop₀ • (-g) a
⊢ -f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt (-f) x).untop₀ • (-g) z

Tactic:
filter_upwards [h₃g] with a ha
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
a : 𝕜
ha : f a = (a - x) ^ (meromorphicOrderAt f x).untop₀ • g a
⊢ (-f) a = (a - x) ^ (meromorphicOrderAt (-f) x).untop₀ • (-g) a

Tactic:
simp [ha, ← meromorphicOrderAt_neg]

Premises used: meromorphicOrderAt_neg
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
⊢ meromorphicTrailingCoeffAt (fun (z : 𝕜) ↦ -f z) x = -meromorphicTrailingCoeffAt f x

Tactic:
meromorphicTrailingCoeffAt_neg

Premises used: meromorphicTrailingCoeffAt_neg