diff --git a/Nevanlinna/laplace.lean b/Nevanlinna/laplace.lean
index bf6f7ec..4a22111 100644
--- a/Nevanlinna/laplace.lean
+++ b/Nevanlinna/laplace.lean
@@ -11,6 +11,7 @@ import Mathlib.Data.Complex.Exponential
 import Mathlib.Analysis.RCLike.Basic
 import Mathlib.Order.Filter.Basic
 import Mathlib.Topology.Algebra.InfiniteSum.Module
+import Mathlib.Topology.Basic
 import Mathlib.Topology.Instances.RealVectorSpace
 import Nevanlinna.cauchyRiemann
 import Nevanlinna.partialDeriv
@@ -79,7 +80,19 @@ theorem laplace_compContLinAt {f : ℂ → F} {l : F →L[ℝ] G} {x : ℂ} (h :
   Complex.laplace (l ∘ f) x = (l ∘ (Complex.laplace f)) x := by
 
   have A₂ : ∃ v ∈ nhds x, (IsOpen v) ∧ (x ∈ v) ∧ (ContDiffOn ℝ 2 f v) := by
-    sorry
+    have : ∃ u ∈ nhds x, ContDiffOn ℝ 2 f u := by
+      apply ContDiffAt.contDiffOn h 
+      rfl
+    obtain ⟨u, hu₁, hu₂⟩ := this
+    obtain ⟨v, hv₁, hv₂, hv₃⟩ := mem_nhds_iff.1 hu₁
+    use v
+    constructor
+    · exact IsOpen.mem_nhds hv₂ hv₃
+    · constructor
+      exact hv₂
+      constructor
+      · exact hv₃
+      · exact ContDiffOn.congr_mono hu₂ (fun x => congrFun rfl) hv₁    
   obtain ⟨v, hv₁, hv₂, hv₃, hv₄⟩ := A₂
 
   have D : ∀ w : ℂ, partialDeriv ℝ w (l ∘ f) =ᶠ[nhds x] l ∘ partialDeriv ℝ w (f) := by