field_simp [_root_.pow_succ, sub_ne_zero.mpr hz]
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hz : z ≠ z₀
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
n : ℕ
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ succ n * g w
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ succ n) z
⊢ ↑(succ n) * (z - z₀) ^ (succ n - 1) * g z / ((z - z₀) ^ succ n * g z) +
      (z - z₀) ^ succ n * deriv g z / ((z - z₀) ^ succ n * g z) =
    ↑(succ n) / (z - z₀) + deriv g z / g z
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hz : z ≠ z₀
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
n : ℕ
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ succ n * g w
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ succ n) z
⊢ ((↑n + 1) * (z - z₀) ^ n * g z + (z - z₀) * (z - z₀) ^ n * deriv g z) * ((z - z₀) * g z) =
    ((↑n + 1) * g z + deriv g z * (z - z₀)) * ((z - z₀) * (z - z₀) ^ n * g z)