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