From 656d50e36794891d2de820d0f393c67daff12c10 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 7 Aug 2024 12:28:36 +0200
Subject: [PATCH] Update holomorphic_primitive2.lean

---
 Nevanlinna/holomorphic_primitive2.lean | 29 +++++++++++++-------------
 1 file changed, 15 insertions(+), 14 deletions(-)

diff --git a/Nevanlinna/holomorphic_primitive2.lean b/Nevanlinna/holomorphic_primitive2.lean
index a202aef..a26590d 100644
--- a/Nevanlinna/holomorphic_primitive2.lean
+++ b/Nevanlinna/holomorphic_primitive2.lean
@@ -20,8 +20,9 @@ theorem primitive_zeroAtBasepoint
 
 theorem primitive_fderivAtBasepointZero
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  (f : ℂ  → E)
-  (hf : ContinuousAt f 0) :
+  {f : ℂ  → E}
+  {R : ℝ}
+  (hf : ContinuousOn f (Metric.ball 0 R)) :
   HasDerivAt (primitive 0 f) (f 0) 0 := by
   unfold primitive
   simp
@@ -277,19 +278,20 @@ theorem primitive_translation
 theorem primitive_hasDerivAtBasepoint
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
   {f : ℂ  → E}
+  {R : ℝ}
   (z₀ : ℂ)
-  (hf : ContinuousAt f z₀) :
+  (hf : ContinuousOn f (Metric.ball z₀ R)) :
   HasDerivAt (primitive z₀ f) (f z₀) z₀ := by
 
   let g := f ∘ fun z ↦ z + z₀
-  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
+  have hg : ContinuousOn g (Metric.ball 0 R) := by
+    apply ContinuousOn.comp
+    fun_prop
+    fun_prop
+    intro x hx
+    simp
+    simp at hx
+    assumption
 
   let B := primitive_translation g z₀ z₀
   simp at B
@@ -299,8 +301,7 @@ theorem primitive_hasDerivAtBasepoint
     simp
   rw [this] at B
   rw [B]
-  have : f z₀ = (1 : ℂ) • (f z₀) := by
-    exact (MulAction.one_smul (f z₀)).symm
+  have : f z₀ = (1 : ℂ) • (f z₀) := (MulAction.one_smul (f z₀)).symm
   conv =>
     arg 2
     rw [this]
@@ -309,7 +310,7 @@ theorem primitive_hasDerivAtBasepoint
   simp
   have : g 0 = f z₀ := by simp [g]
   rw [← this]
-  exact A
+  exact primitive_fderivAtBasepointZero hg
   apply HasDerivAt.sub_const
   have : (fun (x : ℂ) ↦ x) = id := by
     funext x