From 321ceba46b871f2a1015a69da3fd88ff2bf688ae Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Sun, 16 Jun 2024 19:15:19 +0200
Subject: [PATCH] Update holomorphic.primitive.lean

---
 Nevanlinna/holomorphic.primitive.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/Nevanlinna/holomorphic.primitive.lean b/Nevanlinna/holomorphic.primitive.lean
index 46732bd..6ff3e98 100644
--- a/Nevanlinna/holomorphic.primitive.lean
+++ b/Nevanlinna/holomorphic.primitive.lean
@@ -219,6 +219,15 @@ theorem primitive_fderivAtBasepoint
   rw [Filter.eventually_iff_exists_mem]
 
   let s := f⁻¹' Metric.ball (f 0) c
+  have : IsOpen s := by
+    apply IsOpen.mem_nhds
+    apply IsOpen.preimage hf
+    exact Metric.isOpen_ball
+  
+
+  --sorry
+  --apply isOpen_iff_ball_subset
+
   use s
   constructor
   · apply IsOpen.mem_nhds