simp only [not_frequently, InjOn, not_forall]
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
h : ¬InjOn f U
x : ℂ
hx : x ∈ U
y : ℂ
hy : y ∈ U
hfxy : f x = f y
hxy : x ≠ y
g : ℂ → ℂ := fun z => f z - f x
G : ι → ℂ → ℂ := fun n z => F n z - f x
hG : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (G n) U
hg : TendstoLocallyUniformlyOn G g p U
hgx : g x = 0
hgy : g y = 0
hi : ¬∀ z ∈ U, g z = 0
⊢ ¬∃ᶠ (n : ι) in p, InjOn (F n) U
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
h : ¬InjOn f U
x : ℂ
hx : x ∈ U
y : ℂ
hy : y ∈ U
hfxy : f x = f y
hxy : x ≠ y
g : ℂ → ℂ := fun z => f z - f x
G : ι → ℂ → ℂ := fun n z => F n z - f x
hG : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (G n) U
hg : TendstoLocallyUniformlyOn G g p U
hgx : g x = 0
hgy : g y = 0
hi : ¬∀ z ∈ U, g z = 0
⊢ ∀ᶠ (x : ι) in p, ∃ x_1, ∃ (_ : x_1 ∈ U), ∃ x_2, ∃ (_ : x_2 ∈ U) (_ : F x x_1 = F x x_2), ¬x_1 = x_2