case neg =>
  rw [norm_eq_abs] at h
  have g'0_le_1 := abs_deriv_le_one_of_mapsTo_ball g_diff g_maps g_0_eq_0 zero_lt_one
  have g'0_lt_1 : abs (deriv g 0) < 1 := Ne.lt_of_le h g'0_le_1
  have g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻) u * deriv f 0 :=
    deriv.comp 0 ((φ u_in_𝔻).is_diff.differentiableAt (isOpen_ball.mem_nhds u_in_𝔻))
      (f_diff.differentiableAt (ball_mem_nhds _ zero_lt_one))
  have e1 : 1 - (normSq u : ℂ) ≠ 0 := by
    simpa [normSq_eq_conj_mul_self, mul_comm] using one_sub_mul_conj_ne_zero u_in_𝔻 u_in_𝔻
  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
  have e2 : 0 ≤ normSq u := normSq_nonneg _
  have e3 : normSq u < 1 := by
    rw [normSq_eq_abs]
    have : abs u < 1 := mem_𝔻_iff.mp u_in_𝔻
    simp only [sq_lt_one_iff_abs_lt_one, Complex.abs_abs, this]
  simp [normSq_eq_abs, ← mem_𝔻_iff]
  simp only [φ'u_u, one_div] at g'0_eq_mul
  rw [eq_comm, inv_mul_eq_iff_eq_mul₀ e1] at g'0_eq_mul
  rw [← norm_eq_abs, g'0_eq_mul, norm_mul, mul_comm, ← one_mul (1 : ℝ)]
  refine mul_lt_mul g'0_lt_1 ?_ (norm_pos_iff.mpr e1) zero_le_one
  simp at e2 e3 ⊢
  norm_cast
  rw [abs_sub_le_iff]
  refine ⟨?_, ?_⟩; repeat linarith
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 : ¬‖deriv g 0‖ = 1
⊢ ‖deriv f 0‖ < 1
no goals