From e5b9559f695bafe7fd369ffb04c3c0585871e58f Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 8 Aug 2024 12:40:32 +0200
Subject: [PATCH] Update holomorphic_examples.lean

---
 Nevanlinna/holomorphic_examples.lean | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

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