Nevanlinna/laplace.lean

@@ -11,7 +11,6 @@ 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
@@ -80,19 +79,7 @@ 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
-    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₁    
+    sorry
   obtain ⟨v, hv₁, hv₂, hv₃, hv₄⟩ := A₂
 
   have D : ∀ w : ℂ, partialDeriv ℝ w (l ∘ f) =ᶠ[nhds x] l ∘ partialDeriv ℝ w (f) := by
@@ -119,12 +106,13 @@ theorem laplace_compContLinAt {f : ℂ → F} {l : F →L[ℝ] G} {x : ℂ} (h :
   simp
 
   -- DifferentiableAt ℝ (partialDeriv ℝ Complex.I f) x
-  apply ContDiffAt.differentiableAt (partialDeriv_contDiffAt ℝ (ContDiffOn.contDiffAt hv₄ hv₁) Complex.I)
-  rfl
+  unfold partialDeriv
+
+  sorry
 
   -- DifferentiableAt ℝ (partialDeriv ℝ 1 f) x
-  apply ContDiffAt.differentiableAt (partialDeriv_contDiffAt ℝ (ContDiffOn.contDiffAt hv₄ hv₁) 1)
-  rfl
+
+  sorry
 
 
 theorem laplace_compCLE {f : ℂ → F} {l : F ≃L[ℝ] G} (h : ContDiff ℝ 2 f) :