Update

2024-10-24 12:50:08 +02:00
parent e7ca812ad8
commit 570a58aab7
2 changed files with 16 additions and 10 deletions
--- a/Nevanlinna/stronglyMeromorphic.lean
+++ b/Nevanlinna/stronglyMeromorphic.lean
@@ -172,11 +172,17 @@ theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
          · let h₄f := (hf.order_eq_int_iff 0).1 h₃f
            let G := Classical.choose h₄f
            simp [h₃f]
-            let hG := Classical.choose_spec h₄f
-            simp at hG
-
-            sorry
-          · simp [h₃f]
+            obtain ⟨h₁G, h₂G, h₃G⟩  := Classical.choose_spec h₄f
+            simp at h₃G
+            have hn : n = 0 := by
+              sorry
+            rw [hn]
+            simp
+            have : g =ᶠ[𝓝 z₀] G := by
+              sorry
+            rw [Filter.EventuallyEq.eq_of_nhds this]
+          · have : hf.order ≠ 0 := h₃f
+            simp [this]
            left
            apply zero_zpow n
            dsimp [n]