From 12d81cb0a944c2d8cca7cd6e267fad74a5de4f53 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 17 Sep 2024 10:43:46 +0200
Subject: [PATCH] Update divisor.lean

---
 Nevanlinna/divisor.lean | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

diff --git a/Nevanlinna/divisor.lean b/Nevanlinna/divisor.lean
index 3f86e6c..728cddd 100644
--- a/Nevanlinna/divisor.lean
+++ b/Nevanlinna/divisor.lean
@@ -23,7 +23,13 @@ noncomputable def Divisor.n
 noncomputable def Divisor.N_trunk
   (D : Divisor) : ℤ → ℝ → ℝ := fun k r ↦ ∫ (t : ℝ) in (1)..r, (D.n_trunk k t) / t
 
-
+theorem Divisor.compactSupport
+  (D : Divisor)
+  {U : Set ℂ}
+  (h₁U : IsCompact U)
+  (h₂U : Function.support D ⊆ U) :
+  Set.Finite (Function.support D) := by
+  sorry
 
 
 noncomputable def AnalyticOn.zeroDivisor
@@ -122,8 +128,12 @@ theorem AnalyticOn.support_of_zeroDivisor₂
   (hf : AnalyticOn ℂ f U) :
   Function.support hf.zeroDivisor ⊆ f⁻¹' {0} := by
 
-  simp
   intro z hz
-  dsimp [AnalyticOn.zeroDivisor]
+  dsimp [AnalyticOn.zeroDivisor] at hz
+  have t₀ := hf.support_of_zeroDivisor hz
+  simp [hf.support_of_zeroDivisor hz] at hz
+  let A := hz.1
+  let C := (hf z t₀).order_eq_zero_iff
   simp
+  rw [C] at A
   tauto