Complex.Hadamard.divisorComplementPartialProduct_ne_zero_on_ball

lemma divisorComplementPartialProduct_ne_zero_on_ball    (m : ℕ) {f : ℂ → ℂ} {z₀ : ℂ} {ε : ℝ}    (hball :      Metric.ball z₀ ε ∩ (MeromorphicOn.divisor f (Set.univ : Set ℂ)).support = {z₀})    (s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ))) :    ∀ z ∈ Metric.ball z₀ ε,      divisorComplementPartialProduct m f z₀ s z ≠ 0 := by  intro z hz  have hfac :      ∀ p ∈ s, divisorComplementFactor m f z₀ p z ≠ 0 := by    intro p hp    by_cases hpF : p ∈ divisorZeroIndex₀_fiberFinset (f := f) z₀    · simp only [divisorComplementFactor_eq_one_of_mem m f z₀ p z hpF]      exact one_ne_zero    · have hne : weierstrassFactor m (z / divisorZeroIndex₀_val p) ≠ 0 :=        weierstrassFactor_div_ne_zero_on_ball_of_not_mem_fiberFinset          (m := m) (f := f) (z₀ := z₀) (ε := ε) hball p hpF z hz      rw [divisorComplementFactor_eq_weierstrassFactor_of_not_mem m f z₀ p z hpF]      exact hne  simpa [divisorComplementPartialProduct, Finset.prod_ne_zero_iff] using hfac