import Mathlib.Analysis.Meromorphic.Basic
import Mathlib.Analysis.Meromorphic.Order

open MeromorphicOn Metric Real Set Classical

variable
  {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]

/-- Derivatives of meromorphic functions are meromorphic. -/
theorem meromorphicAt_deriv_of_order_eq_top {f : 𝕜 → 𝕜} {x : 𝕜}
    (h : MeromorphicAt f x) (h₁ : h.order ≠ ⊤) :
    MeromorphicAt (deriv f) x := by

  have := h.eventually_analyticAt
  obtain ⟨n, hn⟩ := h

  let g : 𝕜 → 𝕜 := sorry
  rw [MeromorphicAt.meromorphicAt_congr]

  sorry