simp [DifferentiableAt.mul_const]
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
h1 : DifferentiableAt ℂ (fun z => z - u) z
⊢ DifferentiableAt ℂ (fun z => 1 - z * (starRingEnd ℂ) u) z
no goals