import Mathlib.Analysis.Analytic.IsolatedZeros
import Nevanlinna.holomorphic


noncomputable def zeroDivisor
  (f : ℂ → ℂ) :
  ℂ → ℕ := by
  intro z
  if hf : AnalyticAt ℂ f z then
    exact hf.order.toNat
  else
    exact 0


theorem discreteZeros
  {f : ℂ → ℂ} :
  DiscreteTopology (Function.support (zeroDivisor f)) := by
  sorry


theorem zeroDivisor_finiteOnCompact
  {f : ℂ → ℂ}
  {s : Set ℂ}
  (hs : IsCompact s) :
  Set.Finite (s ∩ Function.support (zeroDivisor f)) := by
  sorry


theorem eliminatingZeros
  {f : ℂ → ℂ}
  {z₀ : ℂ}
  {R : ℝ}
  (h₁f : ∀ z ∈ Metric.ball z₀ R, HolomorphicAt f z)
  (h₂f : ∃ z ∈ Metric.ball z₀ R, f z ≠ 0) :
  ∃ F : ℂ → ℂ, ∀ z ∈ Metric.ball z₀ R, (HolomorphicAt F z) ∧ (f z = (F z) * ∏ᶠ a ∈ Metric.ball z₀ R, (z - a) ^ (zeroDivisor f a) ) := by
  sorry