Complex.Hadamard.exists_ball_eq_divisorCanonicalProduct_div_pow_eq

theorem exists_ball_eq_divisorCanonicalProduct_div_pow_eq    (m : ℕ) (f : ℂ → ℂ)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)))    (z₀ : ℂ) :    ∃ ε > 0, ∃ u : ℂ → ℂ, AnalyticAt ℂ u z₀ ∧      u z₀ ≠ 0 ∧        ∀ z : ℂ, z ∈ Metric.ball z₀ ε → z ≠ z₀ →          (divisorCanonicalProduct m f (Set.univ : Set ℂ) z) /              (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card =            (divisorComplementCanonicalProduct m f z₀ z) * u z := by  let fiber : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) :=    divisorZeroIndex₀_fiberFinset (f := f) z₀  have hfib : ∃ u : ℂ → ℂ, AnalyticAt ℂ u z₀ ∧ u z₀ ≠ 0 ∧          (fun z : ℂ => divisorPartialProduct m f fiber z) =ᶠ[𝓝 z₀]            fun z : ℂ => (z - z₀) ^ fiber.card • u z := by    simpa [fiber, divisorPartialProduct] using      (exists_analyticAt_eq_pow_smul_of_partialProduct_contains_fiber (m := m) (f := f) (z₀ := z₀)        (s := fiber) (by rfl : fiber ⊆ fiber))  rcases hfib with ⟨u, huA, hu0, huEq⟩  have hmem : {z : ℂ | divisorPartialProduct m f fiber z =      (z - z₀) ^ fiber.card • u z} ∈ 𝓝 z₀ := huEq  rcases Metric.mem_nhds_iff.1 hmem with ⟨ε, hε, hball⟩  refine ⟨ε, hε, u, huA, hu0, ?_⟩  have hq :      TendstoLocallyUniformlyOn (fun s z => (divisorPartialProduct m f s z) / (z - z₀) ^ fiber.card)        (fun z => (divisorCanonicalProduct m f (Set.univ : Set ℂ) z) / (z - z₀) ^ fiber.card)        (Filter.atTop : Filter (Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ))))        ((Set.univ : Set ℂ) \ {z₀}) :=    tendstoLocallyUniformlyOn_divisorPartialProduct_div_pow_sub      (m := m) (f := f) (h_sum := h_sum) (z₀ := z₀) (k := fiber.card)  have hcomp :      TendstoLocallyUniformlyOn        (fun s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) =>          divisorComplementPartialProduct m f z₀ s)        (divisorComplementCanonicalProduct m f z₀)        Filter.atTop        (Set.univ : Set ℂ) :=    tendstoLocallyUniformlyOn_divisorComplementPartialProduct_univ (m := m) (f := f)    (z₀ := z₀) h_sum  intro z hz hzne  have hz' : z ∈ ((Set.univ : Set ℂ) \ {z₀}) := by    refine ⟨by simp, ?_⟩    simpa [Set.mem_singleton_iff] using hzne  have hF : Tendsto (fun s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) =>          (divisorPartialProduct m f s z) / (z - z₀) ^ fiber.card) (Filter.atTop : Filter _)        (𝓝 ((divisorCanonicalProduct m f (Set.univ : Set ℂ) z) / (z - z₀) ^ fiber.card)) :=    hq.tendsto_at hz'  have hG0 : Tendsto  (fun s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) =>          divisorComplementPartialProduct m f z₀ s z) (Filter.atTop : Filter _)        (𝓝 (divisorComplementCanonicalProduct m f z₀ z)) :=    hcomp.tendsto_at (by simp : z ∈ (Set.univ : Set ℂ))  have hG : Tendsto (fun s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) =>          (divisorComplementPartialProduct m f z₀ s z) * u z) (Filter.atTop : Filter _)        (𝓝 ((divisorComplementCanonicalProduct m f z₀ z) * u z)) :=    (hG0.mul tendsto_const_nhds)  have hsub : ∀ᶠ s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) in (Filter.atTop : Filter _),      fiber ⊆ s := eventually_atTop_subset_fiberFinset (f := f) z₀  have heq_eventually :      ∀ᶠ s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) in (Filter.atTop : Filter _),        (divisorPartialProduct m f s z) / (z - z₀) ^ fiber.card          = (divisorComplementPartialProduct m f z₀ s z) * u z := by    filter_upwards [hsub] with s hs    have hsplit :        divisorPartialProduct m f s z =          divisorPartialProduct m f fiber z * divisorComplementPartialProduct m f z₀ s z := by      simpa [fiber] using        (divisorPartialProduct_eq_fiber_mul_complement_of_subset (m := m) (f := f) (z₀ := z₀)          (z := z) (s := s) hs)    have hfibz :        divisorPartialProduct m f fiber z = (z - z₀) ^ fiber.card • u z := by      exact hball hz    have hzpow : (z - z₀) ^ fiber.card ≠ 0 :=      pow_ne_zero _ (sub_ne_zero.mpr hzne)    set a : ℂ := (z - z₀) ^ fiber.card    have ha : a ≠ 0 := by simpa [a] using hzpow    set c : ℂ := divisorComplementPartialProduct m f z₀ s z with hc    rw [hsplit, hfibz, smul_eq_mul]    calc      ((a * u z) * c) / a          = (a * (u z * c)) / a := by simp [mul_assoc]      _ = u z * c := by            simpa [mul_assoc] using (mul_div_cancel_left₀ (u z * c) ha)      _ = c * u z := by ac_rfl      _ = (divisorComplementPartialProduct m f z₀ s z) * u z := by            simp [c]  have hG' :      Tendsto        (fun s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) =>          (divisorPartialProduct m f s z) / (z - z₀) ^ fiber.card)        (Filter.atTop : Filter _)        (𝓝 ((divisorComplementCanonicalProduct m f z₀ z) * u z)) := by    have heq' :        ∀ᶠ s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) in (Filter.atTop : Filter _),          (divisorComplementPartialProduct m f z₀ s z) * u z            = (divisorPartialProduct m f s z) / (z - z₀) ^ fiber.card := by      filter_upwards [heq_eventually] with s hs      exact hs.symm    exact (hG.congr' heq')  exact tendsto_nhds_unique hF hG'