From f43674dedce5d8a7c257b578741c1ef8e80077ba Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 14 Nov 2024 06:49:15 +0100
Subject: [PATCH] working

---
 Nevanlinna/analyticAt.lean              | 11 +++++++++++
 Nevanlinna/meromorphicOn_decompose.lean |  3 ++-
 2 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/Nevanlinna/analyticAt.lean b/Nevanlinna/analyticAt.lean
index 22831aa..2b4ffc3 100644
--- a/Nevanlinna/analyticAt.lean
+++ b/Nevanlinna/analyticAt.lean
@@ -280,3 +280,14 @@ theorem analyticAt_finprod
     exact Finset.analyticAt_prod h₁f.toFinset (fun a _ ↦ hf a)
   · rw [finprod_of_infinite_mulSupport h₁f]
     exact analyticAt_const
+
+
+theorem AnalyticAt.zpow
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  {n : ℤ}
+  (h₁f : AnalyticAt ℂ f z₀)
+  (h₂f : f z₀ ≠ 0) :
+  AnalyticAt ℂ (fun x ↦ (f x) ^ n) z₀ := by
+
+  sorry
diff --git a/Nevanlinna/meromorphicOn_decompose.lean b/Nevanlinna/meromorphicOn_decompose.lean
index b7a85d1..88666cf 100644
--- a/Nevanlinna/meromorphicOn_decompose.lean
+++ b/Nevanlinna/meromorphicOn_decompose.lean
@@ -68,12 +68,13 @@ theorem MeromorphicOn.decompose
       · exact StronglyMeromorphicOn_of_makeStronglyMeromorphic h₁f z hz
       · right
         use h₁f.divisor z
-        use (∏ᶠ p ≠ z, (fun x ↦ (x - p) ^ h₁f.divisor p)) * g
+        use (∏ᶠ p : ({z}ᶜ : Set ℂ), (fun x ↦ (x - p.1) ^ h₁f.divisor p.1)) * g
         constructor
         · apply AnalyticAt.mul₁
           · apply analyticAt_finprod
             intro w
 
+
             sorry
           · apply (h₃g z hz).analytic
             rw [h₂g ⟨z, hz⟩]