From e8fa4b646d71e82ad938f5c886913df1f4cdb5ed Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 20 Aug 2024 12:54:30 +0200
Subject: [PATCH] Cleanup

---
 Nevanlinna/analyticOn_zeroSet.lean | 29 ++++++++++++++---------------
 Nevanlinna/holomorphic_zero.lean   |  1 +
 2 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/Nevanlinna/analyticOn_zeroSet.lean b/Nevanlinna/analyticOn_zeroSet.lean
index 602e060..8a9cebc 100644
--- a/Nevanlinna/analyticOn_zeroSet.lean
+++ b/Nevanlinna/analyticOn_zeroSet.lean
@@ -1,11 +1,6 @@
-import Mathlib.Analysis.Analytic.Linear
-import Init.Classical
-import Mathlib.Analysis.Analytic.Meromorphic
-import Mathlib.Topology.ContinuousOn
-import Mathlib.Analysis.Analytic.IsolatedZeros
 import Mathlib.Analysis.Analytic.Constructions
-import Nevanlinna.holomorphic
-
+import Mathlib.Analysis.Analytic.IsolatedZeros
+import Mathlib.Analysis.Complex.Basic
 
 
 theorem AnalyticOn.order_eq_nat_iff
@@ -97,7 +92,7 @@ theorem AnalyticOn.order_eq_nat_iff
   exact ⟨h₁g z₀ hz₀, ⟨h₂g, Filter.eventually_of_forall h₃g⟩⟩
 
 
-theorem AnalyticOn.order_of_mul
+theorem AnalyticAt.order_mul
   {f₁ f₂ : ℂ → ℂ}
   {z₀ : ℂ}
   (hf₁ : AnalyticAt ℂ f₁ z₀)
@@ -183,10 +178,11 @@ theorem AnalyticOn.eliminateZeros
     have h₁φ : AnalyticAt ℂ φ b₀ := by
       dsimp [φ]
       apply Finset.analyticAt_prod
-      intro b hb
+      intro b _
       apply AnalyticAt.pow
       apply AnalyticAt.sub
-      apply analyticAt_id
+      apply analyticAt_id ℂ
+      exact analyticAt_const
 
     have h₂φ : h₁φ.order = (0 : ℕ) := by
       rw [AnalyticAt.order_eq_nat_iff h₁φ 0]
@@ -198,13 +194,16 @@ theorem AnalyticOn.eliminateZeros
           push_neg
           rw [Finset.prod_ne_zero_iff]
           intro a ha
-          have AA : b₀.1 - a ≠ 0 := by
-            sorry
-          simp [AA]
-
+          simp
+          have : ¬ (b₀.1 - a.1 = 0) := by
+            by_contra C
+            rw [sub_eq_zero] at C
+            rw [SetCoe.ext C] at hb
+            tauto
+          tauto
         · simp
 
-    rw [AnalyticOn.order_of_mul h₁φ (h₁g₀ b₀ b₀.2)]
+    rw [AnalyticAt.order_mul h₁φ (h₁g₀ b₀ b₀.2)]
 
     rw [h₂φ]
     simp
diff --git a/Nevanlinna/holomorphic_zero.lean b/Nevanlinna/holomorphic_zero.lean
index 68ab121..2e5fbf7 100644
--- a/Nevanlinna/holomorphic_zero.lean
+++ b/Nevanlinna/holomorphic_zero.lean
@@ -3,6 +3,7 @@ import Mathlib.Analysis.Analytic.Meromorphic
 import Mathlib.Topology.ContinuousOn
 import Mathlib.Analysis.Analytic.IsolatedZeros
 import Nevanlinna.holomorphic
+import Nevanlinna.analyticOn_zeroSet
 
 
 noncomputable def zeroDivisor