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