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

---
 Nevanlinna/laplace.lean | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

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