Complex.Hadamard.tendstoLocallyUniformlyOn_divisorComplementPartialProduct_univ

theorem tendstoLocallyUniformlyOn_divisorComplementPartialProduct_univ    (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1))) :    TendstoLocallyUniformlyOn      (fun s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) =>        divisorComplementPartialProduct m f z₀ s)      (divisorComplementCanonicalProduct m f z₀)      Filter.atTop      (Set.univ : Set ℂ) := by  have hprod :      HasProdLocallyUniformlyOn        (fun (p : divisorZeroIndex₀ f (Set.univ : Set ℂ)) (z : ℂ) =>          divisorComplementFactor m f z₀ p z)        (divisorComplementCanonicalProduct m f z₀)        (Set.univ : Set ℂ) :=    hasProdLocallyUniformlyOn_divisorComplementCanonicalProduct_univ (m := m) (f := f)      (z₀ := z₀) h_sum  have h :      TendstoLocallyUniformlyOn        (fun (s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ))) (z : ℂ) =>          ∏ p ∈ s,            if divisorZeroIndex₀_val p = z₀ then (1 : ℂ)            else weierstrassFactor m (z / divisorZeroIndex₀_val p))        (divisorComplementCanonicalProduct m f z₀)        Filter.atTop        (Set.univ : Set ℂ) := by    simpa [HasProdLocallyUniformlyOn, divisorComplementFactor, mem_divisorZeroIndex₀_fiberFinset]      using hprod  refine h.congr (G := fun s z => divisorComplementPartialProduct m f z₀ s z) ?_  intro s z hz  simp [divisorComplementPartialProduct_def]