diff --git a/Nevanlinna/stronglyMeromorphic.lean b/Nevanlinna/stronglyMeromorphic.lean
index 3223e64..09696ea 100644
--- a/Nevanlinna/stronglyMeromorphic.lean
+++ b/Nevanlinna/stronglyMeromorphic.lean
@@ -168,8 +168,12 @@ theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
           exact h₃g
         · unfold MeromorphicAt.makeStronglyMeromorphicAt
           simp
-          by_cases h₃f : hf.order = 0
-          · simp [h₃f]
+          by_cases h₃f : hf.order = (0 : ℤ)
+          · 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]