Update stronglyMeromorphic.lean

Nevanlinna/stronglyMeromorphic.lean

@@ -134,6 +134,28 @@ lemma Mnhds
   · exact h₂t
 
 
+theorem localIdentity
+  {f g : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : AnalyticAt ℂ f z₀)
+  (hg : AnalyticAt ℂ g z₀) :
+  f =ᶠ[𝓝[≠] z₀] g → f =ᶠ[𝓝 z₀] g := by
+  intro h
+  let Δ := f - g
+  have : AnalyticAt ℂ Δ z₀ := AnalyticAt.sub hf hg
+  have t₁ : Δ =ᶠ[𝓝[≠] z₀] 0 := by
+    exact Filter.eventuallyEq_iff_sub.mp h
+
+  have : Δ =ᶠ[𝓝 z₀] 0 := by
+    rcases (AnalyticAt.eventually_eq_zero_or_eventually_ne_zero this) with h | h
+    · exact h
+    · have := Filter.EventuallyEq.eventually t₁
+      let A := Filter.eventually_and.2 ⟨this, h⟩
+      let _ := Filter.Eventually.exists A
+      tauto
+  exact Filter.eventuallyEq_iff_sub.mpr this
+
+
 theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
   {f : ℂ → ℂ}
   {z₀ : ℂ}
@@ -170,13 +192,19 @@ theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
           simp
           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]
+            obtain ⟨h₁G, h₂G, h₃G⟩  := Classical.choose_spec h₄f
+            simp at h₃G
+            have hn : n = 0 := Eq.symm ((fun {α} {a} {b} h => (WithTop.eq_untop_iff h).mpr) h₂f (id (Eq.symm h₃f)))
+            rw [hn]
+            rw [hn] at h₃g; simp at h₃g
+            simp
+            have : g =ᶠ[𝓝 z₀] (Classical.choose h₄f) := by
+              apply localIdentity h₁g h₁G
+              exact Filter.EventuallyEq.trans (Filter.EventuallyEq.symm h₃g) h₃G
+            rw [Filter.EventuallyEq.eq_of_nhds this]
+          · have : hf.order ≠ 0 := h₃f
+            simp [this]
             left
             apply zero_zpow n
             dsimp [n]

lake-manifest.json

@@ -5,12 +5,12 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7c5548eeeb1748da5c2872dbd866d3acbaea4b3f",
+   "rev": "dc72dcdb8e97b3c56bd70f06f043ed2dee3258e6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b20a88676fd00affb90cbc9f1ff004ae588103b3",
+   "rev": "9ac12945862fa39eab7795c2f79bb9aa0c8e332c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9b4088ccf0f44ddd7b1132bb1348aef8cf481e12",
+   "rev": "0ea83a676d288220ba227808568cbb80fe43ace0",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "818db408b33f801f4094614250e6b3cfb9e065c8",
+   "rev": "893b3a846645d48ac45143ec02149cc551acd99d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,