have h10 : f '' U ⊆ ball 0 1 := by
  have := ((hf.1.1.analyticOn hU).is_constant_or_isOpen hU').resolve_left h7 U subset_rfl hU
  simpa [interior_closedBall] using this.subset_interior_iff.2 (mapsTo'.1 hf.1.2)
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
h5 : 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
h5 : f ∈ 𝓘 U
h10 : f '' U ⊆ ball 0 1
⊢ f '' U = ball 0 1