From a6defe8296613dae88226fae2923d699c6627747 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Fri, 25 Oct 2024 14:14:07 +0200 Subject: [PATCH] Update stronglyMeromorphicAt.lean --- Nevanlinna/stronglyMeromorphicAt.lean | 37 ++++++++++++++++++++++++--- 1 file changed, 33 insertions(+), 4 deletions(-) diff --git a/Nevanlinna/stronglyMeromorphicAt.lean b/Nevanlinna/stronglyMeromorphicAt.lean index 9e5eadb..7a4d04f 100644 --- a/Nevanlinna/stronglyMeromorphicAt.lean +++ b/Nevanlinna/stronglyMeromorphicAt.lean @@ -233,12 +233,41 @@ theorem makeStronglyMeromorphic_id simp [B] exact Filter.EventuallyEq.eq_of_nhds h₁f · obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h₁f - + rw [Filter.EventuallyEq.eq_of_nhds h₃g] + have : h₀f.meromorphicAt.order = n := by + rw [MeromorphicAt.order_eq_int_iff (StronglyMeromorphicAt.meromorphicAt h₀f) n] + use g + constructor + · assumption + · constructor + · assumption + · exact eventually_nhdsWithin_of_eventually_nhds h₃g by_cases h₃f : h₀f.meromorphicAt.order = 0 · simp [h₃f] - sorry + have hn : n = (0 : ℤ) := by + rw [h₃f] at this + exact WithTop.coe_eq_zero.mp (id (Eq.symm this)) + simp_rw [hn] + simp + let t₀ : h₀f.meromorphicAt.order = (0 : ℤ) := by + exact h₃f + let A := (h₀f.meromorphicAt.order_eq_int_iff 0).1 t₀ + have : g =ᶠ[𝓝 z₀] (Classical.choose A) := by + obtain ⟨h₀, h₁, h₂⟩ := Classical.choose_spec A + apply localIdentity h₁g h₀ + rw [hn] at h₃g + simp at h₃g + simp at h₂ + have h₄g : f =ᶠ[𝓝[≠] z₀] g := by + apply Filter.EventuallyEq.filter_mono h₃g + exact nhdsWithin_le_nhds + exact Filter.EventuallyEq.trans (Filter.EventuallyEq.symm h₄g) h₂ + exact Filter.EventuallyEq.eq_of_nhds this · simp [h₃f] - - sorry + left + apply zero_zpow n + by_contra hn + rw [hn] at this + tauto · exact m₁ (StronglyMeromorphicAt.meromorphicAt hf) z hz