case neg =>
  obtain ⟨z₀, hz₀⟩ : U.Nonempty := good_domain.is_nonempty
  have : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f z)) := by
    refine λ z hz => (map_mono inf_le_left).trans ?_
    exact ((UniformOnFun.uniformContinuous_eval_of_mem ℂ (compacts U)
      (mem_singleton z) ⟨singleton_subset_iff.2 hz, isCompact_singleton⟩).continuous).tendsto f
  refine Or.inr ⟨f z₀, λ z hz => tendsto_nhds_unique ((this z hz).congr' ?_) (this z₀ hz₀)⟩
  filter_upwards [not_frequently.1 h, h2] with f hf1 hf2
  obtain ⟨w, hw⟩ := hf2.2.resolve_left hf1
  exact (hw hz).trans (hw hz₀).symm
ι : 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
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U
no goals