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 : ℂ → ℂ}