case pos =>
  have g_lin : EqOn g (λ (z : ℂ) => z • deriv g 0) (ball 0 1) := by
    have h2 : MapsTo g (ball 0 1) (ball (g 0) 1) := by rwa [g_0_eq_0]
    have h1 : Set.EqOn g (fun z => g 0 + (z - 0) • dslope g 0 0) (Metric.ball 0 1) := by
      apply affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div g_diff h2 (mem_ball_self zero_lt_one)
      rwa [dslope_same, div_one]
    convert h1 using 1
    ext1 z
    rw [g_0_eq_0, zero_add, sub_zero, dslope_same]
  have g'0_ne_0 : deriv g 0 ≠ 0 := λ h' => by simp [h'] at h
  have g_inj : InjOn g 𝔻 := λ x hx y hy => by
    rw [g_lin hx, g_lin hy]
    simp [g'0_ne_0]
  cases f_noninj (injOn_of_injOn_comp g_inj)
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