From fb642a4ed0114275a6d15dd17f17ba886fccee0f Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 14 Nov 2024 16:18:32 +0100
Subject: [PATCH] working

---
 Nevanlinna/meromorphicOn_decompose.lean | 11 +++++++++++
 Nevanlinna/stronglyMeromorphicAt.lean   |  2 +-
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/Nevanlinna/meromorphicOn_decompose.lean b/Nevanlinna/meromorphicOn_decompose.lean
index 88666cf..691fc76 100644
--- a/Nevanlinna/meromorphicOn_decompose.lean
+++ b/Nevanlinna/meromorphicOn_decompose.lean
@@ -10,6 +10,17 @@ 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₂U : IsCompact U)
+  (h₁f : MeromorphicOn f U)
+  (h₂f : ∃ z₀ ∈ U, f z₀ ≠ 0) :
+  ∀ hz : z ∈ U, (h₁f z hz).order ≠ ⊤ := by
+
+  sorry
+
 
 theorem MeromorphicOn.decompose
   {f : ℂ → ℂ}
diff --git a/Nevanlinna/stronglyMeromorphicAt.lean b/Nevanlinna/stronglyMeromorphicAt.lean
index bb40d85..de7cb10 100644
--- a/Nevanlinna/stronglyMeromorphicAt.lean
+++ b/Nevanlinna/stronglyMeromorphicAt.lean
@@ -348,7 +348,7 @@ theorem makeStronglyMeromorphic_id
   · exact m₁ (StronglyMeromorphicAt.meromorphicAt hf) z hz
 
 
-theorem StronglyMeromorphicAt.decompose
+theorem StronglyMeromorphicAt.eliminate
   {f : ℂ → ℂ}
   {z₀ : ℂ}
   (h₁f : StronglyMeromorphicAt f z₀)