From 47ab90446f9acf74071de2e8c73502e266bf2e46 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 30 May 2024 10:05:13 +0200
Subject: [PATCH] Update laplace.lean

---
 Nevanlinna/laplace.lean | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/Nevanlinna/laplace.lean b/Nevanlinna/laplace.lean
index ccc4b8a..bf6f7ec 100644
--- a/Nevanlinna/laplace.lean
+++ b/Nevanlinna/laplace.lean
@@ -106,13 +106,12 @@ theorem laplace_compContLinAt {f : ℂ → F} {l : F →L[ℝ] G} {x : ℂ} (h :
   simp
 
   -- DifferentiableAt ℝ (partialDeriv ℝ Complex.I f) x
-  unfold partialDeriv
-
-  sorry
+  apply ContDiffAt.differentiableAt (partialDeriv_contDiffAt ℝ (ContDiffOn.contDiffAt hv₄ hv₁) Complex.I)
+  rfl
 
   -- DifferentiableAt ℝ (partialDeriv ℝ 1 f) x
-
-  sorry
+  apply ContDiffAt.differentiableAt (partialDeriv_contDiffAt ℝ (ContDiffOn.contDiffAt hv₄ hv₁) 1)
+  rfl
 
 
 theorem laplace_compCLE {f : ℂ → F} {l : F ≃L[ℝ] G} (h : ContDiff ℝ 2 f) :