rintro z hz
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
⊢ LeftInvOn (pre_φ (-u)) (pre_φ u) 𝔻
z✝ u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
z : ℂ
hz : z ∈ 𝔻
⊢ pre_φ (-u) (pre_φ u z) = z