Update meromorphicOn.lean

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
-
+  · constructor
-
+    · exact isOpen_induced h₂t'
-
+    · exact h₃t'
-  rw [← eventually_eventually_nhds] at hz
-
-
-  sorry
-
 
 theorem MeromorphicOn.order_ne_top
   {f : ℂ → ℂ}