From 68acec101e1bc8b8d4a77ec7c1a98c1ebd41b2cf Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 18 Nov 2024 19:27:51 +0100
Subject: [PATCH] Update meromorphicOn.lean

---
 Nevanlinna/meromorphicOn.lean | 38 +++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)

diff --git a/Nevanlinna/meromorphicOn.lean b/Nevanlinna/meromorphicOn.lean
index 3e8447c..4ebf212 100644
--- a/Nevanlinna/meromorphicOn.lean
+++ b/Nevanlinna/meromorphicOn.lean
@@ -54,6 +54,44 @@ theorem MeromorphicOn.open_of_order_eq_top
     · exact isOpen_induced h₂t'
     · exact h₃t'
 
+theorem MeromorphicOn.open_of_order_neq_top
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁f : MeromorphicOn f U) :
+  IsOpen { u : U | (h₁f u.1 u.2).order ≠ ⊤ } := by
+
+  apply isOpen_iff_forall_mem_open.mpr
+  intro z hz
+  simp at hz
+
+  let A := (h₁f z.1 z.2).eventually_eq_zero_or_eventually_ne_zero
+  rcases A with h|h
+  · rw [← (h₁f z.1 z.2).order_eq_top_iff] at h
+    tauto
+  · let A := (h₁f z.1 z.2).eventually_analyticAt
+    let B := Filter.Eventually.and h A
+    rw [eventually_nhdsWithin_iff] at B
+    rw [eventually_nhds_iff] at B
+    obtain ⟨t', h₁t', h₂t', h₃t'⟩ := B
+    let t : Set U := Subtype.val ⁻¹' t'
+    use t
+    constructor
+    · intro w hw
+      simp
+      by_cases h₁w : w = z
+      · rwa [h₁w]
+      · let B := h₁t' w hw
+        simp at B
+        have : (w : ℂ) ≠ (z : ℂ) := by exact Subtype.coe_ne_coe.mpr h₁w
+        let C := B this
+        let D := C.2.order_eq_zero_iff.2 C.1
+        rw [C.2.meromorphicAt_order, D]
+        simp
+    · constructor
+      · exact isOpen_induced h₂t'
+      · exact h₃t'
+
+
 theorem MeromorphicOn.order_ne_top
   {f : ℂ → ℂ}
   {U : Set ℂ}