From 092bfd85a390de4258486577776d646b9769d07f Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 26 Nov 2024 11:20:02 +0100
Subject: [PATCH] Update stronglyMeromorphicOn_ratlPolynomial.lean

---
 .../stronglyMeromorphicOn_ratlPolynomial.lean | 63 ++++++++++---------
 1 file changed, 32 insertions(+), 31 deletions(-)

diff --git a/Nevanlinna/stronglyMeromorphicOn_ratlPolynomial.lean b/Nevanlinna/stronglyMeromorphicOn_ratlPolynomial.lean
index 3ecd628..695131d 100644
--- a/Nevanlinna/stronglyMeromorphicOn_ratlPolynomial.lean
+++ b/Nevanlinna/stronglyMeromorphicOn_ratlPolynomial.lean
@@ -82,8 +82,7 @@ theorem stronglyMeromorphicOn_divisor_ratlPolynomial₁
       by_contra hCon
       let A := congrFun hCon u
       simp at A
-      have t₁ : (0 : ℂ) ^ d u ≠ 0 := by
-        exact ne_zero_of_eq_one A
+      have t₁ : (0 : ℂ) ^ d u ≠ 0 := ne_zero_of_eq_one A
       rw [zpow_ne_zero_iff h] at t₁
       tauto
 
@@ -104,42 +103,44 @@ theorem stronglyMeromorphicOn_divisor_ratlPolynomial₁
       tauto
     · apply Filter.Eventually.of_forall
       intro x
+      have t₀ : (Function.mulSupport fun u z => (z - u) ^ d u).Finite := by
+        rwa [h₂d]
+      rw [finprod_eq_prod _ t₀]
+      have t₁ : h₁d.toFinset = t₀.toFinset := by
+        simp
+        rwa [eq_comm]
+      rw [t₁]
       simp
+      rw [eq_comm]
+      have : z ∉ h₁d.toFinset.erase z := Finset.not_mem_erase z h₁d.toFinset
+      by_cases hz : z ∈ h₁d.toFinset
+      · rw [t₁] at hz
+        conv =>
+          right
+          rw [← Finset.mul_prod_erase t₀.toFinset _ hz]
+      · have : t₀.toFinset = t₀.toFinset.erase z := by
+          rw [eq_comm]
+          apply Finset.erase_eq_of_not_mem
+          rwa [t₁] at hz
+        rw [this]
 
-      rw [← Finset.mul_prod_erase]
-      sorry
-
-  by_cases hz : z ∈ d.support
-  · sorry
-  · use (∏ᶠ u, fun z ↦ (z - u) ^ d u)
-  constructor
-  ·
-    apply?
-
-  simp [hz]
-
-    sorry
-  · rw [Function.nmem_support.mp fun a => hz (h₂d a)]
-    rw [MeromorphicOn.divisor]
-    simp [hz]
-
+        have : (x - z) ^ d z = 1 := by
+          simp at hz
+          rw [hz]
+          simp
+        rw [this]
+        simp
 
 
 theorem stronglyMeromorphicOn_divisor_ratlPolynomial
-  {U : Set ℂ}
   (d : ℂ → ℤ)
-  (h₁d : Set.Finite d.support)
-  (h₂d : d.support ⊆ U) :
-  (stronglyMeromorphicOn_ratlPolynomial₃ d (U := U)).meromorphicOn.divisor = d := by
+  (h₁d : Set.Finite d.support) :
+  (stronglyMeromorphicOn_ratlPolynomial₃ d).meromorphicOn.divisor = d := by
   funext z
-  by_cases hz : z ∈ U
-  · rw [MeromorphicOn.divisor]
-    simp [hz]
-
-    sorry
-  · rw [Function.nmem_support.mp fun a => hz (h₂d a)]
-    rw [MeromorphicOn.divisor]
-    simp [hz]
+  rw [MeromorphicOn.divisor]
+  simp
+  rw [stronglyMeromorphicOn_divisor_ratlPolynomial₁ d h₁d]
+  simp
 
 
 theorem makeStronglyMeromorphicOn_changeDiscrete'