Complex.logDeriv_weierstrassFactor_one_div

theorem logDeriv_weierstrassFactor_one_div {a z : ℂ} (ha : a ≠ 0) (hz : z ≠ a) :    logDeriv (fun w : ℂ => weierstrassFactor 1 (w / a)) z =      1 / (z - a) + 1 / a := by  have hE :      (fun w : ℂ => weierstrassFactor 1 (w / a)) =        fun w : ℂ => (1 - w / a) * exp (w / a) := by    ext w    simp [weierstrassFactor_def, partialLogSum_eq_sum]  have hf : (1 - z / a) ≠ 0 := by    intro hzero    have hdiv : z / a = 1 := by      exact (sub_eq_zero.mp hzero).symm    exact hz ((div_eq_one_iff_eq ha).1 hdiv)  rw [hE, logDeriv_mul z hf (exp_ne_zero (z / a)) (by fun_prop) (by fun_prop)]  have hleft : logDeriv (fun w : ℂ => 1 - w / a) z = 1 / (z - a) := by    rw [logDeriv_apply]    have hderiv : deriv (fun w : ℂ => 1 - w / a) z = -(1 / a) := by      simp [one_div]    rw [hderiv]    have haz : -z + a ≠ 0 := by      simpa [sub_eq_add_neg, add_comm] using sub_ne_zero.mpr (Ne.symm hz)    field_simp [ha, sub_ne_zero.mpr hz, haz]    have haz' : a - z ≠ 0 := sub_ne_zero.mpr (Ne.symm hz)    have hza : z - a = -(a - z) := by ring    rw [hza]    field_simp [haz']  have hright : logDeriv (fun w : ℂ => exp (w / a)) z = 1 / a := by    rw [logDeriv_apply]    have hderiv : deriv (fun w : ℂ => exp (w / a)) z =        exp (z / a) * (1 / a) := by      simp [one_div]    rw [hderiv]    field_simp [exp_ne_zero (z / a)]  rw [hleft, hright]