internlm/Lean-Github huggingface dataset:
Theorem: hurwitz_inj
Proof 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 _
Proof 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
Theorem: hurwitz_inj
Proof 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]
Proof 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
Theorem: hurwitz_inj
Proof 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⟩
Proof 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
Theorem: hurwitz_inj
Proof 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
Proof 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
Theorem: hurwitz_inj
Proof 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]
Proof 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
Theorem: hurwitz_inj
Proof 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
Proof 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
Theorem: hurwitz_inj
Proof 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
Proof 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
Theorem: hurwitz_inj
Proof 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
Proof 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
Theorem: hurwitz_inj
Proof 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))
Proof 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
Theorem: hurwitz_inj
Proof 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))
Proof 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
Theorem: hurwitz_inj
Proof 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
Proof 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
Theorem: hurwitz_inj
Proof 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
Proof 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
Theorem: hurwitz_inj
Proof 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⟩
Proof 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
Theorem: hurwitz_inj
Proof 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
Proof 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
Theorem: hurwitz_inj
Proof 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]
Proof state after:
no goals
Theorem: hurwitz_inj
Proof 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
Proof 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