Update holomorphic_zero.lean

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