convert h1 using 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 : ‖deriv g 0‖ = 1
h2 : MapsTo g (ball 0 1) (ball (g 0) 1)
h1 : EqOn g (fun z => g 0 + (z - 0) • dslope g 0 0) (ball 0 1)
⊢ EqOn g (fun z => z • deriv g 0) (ball 0 1)
case h.e'_4
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
h2 : MapsTo g (ball 0 1) (ball (g 0) 1)
h1 : EqOn g (fun z => g 0 + (z - 0) • dslope g 0 0) (ball 0 1)
⊢ (fun z => z • deriv g 0) = fun z => g 0 + (z - 0) • dslope g 0 0