diff --git a/Nevanlinna/holomorphic_JensenFormula2.lean b/Nevanlinna/holomorphic_JensenFormula2.lean
index 3030ca6..b446012 100644
--- a/Nevanlinna/holomorphic_JensenFormula2.lean
+++ b/Nevanlinna/holomorphic_JensenFormula2.lean
@@ -7,30 +7,31 @@ import Nevanlinna.specialFunctions_CircleIntegral_affine
 
 open Real
 
-lemma h₁U : IsPreconnected (Metric.closedBall (0 : ℂ) 1) :=
-  (convex_closedBall (0 : ℂ) 1).isPreconnected
-
-lemma h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) :=
-  isCompact_closedBall 0 1
 
 
 theorem jensen_case_R_eq_one
   (f : ℂ → ℂ)
-  (h'₁f : AnalyticOn ℂ f (Metric.closedBall (0 : ℂ) 1))
+  (h₁f : AnalyticOn ℂ f (Metric.closedBall (0 : ℂ) 1))
   (h₂f : f 0 ≠ 0) :
-  log ‖f 0‖ = -∑ᶠ s, (h'₁f.order s).toNat * log (‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 1 x)‖ := by
+  log ‖f 0‖ = -∑ᶠ s, (h₁f.order s).toNat * log (‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 1 x)‖ := by
+
+  have h₁U : IsPreconnected (Metric.closedBall (0 : ℂ) 1) :=
+    (convex_closedBall (0 : ℂ) 1).isPreconnected
+
+  have h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) :=
+    isCompact_closedBall 0 1
 
   have h'₂f : ∃ u ∈ (Metric.closedBall (0 : ℂ) 1), f u ≠ 0 := by
     use 0; simp; exact h₂f
 
-  obtain ⟨F, h₁F, h₂F, h₃F⟩ := AnalyticOnCompact.eliminateZeros₂ h₁U h₂U h'₁f h'₂f
+  obtain ⟨F, h₁F, h₂F, h₃F⟩ := AnalyticOnCompact.eliminateZeros₂ h₁U h₂U h₁f h'₂f
 
   have h'₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by
     intro z h₁z
     apply AnalyticAt.holomorphicAt
     exact h₁F z h₁z
 
-  let G := fun z ↦ log ‖F z‖ + ∑ s ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset, (h'₁f.order s).toNat * log ‖z - s‖
+  let G := fun z ↦ log ‖F z‖ + ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order s).toNat * log ‖z - s‖
 
   have decompose_f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → log ‖f z‖ = G z := by
     intro z h₁z h₂z
@@ -59,7 +60,7 @@ theorem jensen_case_R_eq_one
     abel
 
     -- ∀ x ∈ ⋯.toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0
-    have : ∀ x ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0 := by
+    have : ∀ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, Complex.abs (z - ↑x) ^ (h₁f.order x).toNat ≠ 0 := by
       intro s hs
       simp at hs
       simp
@@ -69,7 +70,7 @@ theorem jensen_case_R_eq_one
     exact this
 
     -- ∏ x ∈ ⋯.toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0
-    have : ∀ x ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0 := by
+    have : ∀ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, Complex.abs (z - ↑x) ^ (h₁f.order x).toNat ≠ 0 := by
       intro s hs
       simp at hs
       simp
@@ -104,7 +105,7 @@ theorem jensen_case_R_eq_one
     apply Set.Countable.mono t₀
     apply Set.Countable.preimage_circleMap
     apply Set.Finite.countable
-    let A := finiteZeros h₁U h₂U h'₁f h'₂f
+    let A := finiteZeros h₁U h₂U h₁f h'₂f
 
     have : (Metric.closedBall 0 1 ∩ f ⁻¹' {0}) = (Metric.closedBall 0 1).restrict f ⁻¹' {0} := by
       ext z
@@ -117,7 +118,7 @@ theorem jensen_case_R_eq_one
 
   have decompose_int_G : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x)
     = (∫ (x : ℝ) in (0)..2 * π, log (Complex.abs (F (circleMap 0 1 x))))
-        + ∑ x ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset, (h'₁f.order x).toNat * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - ↑x)) := by
+        + ∑ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order x).toNat * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - ↑x)) := by
     dsimp [G]
     rw [intervalIntegral.integral_add]
     rw [intervalIntegral.integral_finset_sum]
@@ -175,8 +176,8 @@ theorem jensen_case_R_eq_one
     apply Continuous.continuousAt
     apply continuous_circleMap
 
-    have : (fun x => ∑ s ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset, (h'₁f.order s).toNat * log (Complex.abs (circleMap 0 1 x - ↑s)))
-      = ∑ s ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset, (fun x => (h'₁f.order s).toNat * log (Complex.abs (circleMap 0 1 x - ↑s))) := by
+    have : (fun x => ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order s).toNat * log (Complex.abs (circleMap 0 1 x - ↑s)))
+      = ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (fun x => (h₁f.order s).toNat * log (Complex.abs (circleMap 0 1 x - ↑s))) := by
       funext x
       simp
     rw [this]
@@ -252,7 +253,7 @@ theorem jensen_case_R_eq_one
   rw [log_prod]
   simp
 
-  rw [finsum_eq_sum_of_support_subset _ (s := (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset)]
+  rw [finsum_eq_sum_of_support_subset _ (s := (finiteZeros h₁U h₂U h₁f h'₂f).toFinset)]
   simp
   simp
   intro x ⟨h₁x, _⟩
@@ -260,7 +261,7 @@ theorem jensen_case_R_eq_one
 
   dsimp [AnalyticOn.order] at h₁x
   simp only [Function.mem_support, ne_eq, Nat.cast_eq_zero, not_or] at h₁x
-  exact AnalyticAt.supp_order_toNat (AnalyticOn.order.proof_1 h'₁f x) h₁x
+  exact AnalyticAt.supp_order_toNat (AnalyticOn.order.proof_1 h₁f x) h₁x
 
   --
   intro x hx