From f480ae2a0fb9a69f2a3dbe2ccc96bd65868eeb00 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 30 May 2024 09:57:36 +0200
Subject: [PATCH] Update partialDeriv.lean

---
 Nevanlinna/partialDeriv.lean | 29 ++++++++++++-----------------
 1 file changed, 12 insertions(+), 17 deletions(-)

diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean
index ce41acc..7ca77f9 100644
--- a/Nevanlinna/partialDeriv.lean
+++ b/Nevanlinna/partialDeriv.lean
@@ -91,30 +91,25 @@ theorem partialDeriv_contDiff {n : ℕ} {f : E → F} (h : ContDiff 𝕜 (n + 1)
 
 
 theorem partialDeriv_contDiffAt {n : ℕ} {f : E → F} {x : E} (h : ContDiffAt 𝕜 (n + 1) f x) : ∀ v : E, ContDiffAt 𝕜 n (partialDeriv 𝕜 v f) x := by
+
   unfold partialDeriv
   intro v
 
-  let A' := (contDiffAt_succ_iff_hasFDerivAt.1 h)
-  obtain ⟨f', ⟨u, hu₁, hu₂⟩ , hf'⟩ := A'
+  let eval_at_v : (E →L[𝕜] F) →L[𝕜] F := 
+  {
+    toFun := fun l ↦ l v
+    map_add' := by simp
+    map_smul' := by simp
+  }
 
-  have : (fun w => (fderiv 𝕜 f w) v) = (fun f => f v) ∘ (fun w => (fderiv 𝕜 f w)) := by
+  have : (fun w => (fderiv 𝕜 f w) v) = eval_at_v ∘ (fun w => (fderiv 𝕜 f w)) := by
     rfl
   rw [this]
-  apply ContDiffAt.comp
-  apply fderiv_clm_apply
 
-  let A := (contDiffAt_succ_iff_fderiv.1 h).right
-  simp at A
-
-  have : (fun w => (fderiv 𝕜 f w) v) = (fun f => f v) ∘ (fun w => (fderiv 𝕜 f w)) := by
-    rfl
-
-  rw [this]
-  refine ContDiff.comp ?hg A
-  refine ContDiff.of_succ ?hg.h
-  refine ContDiff.clm_apply ?hg.h.hf ?hg.h.hg
-  exact contDiff_id
-  exact contDiff_const
+  apply ContDiffAt.continuousLinearMap_comp
+  -- ContDiffAt 𝕜 (↑n) (fun w => fderiv 𝕜 f w) x
+  apply ContDiffAt.fderiv_right h
+  rfl
 
 
 lemma partialDeriv_fderiv {f : E → F} (hf : ContDiff 𝕜 2 f) (z a b : E) :