Working…

Nevanlinna/meromorphicAt.lean

@@ -145,3 +145,6 @@ theorem MeromorphicAt.order_mul
           · constructor
             · exact IsOpen.inter h₂t₁ h₂t₂
             · exact Set.mem_inter h₃t₁ h₃t₂
+
+
+-- might want theorem MeromorphicAt.order_zpow

Nevanlinna/stronglyMeromorphicOn_eliminate.lean

@@ -30,9 +30,17 @@ theorem MeromorphicOn.decompose₁
     apply AnalyticOnNhd.sub
     exact analyticOnNhd_id
     exact analyticOnNhd_const
-  have h₂h₁ : (h₁h₁ z₀ hz₀).order = -h₁f.divisor z₀ := by
-
-    sorry
+  let n : ℤ := (-h₁f.divisor z₀)
+  have h₂h₁ : (h₁h₁ z₀ hz₀).order = n := by
+    simp_rw [(h₁h₁ z₀ hz₀).order_eq_int_iff]
+    use 1
+    constructor
+    · apply analyticAt_const
+    · constructor
+      · simp
+      · apply eventually_nhdsWithin_of_forall
+        intro z hz
+        simp
 
   let g₁ := f * h₁
   have h₁g₁ : MeromorphicOn g₁ U := by