rw [mem_𝔻_iff] at hu hz
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
⊢ 1 - z * (starRingEnd ℂ) u ≠ 0
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : ‖u‖ < 1
hz : ‖z‖ < 1
⊢ 1 - z * (starRingEnd ℂ) u ≠ 0