From 1c844b9978eaaee3bb886282ad1b78dcf0c4cfbe Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 7 Nov 2024 16:10:37 +0100
Subject: [PATCH] Update meromorphicOn_decompose.lean

---
 Nevanlinna/meromorphicOn_decompose.lean | 27 +++++++++++++++++++++++--
 1 file changed, 25 insertions(+), 2 deletions(-)

diff --git a/Nevanlinna/meromorphicOn_decompose.lean b/Nevanlinna/meromorphicOn_decompose.lean
index ceb2ba4..a13c472 100644
--- a/Nevanlinna/meromorphicOn_decompose.lean
+++ b/Nevanlinna/meromorphicOn_decompose.lean
@@ -19,5 +19,28 @@ theorem MeromorphicOn.decompose
   (h₂f : ∃ z₀ ∈ U, f z₀ ≠ 0) :
   ∃ g : ℂ → ℂ, (AnalyticOnNhd ℂ g U)
     ∧ (∀ z ∈ U, g z ≠ 0)
-    ∧ (Set.EqOn h₁f.makeStronglyMeromorphicOn (fun z ↦ ∏ᶠ p ∈ h₁f.divisor.support, (z-p) ) U) := by
-  sorry
+    ∧ (Set.EqOn h₁f.makeStronglyMeromorphicOn (fun z ↦ ∏ᶠ p, (z - p) ^ (h₁f.divisor p) * g z ) U) := by
+
+  let g₁ : ℂ → ℂ := f * (fun z ↦ ∏ᶠ p, (z - p) ^ (h₁f.divisor p))
+  have h₁g₁ : MeromorphicOn g₁ U := by sorry
+  let g := h₁g₁.makeStronglyMeromorphicOn
+  have h₁g : MeromorphicOn g U := by sorry
+  have h₂g : ∀ z : U, (h₁g z.1 z.2).order = 0 := by sorry
+  have h₃g : StronglyMeromorphicOn g U := by sorry
+  have h₄g : AnalyticOnNhd ℂ g U := by
+    intro z hz
+    apply StronglyMeromorphicAt.analytic (h₃g z hz)
+    rw [h₂g ⟨z, hz⟩]
+  use g
+  constructor
+  · exact h₄g
+  · constructor
+    · intro z hz
+      rw [← (h₄g z hz).order_eq_zero_iff]
+
+      let A := (h₄g z hz).meromorphicAt_order
+      let B := h₂g ⟨z, hz⟩
+      sorry
+    · intro z hz
+
+      sorry