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


/- Strongly MeromorphicAt -/
def StronglyMeromorphicAt
  (f : ℂ → ℂ)
  (z₀ : ℂ) :=
  (∀ᶠ (z : ℂ) in nhds z₀, f z = 0) ∨ (∃ (n : ℤ), ∃ g : ℂ → ℂ, (AnalyticAt ℂ g z₀) ∧ (g z₀ ≠ 0) ∧ (∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ n • g z))


/- Strongly MeromorphicAt is Meromorphic -/
theorem StronglyMeromorphicAt.meromorphicAt
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (hf : StronglyMeromorphicAt f z₀) :
  MeromorphicAt f z₀ := by
  rcases hf with h|h
  · use 0; simp
    rw [analyticAt_congr h]
    exact analyticAt_const
  · obtain ⟨n, g, h₁g, _, h₃g⟩ := h
    rw [meromorphicAt_congr' h₃g]
    apply MeromorphicAt.smul
    apply MeromorphicAt.zpow
    apply MeromorphicAt.sub
    apply MeromorphicAt.id
    apply MeromorphicAt.const
    exact AnalyticAt.meromorphicAt h₁g


/- Strongly MeromorphicAt of non-negative order is analytic -/
theorem StronglyMeromorphicAt.analytic
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (h₁f : StronglyMeromorphicAt f z₀)
  (h₂f : 0 ≤ h₁f.meromorphicAt.order):
  AnalyticAt ℂ f z₀ := by
  let h₁f' := h₁f
  rcases h₁f' with h|h
  · rw [analyticAt_congr h]
    exact analyticAt_const
  · obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h
    rw [analyticAt_congr h₃g]

    have : h₁f.meromorphicAt.order = n := by
      rw [MeromorphicAt.order_eq_int_iff]
      use g
      constructor
      · exact h₁g
      · constructor
        · exact h₂g
        · exact Filter.EventuallyEq.filter_mono h₃g nhdsWithin_le_nhds
    rw [this] at h₂f
    apply AnalyticAt.smul
    nth_rw 1 [← Int.toNat_of_nonneg (WithTop.coe_nonneg.mp h₂f)]
    apply AnalyticAt.pow
    apply AnalyticAt.sub
    apply analyticAt_id -- Warning: want apply AnalyticAt.id
    apply analyticAt_const -- Warning: want AnalyticAt.const
    exact h₁g


/- Analytic functions are strongly meromorphic -/
theorem AnalyticAt.stronglyMeromorphicAt
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (h₁f : AnalyticAt ℂ f z₀) :
  StronglyMeromorphicAt f z₀ := by
  by_cases h₂f : h₁f.order = ⊤
  · rw [AnalyticAt.order_eq_top_iff] at h₂f
    tauto
  · have : h₁f.order ≠ ⊤ := h₂f
    rw [← ENat.coe_toNat_eq_self] at this
    rw [eq_comm, AnalyticAt.order_eq_nat_iff] at this
    right
    use h₁f.order.toNat
    obtain ⟨g, h₁g, h₂g, h₃g⟩ := this
    use g
    tauto


/- Make strongly MeromorphicAt -/
noncomputable def MeromorphicAt.makeStronglyMeromorphicAt
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (hf : MeromorphicAt f z₀) :
  ℂ → ℂ := by
  intro z
  by_cases z = z₀
  · by_cases h₁f : hf.order = (0 : ℤ)
    · rw [hf.order_eq_int_iff] at h₁f
      exact (Classical.choose h₁f) z₀
    · exact 0
  · exact f z

lemma m₁
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (hf : MeromorphicAt f z₀) :
  ∀ z ≠ z₀, f z = hf.makeStronglyMeromorphicAt z := by
  intro z hz
  unfold MeromorphicAt.makeStronglyMeromorphicAt
  simp [hz]

lemma m₂
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (hf : MeromorphicAt f z₀) :
  ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = hf.makeStronglyMeromorphicAt z := by
  apply eventually_nhdsWithin_of_forall
  exact fun x a => m₁ hf x a


open Topology

lemma Mnhds
  {f g : ℂ → ℂ}
  {z₀ : ℂ}
  (h₁ : ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = g z)
  (h₂ : f z₀ = g z₀) :
  ∀ᶠ (z : ℂ) in nhds z₀, f z = g z := by
  rw [eventually_nhds_iff]
  rw [eventually_nhdsWithin_iff] at h₁
  sorry

theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (hf : MeromorphicAt f z₀) :
  StronglyMeromorphicAt hf.makeStronglyMeromorphicAt z₀ := by

  by_cases h₂f : hf.order = ⊤
  · rw [MeromorphicAt.order_eq_top_iff] at h₂f
    let Z : ℂ → ℂ := fun z ↦ 0
    have : hf.makeStronglyMeromorphicAt =ᶠ[𝓝 z₀] 0 := by
      --unfold Filter.EventuallyEq
      apply Mnhds
      · apply eventually_nhdsWithin_of_forall
        intro x hx

        sorry


      sorry



    apply AnalyticAt.stronglyMeromorphicAt
    rw [analyticAt_congr this]
    apply analyticAt_const



  by_cases h₂f : hf.order = 0
  · apply AnalyticAt.stronglyMeromorphicAt

    let A := h₂f
    rw [(by rfl : (0 : WithTop ℤ) = (0 : ℤ)), hf.order_eq_int_iff] at A
    simp at A
    have : hf.makeStronglyMeromorphicAt = Classical.choose A := by
      simp [MeromorphicAt.makeStronglyMeromorphicAt, h₂f]
    let B := Classical.choose_spec A

    rw [this]
    tauto
  · by_cases h₃f : hf.order = ⊤
    · rw [MeromorphicAt.order_eq_top_iff] at h₃f
      left

      sorry
    · sorry



theorem makeStronglyMeromorphic_eventuallyEq
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  (hf : MeromorphicAt f z₀) :
  ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = hf.makeStronglyMeromorphicAt z := by
  sorry