Theorem: hurwitz_inj (RMT4/hurwitz.lean)

State before:
ι : 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
⊢ (∃ w, ∀ z ∈ U, f z = w) ∨ InjOn f U
Tactic:
refine or_iff_not_imp_right.2 (λ h => ?_)
State after:
ι : 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
⊢ ∃ w, ∀ z ∈ U, f z = w

State before:
ι : 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
⊢ ∃ w, ∀ z ∈ U, f z = w
Tactic:
obtain ⟨x, hx, y, hy, hfxy, hxy⟩ : ∃ x ∈ U, ∃ y ∈ U, f x = f y ∧ x ≠ y := by
  simp [InjOn] at h
  obtain ⟨x, h1, y, h2, h3, h4⟩ := h
  refine ⟨x, h1, y, h3, h2, h4⟩
State after:
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
h : ¬InjOn f U
x : ℂ
hx : x ∈ U
y : ℂ
hy : y ∈ U
hfxy : f x = f y
hxy : x ≠ y
⊢ ∃ w, ∀ z ∈ U, f z = w

State before:
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
h : ¬InjOn f U
x : ℂ
hx : x ∈ U
y : ℂ
hy : y ∈ U
hfxy : f x = f y
hxy : x ≠ y
⊢ ∃ w, ∀ z ∈ U, f z = w
Tactic:
set g : ℂ → ℂ := λ z => f z - f x
State after:
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
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
⊢ ∃ w, ∀ z ∈ U, f z = w

State before:
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
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
⊢ ∃ w, ∀ z ∈ U, f z = w
Tactic:
set G : ι → ℂ → ℂ := λ n z => F n z - f x
State after:
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
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
⊢ ∃ w, ∀ z ∈ U, f z = w

State before:
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
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
⊢ ∃ w, ∀ z ∈ U, f z = w
Tactic:
have hG : ∀ᶠ n in p, DifferentiableOn ℂ (G n) U := by
  filter_upwards [hF] with n hF using hF.sub (differentiableOn_const _)
State after:
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
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
⊢ ∃ w, ∀ z ∈ U, f z = w

State before:
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
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
⊢ ∃ w, ∀ z ∈ U, f z = w
Tactic:
have hg : TendstoLocallyUniformlyOn G g p U :=
  hurwitz4 hf (uniformContinuous_id.sub uniformContinuous_const)
State after:
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
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
⊢ ∃ w, ∀ z ∈ U, f z = w

State before:
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
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
⊢ ∃ w, ∀ z ∈ U, f z = w
Tactic:
have hgx : g x = 0 := sub_self _
State after:
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
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
⊢ ∃ w, ∀ z ∈ U, f z = w

State before:
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
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
⊢ ∃ w, ∀ z ∈ U, f z = w
Tactic:
have hgy : g y = 0 := by simp [g, hfxy]
State after:
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
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
⊢ ∃ w, ∀ z ∈ U, f z = w

State before:
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
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
⊢ ∃ w, ∀ z ∈ U, f z = w
Tactic:
suffices this : ∀ z ∈ U, g z = 0
  by exact ⟨f x, by simpa [sub_eq_zero, g] using this⟩
State after:
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
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
⊢ ∀ z ∈ U, g z = 0

State before:
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
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
⊢ ∀ z ∈ U, g z = 0
Tactic:
contrapose hi
State after:
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

State before:
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
Tactic:
simp only [not_frequently, InjOn, not_forall]
State after:
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

State before:
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
Tactic:
have h1 : DifferentiableOn ℂ g U := hg.differentiableOn hG hU
State after:
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
h1 : DifferentiableOn ℂ g U
⊢ ∀ᶠ (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

State before:
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
h1 : DifferentiableOn ℂ g U
⊢ ∀ᶠ (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
Tactic:
have h2 : ∀ z₀ ∈ U, ∀ᶠ z in 𝓝[≠] z₀, g z ≠ 0 := (hurwitz_1 hU hU' h1).resolve_left hi
State after:
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
h1 : DifferentiableOn ℂ g U
h2 : ∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, 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

State before:
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
h1 : DifferentiableOn ℂ g U
h2 : ∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, 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
Tactic:
obtain ⟨u, v, hu, hv, huv⟩ := t2_separation_nhds hxy
State after:
case intro.intro.intro.intro.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
h1 : DifferentiableOn ℂ g U
h2 : ∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
u v : Set ℂ
hu : u ∈ 𝓝 x
hv : v ∈ 𝓝 y
huv : Disjoint u v
⊢ ∀ᶠ (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

State before:
case intro.intro.intro.intro.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
h1 : DifferentiableOn ℂ g U
h2 : ∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
u v : Set ℂ
hu : u ∈ 𝓝 x
hv : v ∈ 𝓝 y
huv : Disjoint u v
⊢ ∀ᶠ (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
Tactic:
have h3 := hurwitz3 hU hG hg hx hgx (h2 x hx) (inter_mem hu (hU.mem_nhds hx))
State after:
case intro.intro.intro.intro.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
h1 : DifferentiableOn ℂ g U
h2 : ∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
u v : Set ℂ
hu : u ∈ 𝓝 x
hv : v ∈ 𝓝 y
huv : Disjoint u v
h3 : ∀ᶠ (n : ι) in p, ∃ z ∈ u ∩ U, G n 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

State before:
case intro.intro.intro.intro.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
h1 : DifferentiableOn ℂ g U
h2 : ∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
u v : Set ℂ
hu : u ∈ 𝓝 x
hv : v ∈ 𝓝 y
huv : Disjoint u v
h3 : ∀ᶠ (n : ι) in p, ∃ z ∈ u ∩ U, G n 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
Tactic:
have h4 := hurwitz3 hU hG hg hy hgy (h2 y hy) (inter_mem hv (hU.mem_nhds hy))
State after:
case intro.intro.intro.intro.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
h1 : DifferentiableOn ℂ g U
h2 : ∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
u v : Set ℂ
hu : u ∈ 𝓝 x
hv : v ∈ 𝓝 y
huv : Disjoint u v
h3 : ∀ᶠ (n : ι) in p, ∃ z ∈ u ∩ U, G n z = 0
h4 : ∀ᶠ (n : ι) in p, ∃ z ∈ v ∩ U, G n 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

State before:
case intro.intro.intro.intro.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
h1 : DifferentiableOn ℂ g U
h2 : ∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
u v : Set ℂ
hu : u ∈ 𝓝 x
hv : v ∈ 𝓝 y
huv : Disjoint u v
h3 : ∀ᶠ (n : ι) in p, ∃ z ∈ u ∩ U, G n z = 0
h4 : ∀ᶠ (n : ι) in p, ∃ z ∈ v ∩ U, G n 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
Tactic:
filter_upwards [h3.and h4] with n hn
State after:
case 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
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
h1 : DifferentiableOn ℂ g U
h2 : ∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
u v : Set ℂ
hu : u ∈ 𝓝 x
hv : v ∈ 𝓝 y
huv : Disjoint u v
h3 : ∀ᶠ (n : ι) in p, ∃ z ∈ u ∩ U, G n z = 0
h4 : ∀ᶠ (n : ι) in p, ∃ z ∈ v ∩ U, G n z = 0
n : ι
hn : (∃ z ∈ u ∩ U, G n z = 0) ∧ ∃ z ∈ v ∩ U, G n z = 0
⊢ ∃ x, ∃ (_ : x ∈ U), ∃ x_1, ∃ (_ : x_1 ∈ U) (_ : F n x = F n x_1), ¬x = x_1

State before:
case 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
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
h1 : DifferentiableOn ℂ g U
h2 : ∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
u v : Set ℂ
hu : u ∈ 𝓝 x
hv : v ∈ 𝓝 y
huv : Disjoint u v
h3 : ∀ᶠ (n : ι) in p, ∃ z ∈ u ∩ U, G n z = 0
h4 : ∀ᶠ (n : ι) in p, ∃ z ∈ v ∩ U, G n z = 0
n : ι
hn : (∃ z ∈ u ∩ U, G n z = 0) ∧ ∃ z ∈ v ∩ U, G n z = 0
⊢ ∃ x, ∃ (_ : x ∈ U), ∃ x_1, ∃ (_ : x_1 ∈ U) (_ : F n x = F n x_1), ¬x = x_1
Tactic:
obtain ⟨⟨xn, hxn, hGxn⟩, ⟨yn, hyn, hGyn⟩⟩ := hn
State after:
case h.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
h1 : DifferentiableOn ℂ g U
h2 : ∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
u v : Set ℂ
hu : u ∈ 𝓝 x
hv : v ∈ 𝓝 y
huv : Disjoint u v
h3 : ∀ᶠ (n : ι) in p, ∃ z ∈ u ∩ U, G n z = 0
h4 : ∀ᶠ (n : ι) in p, ∃ z ∈ v ∩ U, G n z = 0
n : ι
xn : ℂ
hxn : xn ∈ u ∩ U
hGxn : G n xn = 0
yn : ℂ
hyn : yn ∈ v ∩ U
hGyn : G n yn = 0
⊢ ∃ x, ∃ (_ : x ∈ U), ∃ x_1, ∃ (_ : x_1 ∈ U) (_ : F n x = F n x_1), ¬x = x_1

State before:
case h.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
h1 : DifferentiableOn ℂ g U
h2 : ∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
u v : Set ℂ
hu : u ∈ 𝓝 x
hv : v ∈ 𝓝 y
huv : Disjoint u v
h3 : ∀ᶠ (n : ι) in p, ∃ z ∈ u ∩ U, G n z = 0
h4 : ∀ᶠ (n : ι) in p, ∃ z ∈ v ∩ U, G n z = 0
n : ι
xn : ℂ
hxn : xn ∈ u ∩ U
hGxn : G n xn = 0
yn : ℂ
hyn : yn ∈ v ∩ U
hGyn : G n yn = 0
⊢ ∃ x, ∃ (_ : x ∈ U), ∃ x_1, ∃ (_ : x_1 ∈ U) (_ : F n x = F n x_1), ¬x = x_1
Tactic:
refine ⟨xn, hxn.2, yn, hyn.2, ?_, huv.ne_of_mem hxn.1 hyn.1⟩
State after:
case h.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
h1 : DifferentiableOn ℂ g U
h2 : ∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
u v : Set ℂ
hu : u ∈ 𝓝 x
hv : v ∈ 𝓝 y
huv : Disjoint u v
h3 : ∀ᶠ (n : ι) in p, ∃ z ∈ u ∩ U, G n z = 0
h4 : ∀ᶠ (n : ι) in p, ∃ z ∈ v ∩ U, G n z = 0
n : ι
xn : ℂ
hxn : xn ∈ u ∩ U
hGxn : G n xn = 0
yn : ℂ
hyn : yn ∈ v ∩ U
hGyn : G n yn = 0
⊢ F n xn = F n yn

State before:
case h.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
h1 : DifferentiableOn ℂ g U
h2 : ∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
u v : Set ℂ
hu : u ∈ 𝓝 x
hv : v ∈ 𝓝 y
huv : Disjoint u v
h3 : ∀ᶠ (n : ι) in p, ∃ z ∈ u ∩ U, G n z = 0
h4 : ∀ᶠ (n : ι) in p, ∃ z ∈ v ∩ U, G n z = 0
n : ι
xn : ℂ
hxn : xn ∈ u ∩ U
hGxn : G n xn = 0
yn : ℂ
hyn : yn ∈ v ∩ U
hGyn : G n yn = 0
⊢ F n xn = F n yn
Tactic:
rw [sub_eq_zero] at hGxn hGyn
State after:
case h.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
h1 : DifferentiableOn ℂ g U
h2 : ∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
u v : Set ℂ
hu : u ∈ 𝓝 x
hv : v ∈ 𝓝 y
huv : Disjoint u v
h3 : ∀ᶠ (n : ι) in p, ∃ z ∈ u ∩ U, G n z = 0
h4 : ∀ᶠ (n : ι) in p, ∃ z ∈ v ∩ U, G n z = 0
n : ι
xn : ℂ
hxn : xn ∈ u ∩ U
hGxn : F n xn = f x
yn : ℂ
hyn : yn ∈ v ∩ U
hGyn : F n yn = f x
⊢ F n xn = F n yn

State before:
case h.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
h1 : DifferentiableOn ℂ g U
h2 : ∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
u v : Set ℂ
hu : u ∈ 𝓝 x
hv : v ∈ 𝓝 y
huv : Disjoint u v
h3 : ∀ᶠ (n : ι) in p, ∃ z ∈ u ∩ U, G n z = 0
h4 : ∀ᶠ (n : ι) in p, ∃ z ∈ v ∩ U, G n z = 0
n : ι
xn : ℂ
hxn : xn ∈ u ∩ U
hGxn : F n xn = f x
yn : ℂ
hyn : yn ∈ v ∩ U
hGyn : F n yn = f x
⊢ F n xn = F n yn
Tactic:
rw [hGxn, hGyn]
State after:
no goals

State before:
ι : 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
Tactic:
simp [InjOn] at h
State after:
ι : 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

State before:
ι : 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
Tactic:
obtain ⟨x, h1, y, h2, h3, h4⟩ := h
State after:
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

State before:
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
Tactic:
refine ⟨x, h1, y, h3, h2, h4⟩
State after:
no goals

State before:
ι : 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 : ℂ
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
⊢ ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (G n) U
Tactic:
filter_upwards [hF] with n hF using hF.sub (differentiableOn_const _)
State after:
no goals

State before:
ι : 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 : ℂ
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
⊢ g y = 0
Tactic:
simp [g, hfxy]
State after:
no goals

State before:
ι : 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 : ℂ
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
this : ∀ z ∈ U, g z = 0
⊢ ∃ w, ∀ z ∈ U, f z = w
Tactic:
exact ⟨f x, by simpa [sub_eq_zero, g] using this⟩
State after:
no goals

State before:
ι : 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 : ℂ
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
this : ∀ z ∈ U, g z = 0
⊢ ∀ z ∈ U, f z = f x
Tactic:
simpa [sub_eq_zero, g] using this
State after:
no goals