From 1a14bbbdd66a3ea3faa59253367c9644c6cba005 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Thu, 14 Nov 2024 14:08:06 +0100 Subject: [PATCH] Update stronglyMeromorphicAt.lean --- Nevanlinna/stronglyMeromorphicAt.lean | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/Nevanlinna/stronglyMeromorphicAt.lean b/Nevanlinna/stronglyMeromorphicAt.lean index 7224e3c..2b644d5 100644 --- a/Nevanlinna/stronglyMeromorphicAt.lean +++ b/Nevanlinna/stronglyMeromorphicAt.lean @@ -392,14 +392,13 @@ theorem StronglyMeromorphicAt.decompose have h₁g : StronglyMeromorphicAt g z₀ := by exact StronglyMeromorphicAt_of_makeStronglyMeromorphic h₁g₁ have h₂g : h₁g.meromorphicAt.order = 0 := by - - - - sorry + rw [← h₁g₁.order_congr (m₂ h₁g₁)] + exact h₂g₁ constructor · apply analytic - · sorry + · rw [h₂g] · exact h₁g · constructor - · sorry - · sorry + · exact (order_eq_zero_iff h₁g).mp h₂g + · + sorry