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)