From 637c0cf17555e94de70b0a12c97813c118ba023d Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 31 May 2024 16:10:06 +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 7e6b12c..e45212b 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -112,7 +112,7 @@ theorem harmonic_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (h : Harmonic
   Harmonic (c • f) := by
   constructor
   · exact ContDiff.const_smul c h.1
-  · rw [laplace_smul h.1]
+  · rw [laplace_smul]
     dsimp
     intro z
     rw [h.2 z]