From 6e204a0348b2eb8b913686d59dfd13bf491f6950 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Sat, 16 Nov 2024 13:24:50 +0100
Subject: [PATCH] Update meromorphicOn.lean

---
 Nevanlinna/meromorphicOn.lean | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

diff --git a/Nevanlinna/meromorphicOn.lean b/Nevanlinna/meromorphicOn.lean
index 01d1559..ec8c4a2 100644
--- a/Nevanlinna/meromorphicOn.lean
+++ b/Nevanlinna/meromorphicOn.lean
@@ -22,17 +22,16 @@ theorem MeromorphicOn.open_of_order_eq_top
   rw [eventually_nhdsWithin_iff] at hz
   rw [eventually_nhds_iff] at hz
   obtain ⟨t', h₁t', h₂t', h₃t'⟩ := hz
-  let t :=
-  have : t ⊆ { u : U | (h₁f u.1 u.2).order = ⊤} := by
+
+  let t : Set U := Subtype.val ⁻¹' t'
+  use t
+  constructor
+  · intro w hw
+    simp
     sorry
-
-
-
-  rw [← eventually_eventually_nhds] at hz
-
-
-  sorry
-
+  · constructor
+    · exact isOpen_induced h₂t'
+    · exact h₃t'
 
 theorem MeromorphicOn.order_ne_top
   {f : ℂ → ℂ}