diff --git a/Nevanlinna/analyticOn_zeroSet.lean b/Nevanlinna/analyticOn_zeroSet.lean
index 95d38d8..8295200 100644
--- a/Nevanlinna/analyticOn_zeroSet.lean
+++ b/Nevanlinna/analyticOn_zeroSet.lean
@@ -213,14 +213,14 @@ theorem discreteZeros
   (hU : IsPreconnected U)
   (h₁f : AnalyticOn ℂ f U)
   (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  DiscreteTopology ↑(U ∩ f⁻¹' {0}) := by
+  DiscreteTopology ((U.restrict 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
+  let A := XX hU h₁f h₂f z.1.2
   rw [eq_comm] at A
   rw [AnalyticAt.order_eq_nat_iff] at A
   obtain ⟨g, h₁g, h₂g, h₃g⟩ := A
@@ -265,9 +265,9 @@ theorem discreteZeros
     _ < min ε₁ ε₂ := by assumption
     _ ≤ ε₁ := by exact min_le_left ε₁ ε₂
 
-
   have F := h₂ε₂ y.1 h₂y
-  rw [y.2.2] at F
+  have : f y = 0 := by exact y.2
+  rw [this] at F
   simp at F
 
   have : g y.1 ≠ 0 := by
@@ -285,7 +285,7 @@ theorem finiteZeros
   (h₂U : IsCompact U)
   (h₁f : AnalyticOn ℂ f U)
   (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  Set.Finite ↑(U ∩ f⁻¹' {0}) := by
+  Set.Finite ((U.restrict f)⁻¹' {0}) := by
 
   have hinter : IsCompact ↑(U ∩ f⁻¹' {0}) := by
     apply IsCompact.of_isClosed_subset h₂U