diff --git a/Nevanlinna/analyticOn_zeroSet.lean b/Nevanlinna/analyticOn_zeroSet.lean
index 49e0bb1..63fcf34 100644
--- a/Nevanlinna/analyticOn_zeroSet.lean
+++ b/Nevanlinna/analyticOn_zeroSet.lean
@@ -359,13 +359,10 @@ theorem AnalyticOnCompact.eliminateZeros
 
   let A₁ := ι⁻¹' (U ∩ f⁻¹' {0})
 
-  have t₁ : (U ∩ f⁻¹' {0}).Finite := by
-    sorry
-
   have : A₁.Finite := by
     apply Set.Finite.preimage
     exact Set.injOn_subtype_val
-    exact t₁
+    exact finiteZeros h₁U h₂U h₁f h₂f
   let A := this.toFinset
 
   let n : ℂ → ℕ := by
@@ -375,7 +372,12 @@ theorem AnalyticOnCompact.eliminateZeros
     · exact 0
 
   have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
-    sorry
+    intro a _
+    dsimp [n]
+    simp
+    rw [eq_comm]
+    apply XX h₁U
+    exact h₂f
 
   obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
   use g