simp [InjOn] at h
ι : 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
h : ¬InjOn f U
⊢ ∃ x ∈ U, ∃ y ∈ U, f x = f y ∧ x ≠ y
ι : 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
h : ∃ x ∈ U, ∃ x_1, f x = f x_1 ∧ x_1 ∈ U ∧ ¬x = x_1
⊢ ∃ x ∈ U, ∃ y ∈ U, f x = f y ∧ x ≠ y