Complex.Hadamard.differentiableOn_divisorPartialProduct_div_pow_sub

theorem differentiableOn_divisorPartialProduct_div_pow_sub    (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ) (k : ℕ)    (s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ))) :    DifferentiableOn ℂ (fun z : ℂ => (divisorPartialProduct m f s z) / (z - z₀) ^ k)      ((Set.univ : Set ℂ) \ {z₀}) := by  have hdiff_prod : DifferentiableOn ℂ (divisorPartialProduct m f s) (Set.univ : Set ℂ) := by    exact (differentiable_divisorPartialProduct m f s).differentiableOn  have hdiff_den : DifferentiableOn ℂ (fun z : ℂ => (z - z₀) ^ k) ((Set.univ : Set ℂ) \ {z₀}) := by    have : Differentiable ℂ (fun z : ℂ => (z - z₀) ^ k) := by      fun_prop    exact this.differentiableOn  by_cases hk : k = 0  · subst hk    simpa [pow_zero] using! (hdiff_prod.mono (by intro z hz; exact hz.1))  · have hne : ∀ z ∈ ((Set.univ : Set ℂ) \ {z₀}), (fun z : ℂ => (z - z₀) ^ k) z ≠ 0 := by      intro z hz      have hz' : z ≠ z₀ := by        simpa [Set.mem_sdiff, Set.mem_singleton_iff] using hz.2      exact pow_ne_zero _ (sub_ne_zero.mpr hz')    have hdiff_inv :        DifferentiableOn ℂ (fun z : ℂ => ((z - z₀) ^ k)⁻¹) ((Set.univ : Set ℂ) \ {z₀}) :=      hdiff_den.inv hne    simpa [div_eq_mul_inv] using! (hdiff_prod.mono (by intro z hz; exact hz.1)).mul hdiff_inv