From 2146909338edb0ce44f9d6c3569bb4441166ba0d Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 4 Nov 2024 13:22:12 +0100
Subject: [PATCH] Working (hard)

---
 Nevanlinna/meromorphicAt.lean         | 15 ++++
 Nevanlinna/meromorphicOn_divisor.lean | 98 +++++++++++++++++++++------
 2 files changed, 94 insertions(+), 19 deletions(-)
 create mode 100644 Nevanlinna/meromorphicAt.lean

diff --git a/Nevanlinna/meromorphicAt.lean b/Nevanlinna/meromorphicAt.lean
new file mode 100644
index 0000000..89f1104
--- /dev/null
+++ b/Nevanlinna/meromorphicAt.lean
@@ -0,0 +1,15 @@
+import Mathlib.Analysis.Analytic.Meromorphic
+import Nevanlinna.analyticAt
+import Nevanlinna.divisor
+
+
+open scoped Interval Topology
+open Real Filter MeasureTheory intervalIntegral
+
+
+theorem MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicAt f z₀) :
+  (∀ᶠ (z : ℂ) in nhds z₀, f z = 0) ∨ ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z ≠ 0 := by
+  sorry
diff --git a/Nevanlinna/meromorphicOn_divisor.lean b/Nevanlinna/meromorphicOn_divisor.lean
index 80b12b7..81e99d3 100644
--- a/Nevanlinna/meromorphicOn_divisor.lean
+++ b/Nevanlinna/meromorphicOn_divisor.lean
@@ -6,6 +6,52 @@ import Nevanlinna.divisor
 open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
 
+theorem MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicAt f z₀) :
+  (∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = 0) ∨ ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z ≠ 0 := by
+
+  obtain ⟨n, h⟩ := hf
+  let A := h.eventually_eq_zero_or_eventually_ne_zero
+
+  rw [eventually_nhdsWithin_iff]
+  rw [eventually_nhds_iff]
+  rcases A with h₁|h₂
+  · rw [eventually_nhds_iff] at h₁
+    obtain ⟨N, h₁N, h₂N, h₃N⟩ := h₁
+    left
+    use N
+    constructor
+    · intro y h₁y h₂y
+      let A := h₁N y h₁y
+      simp at A
+      rcases A with h₃|h₄
+      · let B := h₃.1
+        simp at h₂y
+        let C := sub_eq_zero.1 B
+        tauto
+      · assumption
+    · constructor
+      · exact h₂N
+      · exact h₃N
+  · right
+    rw [eventually_nhdsWithin_iff]
+    rw [eventually_nhds_iff]
+    rw [eventually_nhdsWithin_iff] at h₂
+    rw [eventually_nhds_iff] at h₂
+    obtain ⟨N, h₁N, h₂N, h₃N⟩ := h₂
+    use N
+    constructor
+    · intro y h₁y h₂y
+      by_contra h
+      let A := h₁N y h₁y h₂y
+      rw [h] at A
+      simp at A
+    · constructor
+      · exact h₂N
+      · exact h₃N
+
 
 noncomputable def MeromorphicOn.divisor
   {f : ℂ → ℂ}
@@ -32,30 +78,44 @@ noncomputable def MeromorphicOn.divisor
     apply eventually_nhdsWithin_iff.2
     rw [eventually_nhds_iff]
 
-    rcases AnalyticAt.eventually_eq_zero_or_eventually_ne_zero (hf z hz) with h|h
-    · rw [eventually_nhds_iff] at h
-      obtain ⟨N, h₁N, h₂N, h₃N⟩ := h
-      use N
-      constructor
-      · intro y h₁y _
-        by_cases h₃y : y ∈ U
-        · simp [h₃y]
-          right
-          rw [AnalyticAt.order_eq_top_iff (hf y h₃y)]
-          rw [eventually_nhds_iff]
-          use N
-        · simp [h₃y]
-      · tauto
-
-    · rw [eventually_nhdsWithin_iff, eventually_nhds_iff] at h
+    rcases MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero (hf z hz) with h|h
+    · rw [eventually_nhdsWithin_iff] at h
+      rw [eventually_nhds_iff] at h
       obtain ⟨N, h₁N, h₂N, h₃N⟩ := h
       use N
       constructor
       · intro y h₁y h₂y
         by_cases h₃y : y ∈ U
         · simp [h₃y]
-          left
-          rw [AnalyticAt.order_eq_zero_iff (hf y h₃y)]
-          exact h₁N y h₁y h₂y
+          right
+          rw [MeromorphicAt.order_eq_top_iff (hf y h₃y)]
+          rw [eventually_nhdsWithin_iff]
+          rw [eventually_nhds_iff]
+          use N ∩ {z}ᶜ
+          constructor
+          · intro x h₁x _
+            exact h₁N x h₁x.1 h₁x.2
+          · constructor
+            · exact IsOpen.inter h₂N isOpen_compl_singleton
+            · exact Set.mem_inter h₁y h₂y
+        · simp [h₃y]
+      · tauto
+
+    · let A := (hf z hz).eventually_analyticAt
+      let B := Filter.eventually_and.2 ⟨h, A⟩
+      rw [eventually_nhdsWithin_iff, eventually_nhds_iff] at B
+      obtain ⟨N, h₁N, h₂N, h₃N⟩ := B
+      use N
+      constructor
+      · intro y h₁y h₂y
+        by_cases h₃y : y ∈ U
+        · simp [h₃y]
+          left
+          rw [(h₁N y h₁y h₂y).2.meromorphicAt_order]
+          let D := (h₁N y h₁y h₂y).2.order_eq_zero_iff.2
+          let C := (h₁N y h₁y h₂y).1
+          let E := D C
+          rw [E]
+          simp
         · simp [h₃y]
       · tauto