have h7 : ¬ ∃ w, EqOn f (λ _ => w) U := by
  obtain ⟨g, hg⟩ : (𝓘 U).Nonempty := 𝓘_nonempty
  specialize hfg g (𝓘_subset_𝓙 hg)
  have := norm_pos_iff.1 ((norm_pos_iff.2 (deriv_ne_zero_of_inj hU hg.1.1 hg.2 hz₀)).trans_le hfg)
  contrapose! this
  obtain ⟨w, hw : EqOn f (λ _ => w) U⟩ := this
  simpa only [deriv_const'] using (hw.eventuallyEq_of_mem (hU.mem_nhds hz₀)).deriv_eq
case intro.intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
case intro.intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1