have φ'u_u : deriv (φ u_in_𝔻) u = 1 / (1 - normSq u) := by
  set w := 1 - conj u * u with hw
  have : w ≠ 0 := by simpa [normSq_eq_conj_mul_self, mul_comm u] using e1
  rw [φ_deriv u_in_𝔻 u_in_𝔻, normSq_eq_conj_mul_self, mul_comm u, ← hw]
  field_simp; ring
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
⊢ ‖deriv f 0‖ < 1
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
⊢ ‖deriv f 0‖ < 1