nevanlinna/Nevanlinna/meromorphicAt.lean

import Mathlib.Analysis.Analytic.Meromorphic
import Nevanlinna.analyticAt
import Nevanlinna.divisor


open scoped Interval Topology
open Real Filter MeasureTheory intervalIntegral


theorem MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (hf : MeromorphicAt f z₀) :
  (∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = 0) ∨ ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z ≠ 0 := by

  obtain ⟨n, h⟩ := hf
  let A := h.eventually_eq_zero_or_eventually_ne_zero

  rw [eventually_nhdsWithin_iff]
  rw [eventually_nhds_iff]
  rcases A with h₁|h₂
  · rw [eventually_nhds_iff] at h₁
    obtain ⟨N, h₁N, h₂N, h₃N⟩ := h₁
    left
    use N
    constructor
    · intro y h₁y h₂y
      let A := h₁N y h₁y
      simp at A
      rcases A with h₃|h₄
      · let B := h₃.1
        simp at h₂y
        let C := sub_eq_zero.1 B
        tauto
      · assumption
    · constructor
      · exact h₂N
      · exact h₃N
  · right
    rw [eventually_nhdsWithin_iff]
    rw [eventually_nhds_iff]
    rw [eventually_nhdsWithin_iff] at h₂
    rw [eventually_nhds_iff] at h₂
    obtain ⟨N, h₁N, h₂N, h₃N⟩ := h₂
    use N
    constructor
    · intro y h₁y h₂y
      by_contra h
      let A := h₁N y h₁y h₂y
      rw [h] at A
      simp at A
    · constructor
      · exact h₂N
      · exact h₃N