nevanlinna/Nevanlinna/stronglyMeromorphicOn_eliminate.lean

import Mathlib.Analysis.Analytic.Meromorphic
import Nevanlinna.analyticAt
import Nevanlinna.divisor
import Nevanlinna.meromorphicAt
import Nevanlinna.meromorphicOn_divisor
import Nevanlinna.stronglyMeromorphicOn
import Nevanlinna.mathlibAddOn


open scoped Interval Topology
open Real Filter MeasureTheory intervalIntegral

lemma untop_eq_untop'
  {n : WithTop ℤ}
  (hn : n ≠ ⊤) :
  n.untop' 0 = n.untop hn := by
  rw [WithTop.untop'_eq_iff]
  simp


theorem MeromorphicOn.decompose₁
  {f : ℂ → ℂ}
  {U : Set ℂ}
  {z₀ : ℂ}
  (hz₀ : z₀ ∈ U)
  (h₁f : MeromorphicOn f U)
  (h₂f : StronglyMeromorphicAt f z₀)
  (h₃f : h₂f.meromorphicAt.order ≠ ⊤) :
  ∃ g : ℂ → ℂ, (MeromorphicOn g U)
    ∧ (AnalyticAt ℂ g z₀)
    ∧ (g z₀ ≠ 0)
    ∧ (f = g * fun z ↦ (z - z₀) ^ (h₁f.divisor z₀)) := by

  let h₁ := fun z ↦ (z - z₀) ^ (-h₁f.divisor z₀)
  have h₁h₁ : MeromorphicOn h₁ U := by
    apply MeromorphicOn.zpow
    apply AnalyticOnNhd.meromorphicOn
    apply AnalyticOnNhd.sub
    exact analyticOnNhd_id
    exact analyticOnNhd_const
  let n : ℤ := (-h₁f.divisor z₀)
  have h₂h₁ : (h₁h₁ z₀ hz₀).order = n := by
    simp_rw [(h₁h₁ z₀ hz₀).order_eq_int_iff]
    use 1
    constructor
    · apply analyticAt_const
    · constructor
      · simp
      · apply eventually_nhdsWithin_of_forall
        intro z hz
        simp

  let g₁ := f * h₁
  have h₁g₁ : MeromorphicOn g₁ U := by
    apply h₁f.mul h₁h₁
  have h₂g₁ : (h₁g₁ z₀ hz₀).order = 0 := by
    rw [(h₁f z₀ hz₀).order_mul (h₁h₁ z₀ hz₀)]
    rw [h₂h₁]
    unfold n
    rw [MeromorphicOn.divisor_def₂ h₁f hz₀ h₃f]
    conv =>
      left
      left
      rw [Eq.symm (WithTop.coe_untop (h₁f z₀ hz₀).order h₃f)]
    have
      (a b c : ℤ)
      (h : a + b = c) :
      (a : WithTop ℤ) + (b : WithTop ℤ) = (c : WithTop ℤ) := by
      rw [← h]
      simp
    rw [this ((h₁f z₀ hz₀).order.untop h₃f) (-(h₁f z₀ hz₀).order.untop h₃f) 0]
    simp
    ring

  let g := (h₁g₁ z₀ hz₀).makeStronglyMeromorphicAt
  have h₂g : StronglyMeromorphicAt g z₀ := by
    exact StronglyMeromorphicAt_of_makeStronglyMeromorphic (h₁g₁ z₀ hz₀)
  have h₁g : MeromorphicOn g U := by
    intro z hz
    by_cases h₁z : z = z₀
    · rw [h₁z]
      apply h₂g.meromorphicAt
    · apply (h₁g₁ z hz).congr
      rw [eventuallyEq_nhdsWithin_iff]
      rw [eventually_nhds_iff]
      use {z₀}ᶜ
      constructor
      · intro y h₁y h₂y
        let A := m₁ (h₁g₁ z₀ hz₀) y h₁y
        unfold g
        rw [← A]
      · constructor
        · exact isOpen_compl_singleton
        · exact h₁z
  have h₃g : (h₁g z₀ hz₀).order = 0 := by
    unfold g
    let B := m₂ (h₁g₁ z₀ hz₀)
    let A := (h₁g₁ z₀ hz₀).order_congr B
    rw [← A]
    rw [h₂g₁]
  have h₄g : AnalyticAt ℂ g z₀ := by
    apply h₂g.analytic
    rw [h₃g]

  use g
  constructor
  · exact h₁g
  · constructor
    · exact h₄g
    · constructor
      · exact (h₂g.order_eq_zero_iff).mp h₃g
      · funext z
        by_cases hz : z = z₀
        · rw [hz]
          simp
          by_cases h : h₁f.divisor z₀ = 0
          · simp [h]
            have h₂h₁ : h₁ = 1 := by
              funext w
              unfold h₁
              simp [h]
            have h₃g₁ : g₁ = f := by
              unfold g₁
              rw [h₂h₁]
              simp
            have h₄g₁ : StronglyMeromorphicAt g₁ z₀ := by
              rwa [h₃g₁]
            let A := h₄g₁.makeStronglyMeromorphic_id
            unfold g
            rw [← A, h₃g₁]
          · have : (0 : ℂ) ^ h₁f.divisor z₀ = (0 : ℂ) := by
              exact zero_zpow (h₁f.divisor z₀) h
            rw [this]
            simp
            let A := h₂f.order_eq_zero_iff.not
            simp at A
            rw [← A]
            unfold MeromorphicOn.divisor at h
            simp [hz₀] at h
            exact h.1
        · simp
          let B := m₁ (h₁g₁ z₀ hz₀) z hz
          unfold g
          rw [← B]
          unfold g₁ h₁
          simp [hz]
          rw [mul_assoc]
          rw [inv_mul_cancel₀]
          simp
          apply zpow_ne_zero
          rwa [sub_ne_zero]