Complex.Hadamard.weierstrassFactor_div_ne_zero_on_ball_of_val_ne

lemma weierstrassFactor_div_ne_zero_on_ball_of_val_ne    (m : ℕ) {f : ℂ → ℂ} {z₀ : ℂ} {ε : ℝ}    (hball : Metric.ball z₀ ε ∩ (MeromorphicOn.divisor f (Set.univ : Set ℂ)).support = {z₀})    (p : divisorZeroIndex₀ f (Set.univ : Set ℂ)) (hp : divisorZeroIndex₀_val p ≠ z₀) :    ∀ z ∈ Metric.ball z₀ ε, weierstrassFactor m (z / divisorZeroIndex₀_val p) ≠ 0 := by  intro z hzball h0  have hz_eq : z = divisorZeroIndex₀_val p := by    have hdiv1 : z / divisorZeroIndex₀_val p = 1 := by      simpa [weierstrassFactor_eq_zero_iff (m := m)] using h0    have ha : divisorZeroIndex₀_val p ≠ 0 := divisorZeroIndex₀_val_ne_zero p    exact (div_eq_one_iff_eq ha).1 hdiv1  have hz_support : z ∈ (MeromorphicOn.divisor f (Set.univ : Set ℂ)).support := by    simp [hz_eq]  have hz0 : z = z₀ := by    have : z ∈ Metric.ball z₀ ε ∩ (MeromorphicOn.divisor f (Set.univ : Set ℂ)).support :=      ⟨hzball, hz_support⟩    simp [hball] at this    simpa using this  have : divisorZeroIndex₀_val p = z₀ := by    calc      divisorZeroIndex₀_val p = z := by simp [hz_eq]      _ = z₀ := hz0  exact hp this