From f9f177e7b9da22b935cb5b56afae7cc50980f495 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 16 Aug 2024 20:24:24 +0200
Subject: [PATCH] Update holomorphic_zero.lean

---
 Nevanlinna/holomorphic_zero.lean | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/Nevanlinna/holomorphic_zero.lean b/Nevanlinna/holomorphic_zero.lean
index 0b4c41d..3e27529 100644
--- a/Nevanlinna/holomorphic_zero.lean
+++ b/Nevanlinna/holomorphic_zero.lean
@@ -115,6 +115,25 @@ theorem zeroDivisor_support_iff
     assumption
 
 
+example
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hU : IsPreconnected U)
+  (h₁f : AnalyticOn ℂ f U)
+  (h₂f : ∃ z ∈ U, f z ≠ 0) :
+  ∀ (hz : z ∈ U), (h₁f z hz).order ≠ ⊤ := by
+  by_contra H
+  push_neg at H
+  obtain ⟨z', hz'⟩ := H
+
+  rw [AnalyticAt.order_eq_top_iff] at hz'
+  let A := AnalyticOn.eqOn_zero_of_preconnected_of_frequently_eq_zero h₁f hU z'
+  rw [AnalyticAt.frequently_eq_iff_eventually_eq] at A
+  let B := A hz'
+
+  sorry
+
+
 theorem discreteZeros
   {f : ℂ → ℂ} :
   DiscreteTopology (Function.support (zeroDivisor f)) := by