field_simp [pre_φ, one_sub_mul_conj_ne_zero hu hz, one_sub_mul_conj_add_mul_conj_ne_zero hu]
z✝ u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
z : ℂ
hz : z ∈ 𝔻
⊢ pre_φ (-u) (pre_φ u z) = z
z✝ u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
z : ℂ
hz : z ∈ 𝔻
⊢ z - u + (1 - z * (starRingEnd ℂ) u) * u = z * (1 - z * (starRingEnd ℂ) u + (z - u) * (starRingEnd ℂ) u)