English
If two functions agree in a punctured neighbourhood of x, then their trailing coefficients at x are equal.
Русский
Если две функции совпадают в окрестности точки x с удалением x, то их хвостовые коэффициенты в x совпадают.
LaTeX
$$$$ f_1 =_{\mathcal{N}(x)\setminus\{x\}} f_2 \Rightarrow \mathrm{meromorphicTrailingCoeffAt}(f_1,x) = \mathrm{meromorphicTrailingCoeffAt}(f_2,x). $$$$
Lean4
/-- If two functions agree in a punctured neighborhood, then their trailing coefficients agree.
-/
theorem meromorphicTrailingCoeffAt_congr_nhdsNE {f₁ f₂ : 𝕜 → E} (h : f₁ =ᶠ[𝓝[≠] x] f₂) :
meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x :=
by
by_cases h₁ : ¬MeromorphicAt f₁ x
· simp [h₁, (MeromorphicAt.meromorphicAt_congr h).not.1 h₁]
rw [not_not] at h₁
by_cases h₂ : meromorphicOrderAt f₁ x = ⊤
· simp_all [meromorphicOrderAt_congr h]
obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_ne_top_iff h₁).1 h₂
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)]
