Complex.hasDerivAt_partialLogSum

lemma hasDerivAt_partialLogSum (m : ℕ) (z : ℂ) :    HasDerivAt (partialLogSum m) (∑ j ∈ Finset.range m, z ^ j) z := by  cases m with  | zero =>      have hzero : partialLogSum 0 = fun _ : ℂ ↦ (0 : ℂ) := by        funext w        exact partialLogSum_zero w      simpa [hzero] using (hasDerivAt_const z (c := (0 : ℂ)))  | succ m =>      have hsum :          (∑ j ∈ Finset.range (m + 1), z ^ j) =            ∑ j ∈ Finset.range (m + 1), (-1) ^ j * (-z) ^ j := by        refine Finset.sum_congr rfl ?_        intro j hj        symm        calc          (-1 : ℂ) ^ j * (-z) ^ j = (-1 : ℂ) ^ j * (((-1 : ℂ) * z) ^ j) := by simp          _ = ((-1 : ℂ) ^ j * (-1 : ℂ) ^ j) * z ^ j := by rw [mul_pow]; ring          _ = z ^ j := by                rw [← pow_add, show j + j = 2 * j by omega, pow_mul]                norm_num      rw [hsum]      simpa [partialLogSum] using!        (((hasDerivAt_logTaylor (m + 1) (-z)).comp z (hasDerivAt_neg z)).neg)