diff --git a/Nevanlinna/analyticOn_zeroSet.lean b/Nevanlinna/analyticOn_zeroSet.lean
index 5daff26..bc6ffa4 100644
--- a/Nevanlinna/analyticOn_zeroSet.lean
+++ b/Nevanlinna/analyticOn_zeroSet.lean
@@ -309,15 +309,7 @@ theorem AnalyticOnCompact.eliminateZeros
   (h₂f : ∃ u ∈ U, f u ≠ 0) :
   ∃ (g : ℂ → ℂ) (A : Finset U), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (h₁f a a.2).order.toNat) • g z := by
 
-  let ι : U → ℂ := Subtype.val
-
-  let A₁ := ι⁻¹' (U ∩ f⁻¹' {0})
-
-  have : A₁.Finite := by
-    apply Set.Finite.preimage
-    exact Set.injOn_subtype_val
-    exact finiteZeros h₁U h₂U h₁f h₂f
-  let A := this.toFinset
+  let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset
 
   let n : ℂ → ℕ := by
     intro z
@@ -354,14 +346,10 @@ theorem AnalyticOnCompact.eliminateZeros
       · exact h₂g ⟨z, h₁z⟩ h₂z
       · have : f z ≠ 0 := by
           by_contra C
-          have : ⟨z, h₁z⟩ ∈ ↑A₁ := by
-            dsimp [A₁, ι]
-            simp
-            exact C
           have : ⟨z, h₁z⟩ ∈ ↑A.toSet := by
             dsimp [A]
             simp
-            exact this
+            exact C
           tauto
         rw [inter z] at this
         exact right_ne_zero_of_smul this