From bfeade409576bc9d94d494dc1ccd7baf29c86d28 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 15 May 2024 21:17:42 +0200
Subject: [PATCH] Update complexHarmonic.lean

---
 Nevanlinna/complexHarmonic.lean | 21 +++++++++------------
 1 file changed, 9 insertions(+), 12 deletions(-)

diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index 1f916e0..536a415 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -159,6 +159,7 @@ theorem logabs_of_holomorphic_is_harmonic
 
     have : (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) = (fun z ↦ (2 : ℝ)⁻¹ • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by
       simp
+      exact rfl
     rw [this]
 
     apply contDiff_iff_contDiffAt.2
@@ -229,18 +230,18 @@ theorem logabs_of_holomorphic_is_harmonic
       exact h₂ z
     rw [this]
     rw [laplace_add]
-    
+
     have : Differentiable ℂ (Complex.log ∘ f) := by
       intro z
-      apply DifferentiableAt.comp 
+      apply DifferentiableAt.comp
       exact Complex.differentiableAt_log (h₃ z)
       exact h₁ z
 
-    have : Complex.laplace (Complex.log ∘ f) = 0 := by
+    have t₁: Complex.laplace (Complex.log ∘ f) = 0 := by
       let A := holomorphic_is_harmonic this
       funext z
       exact A.2 z
-    rw [this]
+    rw [t₁]
     simp
 
     have : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = ⇑(starRingEnd ℂ) ∘ Complex.log ∘ f := by
@@ -253,13 +254,9 @@ theorem logabs_of_holomorphic_is_harmonic
     have : ⇑(starRingEnd ℂ) ∘ Complex.log ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
       rfl
     rw [this]
-    have : ContDiff ℝ 2 (Complex.log ∘ f) := by sorry
-
-    have : Complex.laplace (⇑Complex.conjCLE ∘ f) = ⇑Complex.conjCLE ∘ Complex.laplace (f) := by
-      
-      sorry
-
-    sorry
-
+    rw [laplace_compCLE]
+    rw [t₁]
+    simp
+    sorry
     sorry
     sorry