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