cases n
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ n) z
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
⊢ ↑n * (z - z₀) ^ (n - 1) * g z / ((z - z₀) ^ n * g z) + (z - z₀) ^ n * deriv g z / ((z - z₀) ^ n * g z) =
    ↑n / (z - z₀) + deriv g z / g z
case zero
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
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ zero * g w
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ zero) z
⊢ ↑zero * (z - z₀) ^ (zero - 1) * g z / ((z - z₀) ^ zero * g z) +
      (z - z₀) ^ zero * deriv g z / ((z - z₀) ^ zero * g z) =
    ↑zero / (z - z₀) + deriv g z / g z

case succ
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