obtain ⟨w, hw⟩ := hf2.2.resolve_left hf1
case h
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f✝ : 𝓒 U
hf : ClusterPt f✝ (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f✝ ⊓ 𝓟 (𝓙 U)
this✝ : NeBot l
h1 : Tendsto id l (𝓝 f✝)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
this : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f✝ z))
z : ℂ
hz : z ∈ U
f : ℂ → ℂ
hf1 : ¬InjOn f U
hf2 : f ∈ {x | id x ∈ 𝓙 U}
⊢ eval z f = eval z₀ f
case h.intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f✝ : 𝓒 U
hf : ClusterPt f✝ (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f✝ ⊓ 𝓟 (𝓙 U)
this✝ : NeBot l
h1 : Tendsto id l (𝓝 f✝)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
this : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f✝ z))
z : ℂ
hz : z ∈ U
f : ℂ → ℂ
hf1 : ¬InjOn f U
hf2 : f ∈ {x | id x ∈ 𝓙 U}
w : ℂ
hw : EqOn (id f) (fun x => w) U
⊢ eval z f = eval z₀ f