working

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

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⟩]