have h4 : deriv (fun z => z - u) z = 1 := by simp [deriv_sub_const]
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
h1 : DifferentiableAt ℂ (fun z => z - u) z
h2 : DifferentiableAt ℂ (fun z => 1 - z * (starRingEnd ℂ) u) z
h3 : 1 - z * (starRingEnd ℂ) u ≠ 0
⊢ deriv (φ hu).to_fun z = (1 - u * (starRingEnd ℂ) u) / (1 - z * (starRingEnd ℂ) u) ^ 2
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
h1 : DifferentiableAt ℂ (fun z => z - u) z
h2 : DifferentiableAt ℂ (fun z => 1 - z * (starRingEnd ℂ) u) z
h3 : 1 - z * (starRingEnd ℂ) u ≠ 0
h4 : deriv (fun z => z - u) z = 1
⊢ deriv (φ hu).to_fun z = (1 - u * (starRingEnd ℂ) u) / (1 - z * (starRingEnd ℂ) u) ^ 2