From e843786097d25babc2463f1939b5ba05606010f3 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 7 Nov 2024 09:53:34 +0100
Subject: [PATCH] Cleanup

---
 Nevanlinna/meromorphicAt.lean         | 43 ++++++++++++++++++++++--
 Nevanlinna/meromorphicOn_divisor.lean | 47 +--------------------------
 2 files changed, 42 insertions(+), 48 deletions(-)

diff --git a/Nevanlinna/meromorphicAt.lean b/Nevanlinna/meromorphicAt.lean
index 89f1104..c7f09f0 100644
--- a/Nevanlinna/meromorphicAt.lean
+++ b/Nevanlinna/meromorphicAt.lean
@@ -11,5 +11,44 @@ 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
+  (∀ᶠ (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
diff --git a/Nevanlinna/meromorphicOn_divisor.lean b/Nevanlinna/meromorphicOn_divisor.lean
index 81e99d3..83e2e71 100644
--- a/Nevanlinna/meromorphicOn_divisor.lean
+++ b/Nevanlinna/meromorphicOn_divisor.lean
@@ -1,57 +1,12 @@
 import Mathlib.Analysis.Analytic.Meromorphic
 import Nevanlinna.analyticAt
 import Nevanlinna.divisor
+import Nevanlinna.meromorphicAt
 
 
 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 : ℂ → ℂ}