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

---
 Nevanlinna/complexHarmonic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index 57ba7c7..686ad1b 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -254,7 +254,7 @@ theorem logabs_of_holomorphic_is_harmonic
       rfl
     rw [this]
     have : ContDiff ℝ 2 (Complex.log ∘ f) := by sorry
-    have : Complex.laplace (⇑Complex.conjCLE ∘ f) = ⇑Complex.conjCLE ∘ Complex.laplace (f) := by
+    have : Complex.laplace (⇑Complex.imCLM ∘ f) = ⇑Complex.imCLM ∘ Complex.laplace (f) := by
       apply laplace_compContLin
 
       sorry