have h4 : DifferentiableAt ℂ (λ y => y - z₀) z := (differentiable_id'.sub_const z₀).differentiableAt
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
⊢ deriv f z / f z = ↑n / (z - z₀) + deriv g z / g z
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
⊢ deriv f z / f z = ↑n / (z - z₀) + deriv g z / g z