Complex.Hadamard.divisorCanonicalProduct_eq_zero_of_exists

theorem divisorCanonicalProduct_eq_zero_of_exists    (m : ℕ) (f : ℂ → ℂ) (z : ℂ)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)))    (h0 : ∃ p : divisorZeroIndex₀ f (Set.univ : Set ℂ),      weierstrassFactor m (z / divisorZeroIndex₀_val p) = 0) :    divisorCanonicalProduct m f (Set.univ : Set ℂ) z = 0 := by  have hloc :      HasProdLocallyUniformlyOn        (fun (p : divisorZeroIndex₀ f (Set.univ : Set ℂ)) (w : ℂ) =>          weierstrassFactor m (w / divisorZeroIndex₀_val p))        (divisorCanonicalProduct m f (Set.univ : Set ℂ))        (Set.univ : Set ℂ) :=    hasProdLocallyUniformlyOn_divisorCanonicalProduct_univ (m := m) (f := f) h_sum  have hprod :      HasProd (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>          weierstrassFactor m (z / divisorZeroIndex₀_val p))        (divisorCanonicalProduct m f (Set.univ : Set ℂ) z) :=    hloc.hasProd (by simp : z ∈ (Set.univ : Set ℂ))  have hzero :      HasProd (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>          weierstrassFactor m (z / divisorZeroIndex₀_val p))        0 := by    refine hasProd_zero_of_exists_eq_zero (L := (SummationFilter.unconditional      (divisorZeroIndex₀ f (Set.univ : Set ℂ)))) ?_    rcases h0 with ⟨p, hp⟩    exact ⟨p, hp⟩  exact (hprod.unique hzero)