From e1eb1463e8db519cdb99e3cb763635355462702e Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 3 Jun 2024 13:41:33 +0200
Subject: [PATCH] Cleanup

---
 Nevanlinna/complexHarmonic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index 398e6ef..26d7482 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -308,7 +308,6 @@ theorem holomorphicOn_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} (hs : IsOpe
     simp
 
 
-
 theorem re_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
   Harmonic (Complex.reCLM ∘ f) := by
   apply harmonic_comp_CLM_is_harmonic
@@ -327,7 +326,7 @@ theorem antiholomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f)
   exact holomorphic_is_harmonic h
 
 
-theorem log_normSq_of_holomorphicOn_is_harmonicOn
+theorem log_normSq_of_holomorphicOn_is_harmonicOn'
   {f : ℂ → ℂ}
   {s : Set ℂ}
   (hs : IsOpen s)
@@ -409,6 +408,7 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
   apply holomorphicOn_is_harmonicOn hs
   exact DifferentiableOn.clog h₁ h₃
 
+
 theorem log_normSq_of_holomorphic_is_harmonic
   {f : ℂ → ℂ}
   (h₁ : Differentiable ℂ f)