Complex.Hadamard.weierstrassFactor_div_ne_zero_on_ball_punctured

lemma weierstrassFactor_div_ne_zero_on_ball_punctured    (m : ℕ) {f : ℂ → ℂ} {z₀ : ℂ} {ε : ℝ}    (hball : Metric.ball z₀ ε ∩ (MeromorphicOn.divisor f (Set.univ : Set ℂ)).support = {z₀}) :    ∀ z ∈ Metric.ball z₀ ε, z ≠ z₀ →      ∀ p : divisorZeroIndex₀ f (Set.univ : Set ℂ),        weierstrassFactor m (z / divisorZeroIndex₀_val p) ≠ 0 := by  intro z hz hz0 p  by_cases hp : divisorZeroIndex₀_val p = z₀  · have hz1 : z / divisorZeroIndex₀_val p ≠ (1 : ℂ) := by      have ha : divisorZeroIndex₀_val p ≠ 0 := divisorZeroIndex₀_val_ne_zero p      simpa [hp] using (mt (div_eq_one_iff_eq ha).1 (by simpa [hp] using hz0))    exact _root_.Complex.weierstrassFactor_ne_zero_of_ne_one (m := m) hz1  · exact weierstrassFactor_div_ne_zero_on_ball_of_val_ne (m := m) (f := f) (z₀ := z₀)        (ε := ε) hball p (by simpa using hp) z hz