From 12397c30554ae729e216d46eeb1bb9350eb7ef0b Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 16 Dec 2024 12:43:00 +0100
Subject: [PATCH] =?UTF-8?q?Working=E2=80=A6?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Nevanlinna/meromorphicOn.lean         |  1 -
 Nevanlinna/meromorphicOn_divisor.lean | 25 +++++++++++++++++++++----
 2 files changed, 21 insertions(+), 5 deletions(-)

diff --git a/Nevanlinna/meromorphicOn.lean b/Nevanlinna/meromorphicOn.lean
index 94bef60..fe5e141 100644
--- a/Nevanlinna/meromorphicOn.lean
+++ b/Nevanlinna/meromorphicOn.lean
@@ -2,7 +2,6 @@ import Mathlib.Analysis.Analytic.Meromorphic
 import Nevanlinna.analyticAt
 import Nevanlinna.divisor
 import Nevanlinna.meromorphicAt
-import Nevanlinna.meromorphicOn_divisor
 import Nevanlinna.stronglyMeromorphicOn
 import Nevanlinna.mathlibAddOn
 
diff --git a/Nevanlinna/meromorphicOn_divisor.lean b/Nevanlinna/meromorphicOn_divisor.lean
index 793392e..94353f4 100644
--- a/Nevanlinna/meromorphicOn_divisor.lean
+++ b/Nevanlinna/meromorphicOn_divisor.lean
@@ -2,6 +2,7 @@ import Mathlib.Analysis.Analytic.Meromorphic
 import Nevanlinna.analyticAt
 import Nevanlinna.divisor
 import Nevanlinna.meromorphicAt
+import Nevanlinna.meromorphicOn
 import Nevanlinna.stronglyMeromorphicOn
 
 
@@ -183,17 +184,33 @@ theorem StronglyMeromorphicOn.analyticOnNhd
     tauto
   assumption
 
+
 theorem StronglyMeromorphicOn.support_divisor
   {f : ℂ → ℂ}
   {U : Set ℂ}
-  (hU : IsPreconnected U)
+  (hU : IsConnected U)
   (h₁f : StronglyMeromorphicOn f U)
-  (h₂f : ∃ u ∈ U, f u ≠ 0) :
+  (h₂f : ∃ u : U, f u ≠ 0) :
   U ∩ f⁻¹' {0} = (Function.support h₁f.meromorphicOn.divisor) := by
 
   ext u
   constructor
-  · sorry
+  · intro hu
+    unfold MeromorphicOn.divisor
+    simp [MeromorphicOn.order_ne_top hU h₁f h₂f ⟨u, hu.1⟩]
+    use hu.1
+    rw [(h₁f u hu.1).order_eq_zero_iff]
+    simp
+    exact hu.2
   · intro hu
     simp at hu
-    sorry
+    let A := h₁f.meromorphicOn.divisor.supportInU hu
+    constructor
+    · exact h₁f.meromorphicOn.divisor.supportInU hu
+    · simp
+      let B := (h₁f u A).order_eq_zero_iff.not
+      simp at B
+      rw [← B]
+      unfold MeromorphicOn.divisor at hu
+      simp [A] at hu
+      exact hu.1