From ad5e7c69fdac8efc763fda7e91fdc0cafc19fc6b Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 7 Aug 2024 09:24:55 +0200
Subject: [PATCH] Update holomorphic_primitive2.lean

---
 Nevanlinna/holomorphic_primitive2.lean | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/Nevanlinna/holomorphic_primitive2.lean b/Nevanlinna/holomorphic_primitive2.lean
index b2d28e6..1e4c877 100644
--- a/Nevanlinna/holomorphic_primitive2.lean
+++ b/Nevanlinna/holomorphic_primitive2.lean
@@ -258,7 +258,12 @@ theorem primitive_hasDerivAtBasepoint
   HasDerivAt (primitive z₀ f) (f z₀) z₀ := by
 
   let g := f ∘ fun z ↦ z + z₀
-  have : Continuous g := by continuity
+  have : ContinuousAt g 0 := by
+    apply ContinuousAt.comp
+    simpa
+    apply ContinuousAt.add
+    exact fun ⦃U⦄ a => a
+    exact continuousAt_const
   let A := primitive_fderivAtBasepointZero g this
   simp at A