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