diff --git a/Nevanlinna/analyticOn_zeroSet.lean b/Nevanlinna/analyticOn_zeroSet.lean
index 8a9cebc..b431384 100644
--- a/Nevanlinna/analyticOn_zeroSet.lean
+++ b/Nevanlinna/analyticOn_zeroSet.lean
@@ -233,3 +233,216 @@ theorem AnalyticOn.eliminateZeros
       rw [Finset.prod_insert]
       ring
       exact hb
+
+
+theorem XX
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hU : IsPreconnected U)
+  (h₁f : AnalyticOn ℂ f U)
+  (h₂f : ∃ u ∈ U, f u ≠ 0) :
+  ∀ (hu : u ∈ U), (h₁f u hu).order.toNat = (h₁f u hu).order := by
+
+  intro hu
+  apply ENat.coe_toNat
+  by_contra C
+  rw [(h₁f u hu).order_eq_top_iff] at C
+  rw [← (h₁f u hu).frequently_zero_iff_eventually_zero] at C
+  obtain ⟨u₁, h₁u₁, h₂u₁⟩ := h₂f
+  rw [(h₁f.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hu C) h₁u₁] at h₂u₁
+  tauto
+
+
+theorem discreteZeros
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hU : IsPreconnected U)
+  (h₁f : AnalyticOn ℂ f U)
+  (h₂f : ∃ u ∈ U, f u ≠ 0) :
+  DiscreteTopology ↑(U ∩ f⁻¹' {0}) := by
+
+  simp_rw [← singletons_open_iff_discrete]
+  simp_rw [Metric.isOpen_singleton_iff]
+
+  intro z
+
+  let A := XX hU h₁f h₂f z.2.1
+  rw [eq_comm] at A
+  rw [AnalyticAt.order_eq_nat_iff] at A
+  obtain ⟨g, h₁g, h₂g, h₃g⟩ := A
+
+  rw [Metric.eventually_nhds_iff_ball] at h₃g
+  have : ∃ ε > 0, ∀ y ∈ Metric.ball (↑z) ε, g y ≠ 0 := by
+    have h₄g : ContinuousAt g z := AnalyticAt.continuousAt h₁g
+    have : {0}ᶜ ∈ nhds (g z) := by
+      exact compl_singleton_mem_nhds_iff.mpr h₂g
+
+    let F := h₄g.preimage_mem_nhds this
+    rw [Metric.mem_nhds_iff] at F
+    obtain ⟨ε, h₁ε, h₂ε⟩ := F
+    use ε
+    constructor; exact h₁ε
+    intro y hy
+    let G := h₂ε hy
+    simp at G
+    exact G
+  obtain ⟨ε₁, h₁ε₁⟩ := this
+
+  obtain ⟨ε₂, h₁ε₂, h₂ε₂⟩ := h₃g
+  use min ε₁ ε₂
+  constructor
+  · have : 0 < min ε₁ ε₂ := by
+      rw [lt_min_iff]
+      exact And.imp_right (fun _ => h₁ε₂) h₁ε₁
+    exact this
+
+  intro y
+  intro h₁y
+
+  have h₂y : ↑y ∈ Metric.ball (↑z) ε₂ := by
+    simp
+    calc dist y z
+    _ < min ε₁ ε₂ := by assumption
+    _ ≤ ε₂ := by exact min_le_right ε₁ ε₂
+
+  have h₃y : ↑y ∈ Metric.ball (↑z) ε₁ := by
+    simp
+    calc dist y z
+    _ < min ε₁ ε₂ := by assumption
+    _ ≤ ε₁ := by exact min_le_left ε₁ ε₂
+
+
+  have F := h₂ε₂ y.1 h₂y
+  rw [y.2.2] at F
+  simp at F
+
+  have : g y.1 ≠ 0 := by
+    exact h₁ε₁.2 y h₃y
+  simp [this] at F
+  ext
+  rw [sub_eq_zero] at F
+  tauto
+
+
+theorem finiteZeros
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁U : IsPreconnected U)
+  (h₂U : IsCompact U)
+  (h₁f : AnalyticOn ℂ f U)
+  (h₂f : ∃ u ∈ U, f u ≠ 0) :
+  Set.Finite ↑(U ∩ f⁻¹' {0}) := by
+
+  have hinter : IsCompact ↑(U ∩ f⁻¹' {0}) := by
+    apply IsCompact.of_isClosed_subset h₂U
+    apply h₁f.continuousOn.preimage_isClosed_of_isClosed
+    exact IsCompact.isClosed h₂U
+    exact isClosed_singleton
+    exact Set.inter_subset_left
+
+  apply hinter.finite
+  apply DiscreteTopology.of_subset (s := ↑(U ∩ f⁻¹' {0}))
+  exact discreteZeros h₁U h₁f h₂f
+  rfl
+
+
+
+theorem AnalyticOnCompact.eliminateZeros
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁U : IsPreconnected U)
+  (h₂U : IsCompact U)
+  (h₁f : AnalyticOn ℂ f U)
+  (h₂f : ∃ u ∈ U, f u ≠ 0) :
+  ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a ∈ U, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z := by
+
+
+  let A := U ∩ f ⁻¹' {0}
+
+  by sorry -- (finiteZeros h₁U h₂U h₁f h₂f).toFinset
+  let B := AnalyticOn.eliminateZeros h₁f
+
+
+  apply Finset.induction (α := U) (p := fun A ↦ (∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z)
+
+  -- case empty
+  simp
+  use f
+  simp
+  exact hf
+
+  -- case insert
+  intro b₀ B hb iHyp
+  intro hBinsert
+  obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀⟩ := iHyp (fun a ha ↦ hBinsert a (Finset.mem_insert_of_mem ha))
+
+  have : (h₁g₀ b₀ b₀.2).order = n b₀ := by
+
+    rw [← hBinsert b₀ (Finset.mem_insert_self b₀ B)]
+
+    let φ := fun z ↦ (∏ a ∈ B, (z - a.1) ^ n a.1)
+
+    have : f = fun z ↦ φ z * g₀ z := by
+      funext z
+      rw [h₃g₀ z]
+      rfl
+    simp_rw [this]
+
+    have h₁φ : AnalyticAt ℂ φ b₀ := by
+      dsimp [φ]
+      apply Finset.analyticAt_prod
+      intro b _
+      apply AnalyticAt.pow
+      apply AnalyticAt.sub
+      apply analyticAt_id ℂ
+      exact analyticAt_const
+
+    have h₂φ : h₁φ.order = (0 : ℕ) := by
+      rw [AnalyticAt.order_eq_nat_iff h₁φ 0]
+      use φ
+      constructor
+      · assumption
+      · constructor
+        · dsimp [φ]
+          push_neg
+          rw [Finset.prod_ne_zero_iff]
+          intro a ha
+          simp
+          have : ¬ (b₀.1 - a.1 = 0) := by
+            by_contra C
+            rw [sub_eq_zero] at C
+            rw [SetCoe.ext C] at hb
+            tauto
+          tauto
+        · simp
+
+    rw [AnalyticAt.order_mul h₁φ (h₁g₀ b₀ b₀.2)]
+
+    rw [h₂φ]
+    simp
+
+
+  obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ b₀.2 (n b₀)).1 this
+
+  use g₁
+  constructor
+  · exact h₁g₁
+  · constructor
+    · intro a h₁a
+      by_cases h₂a : a = b₀
+      · rwa [h₂a]
+      · let A' := Finset.mem_of_mem_insert_of_ne h₁a h₂a
+        let B' := h₃g₁ a
+        let C' := h₂g₀ a A'
+        rw [B'] at C'
+        exact right_ne_zero_of_smul C'
+    · intro z
+      let A' := h₃g₀ z
+      rw [h₃g₁ z] at A'
+      rw [A']
+      rw [← smul_assoc]
+      congr
+      simp
+      rw [Finset.prod_insert]
+      ring
+      exact hb
diff --git a/Nevanlinna/holomorphic_zero.lean b/Nevanlinna/holomorphic_zero.lean
index 2e5fbf7..a4017c6 100644
--- a/Nevanlinna/holomorphic_zero.lean
+++ b/Nevanlinna/holomorphic_zero.lean
@@ -282,186 +282,6 @@ theorem zeroDivisor_finiteOnCompact
   exact Set.inter_subset_right
 
 
-theorem AnalyticOn.order_eq_nat_iff
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  {z₀ : ℂ}
-  (hf : AnalyticOn ℂ f U)
-  (hz₀ : z₀ ∈ U)
-  (n : ℕ) :
-  (hf z₀ hz₀).order = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by
-
-  constructor
-  -- Direction →
-  intro hn
-  obtain ⟨gloc, h₁gloc, h₂gloc, h₃gloc⟩ := (AnalyticAt.order_eq_nat_iff (hf z₀ hz₀) n).1 hn
-
-  -- Define a candidate function; this is (f z) / (z - z₀) ^ n with the
-  -- removable singularity removed
-  let g : ℂ → ℂ := fun z ↦ if z = z₀ then gloc z₀ else (f z) / (z - z₀) ^ n
-
-  -- Describe g near z₀
-  have g_near_z₀ : ∀ᶠ (z : ℂ) in nhds z₀, g z = gloc z := by
-    rw [eventually_nhds_iff]
-    obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 h₃gloc
-    use t
-    constructor
-    · intro y h₁y
-      by_cases h₂y : y = z₀
-      · dsimp [g]; simp [h₂y]
-      · dsimp [g]; simp [h₂y]
-        rw [div_eq_iff_mul_eq, eq_comm, mul_comm]
-        exact h₁t y h₁y
-        norm_num
-        rw [sub_eq_zero]
-        tauto
-    · constructor
-      · assumption
-      · assumption
-
-  -- Describe g near points z₁ that are different from z₀
-  have g_near_z₁ {z₁ : ℂ} : z₁ ≠ z₀ → ∀ᶠ (z : ℂ) in nhds z₁, g z = f z / (z - z₀) ^ n := by
-    intro hz₁
-    rw [eventually_nhds_iff]
-    use {z₀}ᶜ
-    constructor
-    · intro y hy
-      simp at hy
-      simp [g, hy]
-    · exact ⟨isOpen_compl_singleton, hz₁⟩
-
-  -- Use g and show that it has all required properties
-  use g
-  constructor
-  · -- AnalyticOn ℂ g U
-    intro z h₁z
-    by_cases h₂z : z = z₀
-    · rw [h₂z]
-      apply AnalyticAt.congr h₁gloc
-      exact Filter.EventuallyEq.symm g_near_z₀
-    · simp_rw [eq_comm] at g_near_z₁
-      apply AnalyticAt.congr _ (g_near_z₁ h₂z)
-      apply AnalyticAt.div
-      exact hf z h₁z
-      apply AnalyticAt.pow
-      apply AnalyticAt.sub
-      apply analyticAt_id
-      apply analyticAt_const
-      simp
-      rw [sub_eq_zero]
-      tauto
-  · constructor
-    · simp [g]; tauto
-    · intro z
-      by_cases h₂z : z = z₀
-      · rw [h₂z, g_near_z₀.self_of_nhds]
-        exact h₃gloc.self_of_nhds
-      · rw [(g_near_z₁ h₂z).self_of_nhds]
-        simp [h₂z]
-        rw [div_eq_mul_inv, mul_comm, mul_assoc, inv_mul_cancel]
-        simp; norm_num
-        rw [sub_eq_zero]
-        tauto
-
-  -- direction ←
-  intro h
-  obtain ⟨g, h₁g, h₂g, h₃g⟩ := h
-  rw [AnalyticAt.order_eq_nat_iff]
-  use g
-  exact ⟨h₁g z₀ hz₀, ⟨h₂g, Filter.eventually_of_forall h₃g⟩⟩
-
-
-theorem AnalyticOn.order_eq_nat_iff'
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  {A : Finset U}
-  (hf : AnalyticOn ℂ f U)
-  (n : A → ℕ) :
-  ∀ a : A, (hf a (Subtype.coe_prop a.val)).order = n a → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a, g a ≠ 0) ∧ ∀ z, f z = (∏ a, (z - a) ^ (n a)) • g z := by
-
-  apply Finset.induction
-
-  let a : A := by sorry
-  let b : ℂ := by sorry
-  let u : U := by sorry
-
-  let X := n a
-  have : a = (3 : ℂ) := by sorry
-  have : b ∈ ↑A := by sorry
-  have : ↑a ∈ U := by exact Subtype.coe_prop a.val
-
-  let Y := ∀ a : A, (hf a (Subtype.coe_prop a.val)).order = n a
-
-  --∀ a : A, (hf (ha a)).order = ↑(n a) →
-
-  intro hn
-  obtain ⟨gloc, h₁gloc, h₂gloc, h₃gloc⟩ := (AnalyticAt.order_eq_nat_iff (hf z₀ hz₀) n).1 hn
-
-  -- Define a candidate function
-  let g : ℂ → ℂ := fun z ↦ if z = z₀ then gloc z₀ else (f z) / (z - z₀) ^ n
-
-  -- Describe g near z₀
-  have g_near_z₀ : ∀ᶠ (z : ℂ) in nhds z₀, g z = gloc z := by
-    rw [eventually_nhds_iff]
-    obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 h₃gloc
-    use t
-    constructor
-    · intro y h₁y
-      by_cases h₂y : y = z₀
-      · dsimp [g]; simp [h₂y]
-      · dsimp [g]; simp [h₂y]
-        rw [div_eq_iff_mul_eq, eq_comm, mul_comm]
-        exact h₁t y h₁y
-        norm_num
-        rw [sub_eq_zero]
-        tauto
-    · constructor
-      · assumption
-      · assumption
-
-  -- Describe g near points z₁ different from z₀
-  have g_near_z₁ {z₁ : ℂ} : z₁ ≠ z₀ → ∀ᶠ (z : ℂ) in nhds z₁, g z = f z / (z - z₀) ^ n := by
-    intro hz₁
-    rw [eventually_nhds_iff]
-    use {z₀}ᶜ
-    constructor
-    · intro y hy
-      simp at hy
-      simp [g, hy]
-    · exact ⟨isOpen_compl_singleton, hz₁⟩
-
-  -- Use g and show that it has all required properties
-  use g
-  constructor
-  · -- AnalyticOn ℂ g U
-    intro z h₁z
-    by_cases h₂z : z = z₀
-    · rw [h₂z]
-      apply AnalyticAt.congr h₁gloc
-      exact Filter.EventuallyEq.symm g_near_z₀
-    · simp_rw [eq_comm] at g_near_z₁
-      apply AnalyticAt.congr _ (g_near_z₁ h₂z)
-      apply AnalyticAt.div
-      exact hf z h₁z
-      apply AnalyticAt.pow
-      apply AnalyticAt.sub
-      apply analyticAt_id
-      apply analyticAt_const
-      simp
-      rw [sub_eq_zero]
-      tauto
-  · constructor
-    · simp [g]; tauto
-    · intro z
-      by_cases h₂z : z = z₀
-      · rw [h₂z, g_near_z₀.self_of_nhds]
-        exact h₃gloc.self_of_nhds
-      · rw [(g_near_z₁ h₂z).self_of_nhds]
-        simp [h₂z]
-        rw [div_eq_mul_inv, mul_comm, mul_assoc, inv_mul_cancel]
-        simp; norm_num
-        rw [sub_eq_zero]
-        tauto
 
 
 noncomputable def zeroDivisorDegree