From cd58c18a7803a32cbad8e6f7fbf488b9cb01699a Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 10 Sep 2024 11:21:49 +0200
Subject: [PATCH] Update analyticOn_zeroSet.lean

---
 Nevanlinna/analyticOn_zeroSet.lean | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/Nevanlinna/analyticOn_zeroSet.lean b/Nevanlinna/analyticOn_zeroSet.lean
index 8295200..5daff26 100644
--- a/Nevanlinna/analyticOn_zeroSet.lean
+++ b/Nevanlinna/analyticOn_zeroSet.lean
@@ -285,19 +285,19 @@ theorem finiteZeros
   (h₂U : IsCompact U)
   (h₁f : AnalyticOn ℂ f U)
   (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  Set.Finite ((U.restrict f)⁻¹' {0}) := by
+  Set.Finite (U.restrict 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
+  have closedness : IsClosed (U.restrict f⁻¹' {0}) := by
+    apply IsClosed.preimage
+    apply continuousOn_iff_continuous_restrict.1
+    exact h₁f.continuousOn
     exact isClosed_singleton
-    exact Set.inter_subset_left
 
-  apply hinter.finite
-  apply DiscreteTopology.of_subset (s := ↑(U ∩ f⁻¹' {0}))
+  have : CompactSpace U := by
+    exact isCompact_iff_compactSpace.mp h₂U
+
+  apply (IsClosed.isCompact closedness).finite
   exact discreteZeros h₁U h₁f h₂f
-  rfl
 
 
 theorem AnalyticOnCompact.eliminateZeros