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'