contrapose! this
case 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
g : 𝓒 U
hg : g ∈ 𝓘 U
hfg : obs z₀ g ≤ obs z₀ f
this : deriv f z₀ ≠ 0
⊢ ¬∃ w, EqOn f (fun x => w) U
case 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
g : 𝓒 U
hg : g ∈ 𝓘 U
hfg : obs z₀ g ≤ obs z₀ f
this : ∃ w, EqOn f (fun x => w) U
⊢ deriv f z₀ = 0