ZetaAppendix.lemma_abadeulmit2_deriv_neg_pi_mul_cot_pi_mul

lemma lemma_abadeulmit2_deriv_neg_pi_mul_cot_pi_mul {z : ℂ} (hz : z ∈ integerComplement) :  deriv (fun w ↦ -π * Complex.cot (π * w)) z =  π ^ 2 / (Complex.sin (π * z)) ^ 2 := by  have hsin : sin (π * z) ≠ 0 := sin_pi_mul_ne_zero hz  have h_deriv_cot : HasDerivAt (fun w ↦ Complex.cot (π * w)) (-(π / sin (π * z) ^ 2)) z := by    have h1 : HasDerivAt (fun (w : ℂ) ↦ (π : ℂ) * w) π z := by      convert! hasDerivAt_mul_const (π : ℂ) using 1      ext; ring    have h2 : HasDerivAt Complex.cot (-(1 / sin (π * z) ^ 2)) (π * z) := by      unfold Complex.cot      convert! (hasDerivAt_cos (π * z)).div (hasDerivAt_sin (π * z)) hsin using 1      field_simp      linear_combination Complex.sin_sq_add_cos_sq (π * z)    convert! h2.comp z h1 using 1    ring  rw [deriv_const_mul _ h_deriv_cot.differentiableAt, h_deriv_cot.deriv]  field_simp