have : deriv (fun y => y - z₀) z = 1 := by
  change deriv (fun y => id y - z₀) z = 1
  simp [deriv_sub_const]
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
e0 : U ∈ 𝓝 z
h4 : deriv f z = deriv (fun w => (w - z₀) * g w) z
e1 : DifferentiableAt ℂ (fun y => y - z₀) z
e2 : DifferentiableAt ℂ g z
⊢ deriv f z = g z + (z - z₀) * deriv g z
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
e0 : U ∈ 𝓝 z
h4 : deriv f z = deriv (fun w => (w - z₀) * g w) z
e1 : DifferentiableAt ℂ (fun y => y - z₀) z
e2 : DifferentiableAt ℂ g z
this : deriv (fun y => y - z₀) z = 1
⊢ deriv f z = g z + (z - z₀) * deriv g z