From 22d9b8aa95210848ea08a6cc8fe947f804ebc7ed Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Sun, 17 Nov 2024 16:56:27 +0100
Subject: [PATCH] Update meromorphicOn.lean

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

diff --git a/Nevanlinna/meromorphicOn.lean b/Nevanlinna/meromorphicOn.lean
index ec8c4a2..86b3749 100644
--- a/Nevanlinna/meromorphicOn.lean
+++ b/Nevanlinna/meromorphicOn.lean
@@ -28,6 +28,8 @@ theorem MeromorphicOn.open_of_order_eq_top
   constructor
   · intro w hw
     simp
+    rw [MeromorphicAt.order_eq_top_iff]
+
     sorry
   · constructor
     · exact isOpen_induced h₂t'