refine ⟨x, h1, y, h3, h2, h4⟩
case intro.intro.intro.intro.intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
hU' : IsPreconnected U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hi : ∃ᶠ (n : ι) in p, InjOn (F n) U
x : ℂ
h1 : x ∈ U
y : ℂ
h2 : f x = f y
h3 : y ∈ U
h4 : ¬x = y
⊢ ∃ x ∈ U, ∃ y ∈ U, f x = f y ∧ x ≠ y
no goals