Update laplace.lean

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
@@ -106,13 +119,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) :