diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index 5a3f612..da7ec8b 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -142,18 +142,18 @@ theorem logabs_of_holomorphic_is_harmonic
 
   constructor
   · -- logabs f is real C²
-    have : (fun z ↦ Real.log ‖f z‖) = (Real.log ∘ Complex.normSq ∘ f) / 2 := by
+    have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
       funext z
       simp
       unfold Complex.abs
       simp
       rw [Real.log_sqrt]
-      exact Complex.normSq_nonneg (f z)
+      rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2]
+      exact Complex.normSq_nonneg (f z)  
     rw [this]
-    have : Real.log ∘ ⇑Complex.normSq ∘ f / 2 = (fun z ↦ (1 / (2 : ℝ)) • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by
-      funext z
+
+    have : (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) = (fun z ↦ (2 : ℝ)⁻¹ • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by
       simp
-      exact div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2
     rw [this]
 
     apply contDiff_iff_contDiffAt.2
@@ -169,5 +169,5 @@ theorem logabs_of_holomorphic_is_harmonic
     exact ContDiff.contDiffAt f_is_real_C2
 
   · -- Laplace vanishes
-  
+
     sorry