import Mathlib.Analysis.Analytic.Meromorphic
import Nevanlinna.analyticAt
import Nevanlinna.divisor
import Nevanlinna.meromorphicAt
import Nevanlinna.meromorphicOn_divisor
import Nevanlinna.stronglyMeromorphicOn
import Nevanlinna.mathlibAddOn

open scoped Interval Topology
open Real Filter MeasureTheory intervalIntegral

theorem MeromorphicOn.order_ne_top
  {f : ℂ → ℂ}
  {U : Set ℂ}
  (h₁U : IsConnected U)
  (h₁f : MeromorphicOn f U) :
  (∃ z₀ : U, (h₁f z₀.1 z₀.2).order ≠ ⊤) ↔ (∀ z : U, (h₁f z.1 z.2).order ≠ ⊤) := by

  constructor
  · intro h
    obtain ⟨h₁z₀, h₂z₀⟩ := h
    intro hz

    sorry

  · intro h
    obtain ⟨w, hw⟩ := h₁U.nonempty
    use ⟨w, hw⟩
    exact h ⟨w, hw⟩