diff --git a/Nevanlinna/analyticOnNhd_divisor.lean b/Nevanlinna/analyticOnNhd_divisor.lean
index e55ffaf..42d00cb 100644
--- a/Nevanlinna/analyticOnNhd_divisor.lean
+++ b/Nevanlinna/analyticOnNhd_divisor.lean
@@ -2,6 +2,7 @@ import Mathlib.Analysis.SpecialFunctions.Integrals
 import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
 import Mathlib.Analysis.Convex.SpecificFunctions.Deriv
 import Nevanlinna.analyticAt
+import Nevanlinna.divisor
 
 open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
@@ -9,89 +10,24 @@ open Real Filter MeasureTheory intervalIntegral
 
 
 
-structure Divisor where
-  toFun : ℂ → ℤ
-  -- This is not what we want. We want: locally finite
-  discreteSupport : DiscreteTopology (Function.support toFun)
-
-instance : CoeFun Divisor (fun _ ↦ ℂ → ℤ) where
-coe := Divisor.toFun
-attribute [coe] Divisor.toFun
-
-
-
-noncomputable def Divisor.deg
-  (D : Divisor) : ℤ := ∑ᶠ z, D z
-
-noncomputable def Divisor.n_trunk
-  (D : Divisor) : ℤ → ℝ → ℤ := fun k r ↦ ∑ᶠ z ∈ Metric.ball 0 r, min k (D z)
-
-noncomputable def Divisor.n
-  (D : Divisor) : ℝ → ℤ := fun r ↦ ∑ᶠ z ∈ Metric.ball 0 r, D z
-
-noncomputable def Divisor.N_trunk
-  (D : Divisor) : ℤ → ℝ → ℝ := fun k r ↦ ∫ (t : ℝ) in (1)..r, (D.n_trunk k t) / t
-
-
-theorem Divisor.support_cap_closed₁
-  {S U : Set ℂ}
-  (hS : DiscreteTopology S)
-  (hU : IsClosed U) :
-  IsClosed (U ∩ S) := by
-
-  rw [← isOpen_compl_iff]
-  rw [isOpen_iff_forall_mem_open]
-  intro x hx
-  by_cases h₁x : x ∈ U
-  · simp at hx
-
-
-    sorry
-  · use Uᶜ
-    constructor
-    · simp
-    · constructor
-      · exact IsClosed.isOpen_compl
-      · assumption
-
-
-
-theorem Divisor.support_cap_closed
-  (D : Divisor)
-  {U : Set ℂ}
-  (h₁U : IsClosed U) :
-  IsClosed (U ∩ D.toFun.support) := by
-  sorry
-
-
-theorem Divisor.support_cap_compact
-  (D : Divisor)
-  {U : Set ℂ}
-  (h₁U : IsCompact U) :
-  Set.Finite (U ∩ (Function.support D)) := by
-
-  apply IsCompact.finite
-  -- Target set is compact
-  apply h₁U.of_isClosed_subset
-  apply D.support_cap_closed h₁U.isClosed
-  exact Set.inter_subset_left
-  -- Target set is discrete
-  apply DiscreteTopology.of_subset D.discreteSupport
-  exact Set.inter_subset_right
-
-
 noncomputable def AnalyticOnNhd.zeroDivisor
   {f : ℂ → ℂ}
   {U : Set ℂ}
   (hf : AnalyticOnNhd ℂ f U) :
-  Divisor where
+  Divisor U where
+
+  toFun := by
+    intro z
+    if hz : z ∈ U then
+      exact ((hf z hz).order.toNat : ℤ)
+    else
+      exact 0
+
+  supportInU := by
+    intro z hz
+    simp only [Function.mem_support] at hz
+    simp only [Function.mem_support, ne_eq, dite_eq_else, Nat.cast_eq_zero, ENat.toNat_eq_zero, not_forall, not_or] at hz
 
-    toFun := by
-      intro z
-      if hz : z ∈ U then
-        exact ((hf z hz).order.toNat : ℤ)
-      else
-        exact 0
 
     discreteSupport := by
       simp_rw [← singletons_open_iff_discrete]
diff --git a/Nevanlinna/holomorphic_JensenFormula.lean b/Nevanlinna/holomorphic_JensenFormula.lean
index 9153f04..63e02a7 100644
--- a/Nevanlinna/holomorphic_JensenFormula.lean
+++ b/Nevanlinna/holomorphic_JensenFormula.lean
@@ -1,6 +1,6 @@
 import Mathlib.Analysis.Complex.CauchyIntegral
 import Mathlib.Analysis.Analytic.IsolatedZeros
-import Nevanlinna.analyticOn_zeroSet
+import Nevanlinna.analyticOnNhd_zeroSet
 import Nevanlinna.harmonicAt_examples
 import Nevanlinna.harmonicAt_meanValue
 import Nevanlinna.specialFunctions_CircleIntegral_affine
diff --git a/Nevanlinna/holomorphic_primitive.lean b/Nevanlinna/holomorphic_primitive.lean
index c132007..b134449 100644
--- a/Nevanlinna/holomorphic_primitive.lean
+++ b/Nevanlinna/holomorphic_primitive.lean
@@ -666,7 +666,7 @@ theorem primitive_additivity'
       dsimp [ε']; simp
       have : |ε| = ε := by apply abs_of_pos h₁ε
       rw [this]
-      apply (inv_mul_lt_iff zero_lt_two).mpr
+      apply (inv_mul_lt_iff₀ zero_lt_two).mpr
       linarith
     have h₁ε' : 0 < ε' := by
       apply mul_pos _ h₁ε
diff --git a/Nevanlinna/holomorphic_zero.lean b/Nevanlinna/holomorphic_zero.lean
index d69e717..6252f52 100644
--- a/Nevanlinna/holomorphic_zero.lean
+++ b/Nevanlinna/holomorphic_zero.lean
@@ -3,7 +3,7 @@ import Mathlib.Analysis.Analytic.Meromorphic
 import Mathlib.Topology.ContinuousOn
 import Mathlib.Analysis.Analytic.IsolatedZeros
 import Nevanlinna.holomorphic
-import Nevanlinna.analyticOn_zeroSet
+import Nevanlinna.analyticOnNhd_zeroSet
 
 
 noncomputable def zeroDivisor
diff --git a/lake-manifest.json b/lake-manifest.json
index b241ad5..7a13544 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bf12ff6041cbab6eba6b54d9467baed807bb2bfd",
+   "rev": "daf1ed91789811cf6bbb7bf2f4dad6b3bad8fbf4",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
+   "rev": "2b2f6d7fbe9d917fc010e9054c1ce11774c9088b",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "50aaaf78b7db5bd635c19c660d59ed31b9bc9b5a",
+   "rev": "b20a88676fd00affb90cbc9f1ff004ae588103b3",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
+   "rev": "63a7d4a353f48f6c5f1bc19d0f018b0513cb370a",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2ba60fa2c384a94735454db11a2d523612eaabff",
+   "rev": "4b61d4abc1659f15ffda5ec24fdebc229d51d066",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "eed3300c27c9f168d53e13bb198a92a147b671d0",
+   "rev": "cbe02ad0a6243d7688e60d69fd7ee0387d6f8059",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
diff --git a/lean-toolchain b/lean-toolchain
index 98556ba..eff86fd 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.12.0-rc1
+leanprover/lean4:v4.13.0-rc3