From 2b7ab1af9d2582f19d1547be63a2f2e64453011f Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 28 Nov 2024 18:24:08 +0100
Subject: [PATCH] Working

---
 Nevanlinna/stronglyMeromorphicOn_ratlPolynomial.lean | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/Nevanlinna/stronglyMeromorphicOn_ratlPolynomial.lean b/Nevanlinna/stronglyMeromorphicOn_ratlPolynomial.lean
index 005f635..948464b 100644
--- a/Nevanlinna/stronglyMeromorphicOn_ratlPolynomial.lean
+++ b/Nevanlinna/stronglyMeromorphicOn_ratlPolynomial.lean
@@ -63,6 +63,13 @@ theorem stronglyMeromorphicOn_ratlPolynomial₃
     apply analyticOnNhd_const
 
 
+theorem stronglyMeromorphicOn_ratlPolynomial₃U
+  (d : ℂ → ℤ)
+  (U : Set ℂ) :
+  StronglyMeromorphicOn (∏ᶠ u, fun z ↦ (z - u) ^ d u) U := by
+  intro z hz
+  exact stronglyMeromorphicOn_ratlPolynomial₃ d z (trivial)
+
 
 theorem stronglyMeromorphicOn_divisor_ratlPolynomial₁
   {z : ℂ}
@@ -166,7 +173,10 @@ theorem stronglyMeromorphicOn_ratlPolynomial₃order
     have : (Function.mulSupport fun u z => (z - u) ^ d u).Infinite := by
       exact hd
     simp_rw [finprod_of_infinite_mulSupport this]
-    sorry
+    have : AnalyticAt ℂ (1 : ℂ → ℂ) z := by exact analyticAt_const
+    rw [AnalyticAt.meromorphicAt_order this]
+    rw [this.order_eq_zero_iff.2 (by simp)]
+    simp
 
 
 theorem stronglyMeromorphicOn_divisor_ratlPolynomial