From 12888b75fbc02b1a9a795215cda3b09e92956446 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 18 Nov 2024 18:44:42 +0100
Subject: [PATCH] Update meromorphicOn.lean

---
 Nevanlinna/meromorphicOn.lean | 25 ++++++++++++++++++++++---
 1 file changed, 22 insertions(+), 3 deletions(-)

diff --git a/Nevanlinna/meromorphicOn.lean b/Nevanlinna/meromorphicOn.lean
index 86b3749..3e8447c 100644
--- a/Nevanlinna/meromorphicOn.lean
+++ b/Nevanlinna/meromorphicOn.lean
@@ -18,19 +18,38 @@ theorem MeromorphicOn.open_of_order_eq_top
   apply isOpen_iff_forall_mem_open.mpr
   intro z hz
   simp at hz
+
+  have h₁z := hz
   rw [MeromorphicAt.order_eq_top_iff] at hz
   rw [eventually_nhdsWithin_iff] at hz
   rw [eventually_nhds_iff] at hz
   obtain ⟨t', h₁t', h₂t', h₃t'⟩ := hz
-
   let t : Set U := Subtype.val ⁻¹' t'
   use t
   constructor
   · intro w hw
     simp
-    rw [MeromorphicAt.order_eq_top_iff]
+    by_cases h₁w : w = z
+    · rwa [h₁w]
+    · --
+      rw [MeromorphicAt.order_eq_top_iff]
+      rw [eventually_nhdsWithin_iff]
+      rw [eventually_nhds_iff]
+      use t' \ {z.1}
+      constructor
+      · intro y h₁y h₂y
+        apply h₁t'
+        exact Set.mem_of_mem_diff h₁y
+        exact Set.mem_of_mem_inter_right h₁y
+      · constructor
+        · apply IsOpen.sdiff h₂t'
+          exact isClosed_singleton
+        · rw [Set.mem_diff]
+          constructor
+          · exact hw
+          · simp
+            exact Subtype.coe_ne_coe.mpr h₁w
 
-    sorry
   · constructor
     · exact isOpen_induced h₂t'
     · exact h₃t'