Complex.Hadamard.differentiable_divisorComplementPartialProduct

theorem differentiable_divisorComplementPartialProduct    (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ)    (s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ))) :    Differentiable ℂ (divisorComplementPartialProduct m f z₀ s) := by  let Φ : divisorZeroIndex₀ f (Set.univ : Set ℂ) → ℂ → ℂ :=    fun p z => divisorComplementFactor m f z₀ p z  have hΦ : ∀ p ∈ s, Differentiable ℂ (Φ p) := by    intro p _hp    by_cases hpF : p ∈ divisorZeroIndex₀_fiberFinset (f := f) z₀    · have hΦp : Φ p = fun _ => (1 : ℂ) := by        ext z        simp only [Φ, divisorComplementFactor_eq_one_of_mem m f z₀ p z hpF]      rw [hΦp]      exact differentiable_const (1 : ℂ)    · have hΦp : Φ p = fun z => weierstrassFactor m (z / divisorZeroIndex₀_val p) := by        ext z        simp only [Φ, divisorComplementFactor_eq_weierstrassFactor_of_not_mem m f z₀ p z hpF]      rw [hΦp]      exact differentiable_weierstrassFactor_divisorZeroIndex₀ m p  have hEq : (fun z : ℂ => ∏ p ∈ s, Φ p z) =      divisorComplementPartialProduct m f z₀ s := by    ext z    simp [Φ, divisorComplementPartialProduct]  have : Differentiable ℂ (fun z : ℂ => ∏ p ∈ s, Φ p z) := by    simpa using (Differentiable.fun_finsetProd (𝕜 := ℂ) (f := Φ) (u := s) hΦ)  simpa [hEq] using this