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) :