diff --git a/Nevanlinna/holomorphic_examples.lean b/Nevanlinna/holomorphic_examples.lean
index e3cedd2..5ed5fca 100644
--- a/Nevanlinna/holomorphic_examples.lean
+++ b/Nevanlinna/holomorphic_examples.lean
@@ -252,15 +252,16 @@ theorem harmonic_is_realOfHolomorphic
 
   constructor
   · -- ∀ (z : ℂ), HolomorphicAt F z
-    intro z
+    intro x hx
     apply HolomorphicAt_iff.2
-    use Set.univ
+    use Metric.ball z R
     constructor
-    · exact isOpen_const
+    · exact Metric.isOpen_ball
     · constructor
-      · simp
-      · intro w _
-        exact regF w
+      · assumption
+      · intro w hw
+        apply (regF w hw).differentiableAt
+        apply IsOpen.mem_nhds Metric.isOpen_ball hw
   · -- (F z).re = f z
     have A := reg₂f.differentiable one_le_two
     have B : Differentiable ℝ (Complex.reCLM ∘ F) := by