field_simp [h3]
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
h5 : deriv (fun z => 1 - z * (starRingEnd ℂ) u) z = -(starRingEnd ℂ) u
⊢ (1 - z * (starRingEnd ℂ) u + (z - u) * (starRingEnd ℂ) u) / (1 - z * (starRingEnd ℂ) u) ^ 2 =
    (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
h5 : deriv (fun z => 1 - z * (starRingEnd ℂ) u) z = -(starRingEnd ℂ) u
⊢ 1 - z * (starRingEnd ℂ) u + (z - u) * (starRingEnd ℂ) u = 1 - u * (starRingEnd ℂ) u