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
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
h₁f₁ : meromorphicOrderAt f₁ x = ⊤
pos : meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₂ x
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x

Tactic:
rw [meromorphicTrailingCoeffAt_of_order_eq_top h₁f₁, zero_add]

Premises used: MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top, zero_add
-- 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
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
h₁f₁ : meromorphicOrderAt f₁ x = ⊤
pos : f₁ + f₂ =ᶠ[𝓝[≠] x] f₂
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₂ x

Tactic:
apply meromorphicTrailingCoeffAt_congr_nhdsNE

Premises used: meromorphicTrailingCoeffAt_congr_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₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
h₁f₁ : meromorphicOrderAt f₁ x = ⊤
h : ∀ (a : 𝕜), f₁ a = 0 → (f₁ + f₂) a = f₂ a
⊢ f₁ + f₂ =ᶠ[𝓝[≠] x] f₂

Tactic:
filter_upwards [meromorphicOrderAt_eq_top_iff.1 h₁f₁]

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
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
h₁f₁ : meromorphicOrderAt f₁ x = ⊤
⊢ ∀ (a : 𝕜), f₁ a = 0 → (f₁ + f₂) a = 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
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicOrderAt f₁ x ≠ ⊤

Tactic:
lia
-- 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
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
neg :
  ∀ (n₁ : ℤ) (hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x) (h₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₂ x)
    (h₁f₁ : ¬(↑n₁ : WithTop ℤ) = ⊤),
    meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x

Tactic:
lift meromorphicOrderAt f₁ x to ℤ using (by lia) with n₁ hn₁

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
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
h₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₂ x
h₁f₁ : ¬(↑n₁ : WithTop ℤ) = ⊤
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 + meromorphicTrailingCoeffAt f₂ x
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x

Tactic:
obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (meromorphicOrderAt_eq_int_iff hf₁).1 hn₁.symm

Premises used: meromorphicOrderAt_eq_int_iff, Iff.mp, Eq.symm
-- 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
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
h₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₂ x
h₁f₁ : ¬(↑n₁ : WithTop ℤ) = ⊤
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
⊢ meromorphicOrderAt f₂ x ≠ ⊤

Tactic:
lia
-- 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
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
h₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₂ x
h₁f₁ : ¬(↑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
neg :
  ∀ (n₂ : ℤ) (hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x) (h₁ : (↑n₁ : WithTop ℤ) = (↑n₂ : WithTop ℤ)),
    meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x

Tactic:
lift meromorphicOrderAt f₂ x to ℤ using (by lia) with n₂ hn₂

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
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
h₁f₁ : ¬(↑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
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
h₁ : (↑n₁ : WithTop ℤ) = (↑n₂ : WithTop ℤ)
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 + meromorphicTrailingCoeffAt f₂ x
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x

Tactic:
obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (meromorphicOrderAt_eq_int_iff hf₂).1 hn₂.symm

Premises used: meromorphicOrderAt_eq_int_iff, Iff.mp, Eq.symm
-- 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
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
h₁f₁ : ¬(↑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
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
h₁ : (↑n₁ : WithTop ℤ) = (↑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
neg :
  ∀ (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₁ = n₂) (g₂ : 𝕜 → E) (h₂ : g₁ x + g₂ x ≠ 0)
    (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 = g₁ x + g₂ x
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x

Tactic:
rw [WithTop.coe_eq_coe, 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₃g₂] at *

Premises used: WithTop.coe_eq_coe, 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₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
h₁f₁ : ¬(↑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
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
h₁ : n₁ = n₂
g₂ : 𝕜 → E
h₂ : g₁ x + g₂ x ≠ 0
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
h :
  ∀ (z : 𝕜) (h₁z : f₁ z = (z - x) ^ n₁ • g₁ z) (h₂z : f₂ z = (z - x) ^ n₂ • g₂ z)
    (h₃z : Membership.mem (γ := Set 𝕜) {x}ᶜ z), (f₁ + f₂) z = (z - x) ^ n₁ • (g₁ + g₂) z
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f₁ + f₂) z = (z - x) ^ n₁ • (g₁ + g₂) z

Tactic:
filter_upwards [h₃g₁, h₃g₂, self_mem_nhdsWithin] with z h₁z h₂z h₃z

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
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
h₁f₁ : ¬(↑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
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
h₁ : n₁ = n₂
g₂ : 𝕜 → E
h₂ : g₁ x + g₂ x ≠ 0
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
z : 𝕜
h₁z : f₁ z = (z - x) ^ n₁ • g₁ z
h₂z : f₂ z = (z - x) ^ n₂ • g₂ z
h₃z : Membership.mem (γ := Set 𝕜) {x}ᶜ z
⊢ (f₁ + f₂) z = (z - x) ^ n₁ • (g₁ + g₂) z

Tactic:
simp_all
-- 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
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
h₁f₁ : ¬(↑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
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
h₁ : n₁ = n₂
g₂ : 𝕜 → E
h₂ : g₁ x + g₂ x ≠ 0
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f₁ + f₂) z = (z - x) ^ n₁ • (g₁ + g₂) z

Tactic:
have τ₀ : ∀ᶠ z in 𝓝[≠] x, (f₁ + f₂) z = (z - x) ^ n₁ • (g₁ + g₂) z := by
    filter_upwards [h₃g₁, h₃g₂, self_mem_nhdsWithin] with z h₁z h₂z h₃z
    simp_all
-- 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
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
h₁f₁ : ¬(↑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
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
h₁ : n₁ = n₂
g₂ : 𝕜 → E
h₂ : g₁ x + g₂ x ≠ 0
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
τ₀ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f₁ + f₂) z = (z - x) ^ n₁ • (g₁ + g₂) z
⊢ AnalyticAt 𝕜 (g₁ + 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₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
h₁f₁ : ¬(↑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
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
h₁ : n₁ = n₂
g₂ : 𝕜 → E
h₂ : g₁ x + g₂ x ≠ 0
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
τ₀ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f₁ + f₂) z = (z - x) ^ n₁ • (g₁ + g₂) z
⊢ (g₁ + g₂) x ≠ 0

Tactic:
simp_all
-- 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
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : (↑n₁ : WithTop ℤ) = meromorphicOrderAt f₁ x
h₁f₁ : ¬(↑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
n₂ : ℤ
hn₂ : (↑n₂ : WithTop ℤ) = meromorphicOrderAt f₂ x
h₁ : n₁ = n₂
g₂ : 𝕜 → E
h₂ : g₁ x + g₂ x ≠ 0
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
τ₀ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f₁ + f₂) z = (z - x) ^ n₁ • (g₁ + g₂) z
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = g₁ x + g₂ x

Tactic:
simp [AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE (by fun_prop)
    (by simp_all) τ₀]

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₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
⊢ meromorphicTrailingCoeffAt (fun (z : 𝕜) ↦ f₁ z + f₂ z) x =
    meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x

Tactic:
MeromorphicAt.meromorphicTrailingCoeffAt_add_eq_add hf₁ hf₂ h₁ h₂

Premises used: MeromorphicAt.meromorphicTrailingCoeffAt_add_eq_add
-- 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
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0
⊢ MeromorphicAt (-f₂) 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₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0
rw :
  meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt (-f₂) x =
    meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x
h₃ : meromorphicOrderAt f₁ x = meromorphicOrderAt (-f₂) x
h₄ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt (-f₂) x ≠ 0
⊢ meromorphicTrailingCoeffAt (f₁ - f₂) x = meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x

Tactic:
rw [sub_eq_add_neg, hf₁.meromorphicTrailingCoeffAt_add_eq_add (by fun_prop)]

Premises used: MeromorphicAt.meromorphicTrailingCoeffAt_add_eq_add, sub_eq_add_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₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0
rw :
  meromorphicTrailingCoeffAt f₁ x + -meromorphicTrailingCoeffAt f₂ x =
    meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x
rw₁ rw₂ :
  meromorphicTrailingCoeffAt f₁ x + -meromorphicTrailingCoeffAt f₂ x =
    meromorphicTrailingCoeffAt f₁ x + -meromorphicTrailingCoeffAt f₂ x
⊢ meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt (-f₂) x =
    meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x

Tactic:
rw [meromorphicTrailingCoeffAt_neg, sub_eq_add_neg]

Premises used: sub_eq_add_neg, meromorphicTrailingCoeffAt_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₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0
h₃ h₄ h₅ h₆ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt (-f₂) x

Tactic:
rwa [← 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₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0
h₃ : meromorphicTrailingCoeffAt f₁ x + -meromorphicTrailingCoeffAt f₂ x ≠ 0
h₄ h₅ h₆ h₇ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0
⊢ meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt (-f₂) x ≠ 0

Tactic:
rwa [meromorphicTrailingCoeffAt_neg, ←sub_eq_add_neg]

Premises used: sub_eq_add_neg, meromorphicTrailingCoeffAt_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₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0
⊢ meromorphicTrailingCoeffAt (fun (z : 𝕜) ↦ f₁ z - f₂ z) x =
    meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x

Tactic:
MeromorphicAt.meromorphicTrailingCoeffAt_sub_eq_sub hf₁ hf₂ h₁ h₂

Premises used: MeromorphicAt.meromorphicTrailingCoeffAt_sub_eq_sub
-- 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
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
pos :
  ∀ (h₁f₁ : meromorphicOrderAt f₁ x = ⊤),
    meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
neg :
  ∀ (h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤),
    meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
⊢ meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x

Tactic:
by_cases h₁f₁ : 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
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁f₁ : meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x

Tactic:
simp_all [meromorphicOrderAt_smul hf₁ hf₂]

Premises used: meromorphicOrderAt_smul
-- 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
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
pos :
  ∀ (h₁f₂ : meromorphicOrderAt f₂ x = ⊤),
    meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
neg :
  ∀ (h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤),
    meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
⊢ meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x

Tactic:
by_cases h₁f₂ : 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
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
h₁f₂ : meromorphicOrderAt f₂ x = ⊤
⊢ meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x

Tactic:
simp_all [meromorphicOrderAt_smul hf₁ hf₂]

Premises used: meromorphicOrderAt_smul
-- 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
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤
neg :
  ∀ (g₁ : 𝕜 → 𝕜) (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₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
⊢ meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x

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

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
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁f₁ : ¬meromorphicOrderAt f₁ x = ⊤
h₁f₂ : ¬meromorphicOrderAt f₂ x = ⊤
g₁ : 𝕜 → 𝕜
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₂ : 𝕜 → 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₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
⊢ meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x

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

Premises used: meromorphicOrderAt_ne_top_iff, Iff.mp