From 6d36769dab91ec387fe9a674480ab5dd32554363 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 14 Jun 2024 21:00:51 +0200
Subject: [PATCH] Update holomorphic.primitive.lean

---
 Nevanlinna/holomorphic.primitive.lean | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/Nevanlinna/holomorphic.primitive.lean b/Nevanlinna/holomorphic.primitive.lean
index 137e34a..d9940bf 100644
--- a/Nevanlinna/holomorphic.primitive.lean
+++ b/Nevanlinna/holomorphic.primitive.lean
@@ -153,11 +153,11 @@ theorem primitive_zeroAtBasepoint
 theorem primitive_lem1
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] [IsScalarTower ℝ ℂ E]
   (v : E) :
-  HasDerivAt (primitive 0 (fun z ↦ v)) v 0 := by
+  HasDerivAt (primitive 0 (fun _ ↦ v)) v 0 := by
   unfold primitive
   simp
 
-  have : (fun (z : ℂ) => z.re • v + Complex.I • z.im • v) = (fun (z : ℂ) => z • v) := by
+  have : (fun (z : ℂ) => z.re • v + Complex.I • z.im • v) = (fun (y : ℂ) => ((fun w ↦ w)  y) • v) := by
     funext z
     rw [smul_comm]
     rw [← smul_assoc]
@@ -166,13 +166,11 @@ theorem primitive_lem1
     rw [this, ← add_smul]
     simp
   rw [this]
-
-
-  apply HasDerivAt.smul_const
-
-
-
-  sorry
+  
+  have hc : HasDerivAt (fun (w : ℂ) ↦ w) 1 0 := by 
+    apply hasDerivAt_id'
+  nth_rewrite 2 [← (one_smul ℂ v)]
+  exact HasDerivAt.smul_const hc v
 
 
 
@@ -182,7 +180,9 @@ theorem primitive_fderivAtBasepoint
   HasDerivAt (primitive 0 f) (f 0) 0 := by
   unfold primitive
   simp
-
+  apply hasDerivAt_iff_isLittleO.2
+  simp
+  
   sorry