From 97293e3a606a20c7d76b54270a6ec26cf2090a3d Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 19 Aug 2024 08:30:02 +0200
Subject: [PATCH] Update holomorphic_zero.lean

---
 Nevanlinna/holomorphic_zero.lean | 27 +++++++++++++++++++++++----
 1 file changed, 23 insertions(+), 4 deletions(-)

diff --git a/Nevanlinna/holomorphic_zero.lean b/Nevanlinna/holomorphic_zero.lean
index d6021cc..50a7735 100644
--- a/Nevanlinna/holomorphic_zero.lean
+++ b/Nevanlinna/holomorphic_zero.lean
@@ -1,3 +1,4 @@
+import Mathlib.Topology.ContinuousOn
 import Mathlib.Analysis.Analytic.IsolatedZeros
 import Nevanlinna.holomorphic
 
@@ -243,10 +244,28 @@ theorem discreteZeros
 
 theorem zeroDivisor_finiteOnCompact
   {f : ℂ → ℂ}
-  {s : Set ℂ}
-  (hs : IsCompact s) :
-  Set.Finite (s ∩ Function.support (zeroDivisor f)) := by
-  sorry
+  {U : Set ℂ}
+  (hU : IsPreconnected U)
+  (h₁f : AnalyticOn ℂ f U)
+  (h₂f : ∃ z ∈ U, f z ≠ 0)
+  (h₂U : IsCompact U) :
+  Set.Finite (U ∩ Function.support (zeroDivisor f)) := by
+
+  have hinter : IsCompact (U ∩ Function.support (zeroDivisor f)) := by
+    apply IsCompact.of_isClosed_subset h₂U
+    rw [supportZeroSet]
+    apply h₁f.continuousOn.preimage_isClosed_of_isClosed
+    exact IsCompact.isClosed h₂U
+    exact isClosed_singleton
+    assumption
+    assumption
+    assumption
+    exact Set.inter_subset_left
+
+  apply hinter.finite
+  apply DiscreteTopology.of_subset (s := Function.support (zeroDivisor f))
+  exact discreteZeros (f := f)
+  exact Set.inter_subset_right
 
 
 theorem eliminatingZeros