have deriv_eq_mul : deriv f z₀ = deriv ψ 0 * deriv h z₀ := by
  have e1 : U ∈ 𝓝 z₀ := good_domain.is_open.mem_nhds hz₀
  have e2 : 𝔻 ∈ 𝓝 (0 : ℂ) := ball_mem_nhds _ zero_lt_one
  have e3 : deriv f z₀ = deriv (ψ ∘ h) z₀ := (eventuallyEq_of_mem e1 f_eq_ψ_h).deriv_eq
  rw [e3, ← h_z₀_eq_0]
  refine deriv.comp z₀ ?_ (h.is_diff.differentiableAt e1)
  rw [h_z₀_eq_0]
  exact ψ_is_diff.differentiableAt e2
case intro.intro.mk
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖
case intro.intro.mk
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
deriv_eq_mul : deriv f.to_fun z₀ = deriv ψ 0 * deriv h.to_fun z₀
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖