From e7ca812ad8cda2c840d13c14695aea6d347c78a8 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Wed, 23 Oct 2024 13:31:22 +0200 Subject: [PATCH] Update stronglyMeromorphic.lean --- Nevanlinna/stronglyMeromorphic.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) 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]