diff --git a/Nevanlinna/holomorphic_JensenFormula.lean b/Nevanlinna/holomorphic_JensenFormula.lean
index e138191..33ccc26 100644
--- a/Nevanlinna/holomorphic_JensenFormula.lean
+++ b/Nevanlinna/holomorphic_JensenFormula.lean
@@ -48,8 +48,9 @@ theorem jensen_case_R_eq_one
   simp at t₁
   rw [t₁]
   simp
-  have : Real.pi⁻¹ * 2⁻¹ * (2 * Real.pi * (logAbsf 0 - ∑ x ∈ S.attach, Real.log (Complex.abs (a x)))) = logAbsf 0 - ∑ x ∈ S.attach, Real.log (Complex.abs (a x)) := by
-    sorry
+  have {w : ℝ} : Real.pi⁻¹ * 2⁻¹ * (2 * Real.pi * w) = w := by
+    ring_nf
+    simp [mul_inv_cancel Real.pi_ne_zero]
   rw [this]
   simp
   rfl