internlm/Lean-Github huggingface dataset:
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 : ∃ 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
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
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
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
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⟩
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 : ℂ
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 _)
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 : ℂ
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]
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 : ℂ
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⟩
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 : ℂ
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
Proof state after:
no goals
Theorem: IsCompact_𝓙
Proof state before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
⊢ IsCompact (𝓙 U)
Tactic:
have hU : IsOpen U := good_domain.is_open
Proof state after:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
⊢ IsCompact (𝓙 U)
Theorem: IsCompact_𝓙
Proof state before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
⊢ IsCompact (𝓙 U)
Tactic:
refine (isCompact_𝓜 hU).of_isClosed_subset ?_ (λ _ hf => hf.1)
Proof state after:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
⊢ IsClosed (𝓙 U)
Theorem: IsCompact_𝓙
Proof state before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
⊢ IsClosed (𝓙 U)
Tactic:
refine isClosed_iff_clusterPt.2 (λ f hf => ?_)
Proof state after:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
⊢ f ∈ 𝓙 U
Theorem: IsCompact_𝓙
Proof state before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
⊢ f ∈ 𝓙 U
Tactic:
set l := 𝓝 f ⊓ 𝓟 (𝓙 U)
Proof state after:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
⊢ f ∈ 𝓙 U
Theorem: IsCompact_𝓙
Proof state before:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
⊢ f ∈ 𝓙 U
Tactic:
haveI : l.NeBot := hf
Proof state after:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
⊢ f ∈ 𝓙 U
Theorem: IsCompact_𝓙
Proof state before:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
⊢ f ∈ 𝓙 U
Tactic:
obtain ⟨h1, h2⟩ := tendsto_inf.1 (@tendsto_id _ l)
Proof state after:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : Tendsto id l (𝓟 (𝓙 U))
⊢ f ∈ 𝓙 U
Theorem: IsCompact_𝓙
Proof state before:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : Tendsto id l (𝓟 (𝓙 U))
⊢ f ∈ 𝓙 U
Tactic:
rw [tendsto_principal] at h2
Proof state after:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
⊢ f ∈ 𝓙 U
Theorem: IsCompact_𝓙
Proof state before:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
⊢ f ∈ 𝓙 U
Tactic:
refine ⟨(IsClosed_𝓜 hU).mem_of_tendsto h1 (h2.mono (λ _ h => h.1)), ?_⟩
Proof state after:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U
Theorem: IsCompact_𝓙
Proof state before:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U
Tactic:
by_cases h : ∃ᶠ f in l, InjOn f U
Proof state after:
case pos
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U

case neg
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U
Theorem: IsCompact_𝓙
Proof state before:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U
Tactic:
case pos =>
  refine (hurwitz_inj hU good_domain.is_preconnected ?_ ((tendsto_𝓒_iff hU).1 h1) h).symm
  filter_upwards [h2] with g hg using hg.1.1
Proof state after:
no goals
Theorem: IsCompact_𝓙
Proof state before:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U
Tactic:
case neg =>
  obtain ⟨z₀, hz₀⟩ : U.Nonempty := good_domain.is_nonempty
  have : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f z)) := by
    refine λ z hz => (map_mono inf_le_left).trans ?_
    exact ((UniformOnFun.uniformContinuous_eval_of_mem ℂ (compacts U)
      (mem_singleton z) ⟨singleton_subset_iff.2 hz, isCompact_singleton⟩).continuous).tendsto f
  refine Or.inr ⟨f z₀, λ z hz => tendsto_nhds_unique ((this z hz).congr' ?_) (this z₀ hz₀)⟩
  filter_upwards [not_frequently.1 h, h2] with f hf1 hf2
  obtain ⟨w, hw⟩ := hf2.2.resolve_left hf1
  exact (hw hz).trans (hw hz₀).symm
Proof state after:
no goals
Theorem: IsCompact_𝓙
Proof state before:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U
Tactic:
refine (hurwitz_inj hU good_domain.is_preconnected ?_ ((tendsto_𝓒_iff hU).1 h1) h).symm
Proof state after:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
⊢ ∀ᶠ (n : 𝓒 U) in l, DifferentiableOn ℂ (id n) U
Theorem: IsCompact_𝓙
Proof state before:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
⊢ ∀ᶠ (n : 𝓒 U) in l, DifferentiableOn ℂ (id n) U
Tactic:
filter_upwards [h2] with g hg using hg.1.1
Proof state after:
no goals
Theorem: IsCompact_𝓙
Proof state before:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U
Tactic:
obtain ⟨z₀, hz₀⟩ : U.Nonempty := good_domain.is_nonempty
Proof state after:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U
Theorem: IsCompact_𝓙
Proof state before:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U
Tactic:
have : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f z)) := by
  refine λ z hz => (map_mono inf_le_left).trans ?_
  exact ((UniformOnFun.uniformContinuous_eval_of_mem ℂ (compacts U)
    (mem_singleton z) ⟨singleton_subset_iff.2 hz, isCompact_singleton⟩).continuous).tendsto f
Proof state after:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this✝ : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
this : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f z))
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U
Theorem: IsCompact_𝓙
Proof state before:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this✝ : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
this : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f z))
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U
Tactic:
refine Or.inr ⟨f z₀, λ z hz => tendsto_nhds_unique ((this z hz).congr' ?_) (this z₀ hz₀)⟩
Proof state after:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this✝ : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
this : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f z))
z : ℂ
hz : z ∈ U
⊢ eval z =ᶠ[l] eval z₀
Theorem: IsCompact_𝓙
Proof state before:
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this✝ : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
this : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f z))
z : ℂ
hz : z ∈ U
⊢ eval z =ᶠ[l] eval z₀
Tactic:
filter_upwards [not_frequently.1 h, h2] with f hf1 hf2
Proof state after:
case h
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f✝ : 𝓒 U
hf : ClusterPt f✝ (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f✝ ⊓ 𝓟 (𝓙 U)
this✝ : NeBot l
h1 : Tendsto id l (𝓝 f✝)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
this : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f✝ z))
z : ℂ
hz : z ∈ U
f : ℂ → ℂ
hf1 : ¬InjOn f U
hf2 : f ∈ {x | id x ∈ 𝓙 U}
⊢ eval z f = eval z₀ f
Theorem: IsCompact_𝓙
Proof state before:
case h
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f✝ : 𝓒 U
hf : ClusterPt f✝ (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f✝ ⊓ 𝓟 (𝓙 U)
this✝ : NeBot l
h1 : Tendsto id l (𝓝 f✝)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
this : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f✝ z))
z : ℂ
hz : z ∈ U
f : ℂ → ℂ
hf1 : ¬InjOn f U
hf2 : f ∈ {x | id x ∈ 𝓙 U}
⊢ eval z f = eval z₀ f
Tactic:
obtain ⟨w, hw⟩ := hf2.2.resolve_left hf1
Proof state after:
case h.intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f✝ : 𝓒 U
hf : ClusterPt f✝ (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f✝ ⊓ 𝓟 (𝓙 U)
this✝ : NeBot l
h1 : Tendsto id l (𝓝 f✝)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
this : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f✝ z))
z : ℂ
hz : z ∈ U
f : ℂ → ℂ
hf1 : ¬InjOn f U
hf2 : f ∈ {x | id x ∈ 𝓙 U}
w : ℂ
hw : EqOn (id f) (fun x => w) U
⊢ eval z f = eval z₀ f
Theorem: IsCompact_𝓙
Proof state before:
case h.intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f✝ : 𝓒 U
hf : ClusterPt f✝ (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f✝ ⊓ 𝓟 (𝓙 U)
this✝ : NeBot l
h1 : Tendsto id l (𝓝 f✝)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
this : ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f✝ z))
z : ℂ
hz : z ∈ U
f : ℂ → ℂ
hf1 : ¬InjOn f U
hf2 : f ∈ {x | id x ∈ 𝓙 U}
w : ℂ
hw : EqOn (id f) (fun x => w) U
⊢ eval z f = eval z₀ f
Tactic:
exact (hw hz).trans (hw hz₀).symm
Proof state after:
no goals
Theorem: IsCompact_𝓙
Proof state before:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
⊢ ∀ z ∈ U, Tendsto (eval z) l (𝓝 (f z))
Tactic:
refine λ z hz => (map_mono inf_le_left).trans ?_
Proof state after:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
z : ℂ
hz : z ∈ U
⊢ map (eval z) (𝓝 f) ≤ 𝓝 (f z)
Theorem: IsCompact_𝓙
Proof state before:
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
h : ¬∃ᶠ (f : ℂ → ℂ) in l, InjOn f U
z₀ : ℂ
hz₀ : z₀ ∈ U
z : ℂ
hz : z ∈ U
⊢ map (eval z) (𝓝 f) ≤ 𝓝 (f z)
Tactic:
exact ((UniformOnFun.uniformContinuous_eval_of_mem ℂ (compacts U)
  (mem_singleton z) ⟨singleton_subset_iff.2 hz, isCompact_singleton⟩).continuous).tendsto f
Proof state after:
no goals
Theorem: ContinuousOn_obs
Proof state before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
hU : IsOpen U
hz₀ : z₀ ∈ U
⊢ ContinuousOn (obs z₀) (𝓗 U)
Tactic:
have e1 : z₀ ∈ {z₀} := mem_singleton _
Proof state after:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
hU : IsOpen U
hz₀ : z₀ ∈ U
e1 : z₀ ∈ {z₀}
⊢ ContinuousOn (obs z₀) (𝓗 U)
Theorem: ContinuousOn_obs
Proof state before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
hU : IsOpen U
hz₀ : z₀ ∈ U
e1 : z₀ ∈ {z₀}
⊢ ContinuousOn (obs z₀) (𝓗 U)
Tactic:
have e2 : {z₀} ∈ compacts U := ⟨singleton_subset_iff.2 hz₀, isCompact_singleton⟩
Proof state after:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
hU : IsOpen U
hz₀ : z₀ ∈ U
e1 : z₀ ∈ {z₀}
e2 : {z₀} ∈ compacts U
⊢ ContinuousOn (obs z₀) (𝓗 U)
Theorem: ContinuousOn_obs
Proof state before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
hU : IsOpen U
hz₀ : z₀ ∈ U
e1 : z₀ ∈ {z₀}
e2 : {z₀} ∈ compacts U
⊢ ContinuousOn (obs z₀) (𝓗 U)
Tactic:
apply continuous_norm.comp_continuousOn
Proof state after:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
hU : IsOpen U
hz₀ : z₀ ∈ U
e1 : z₀ ∈ {z₀}
e2 : {z₀} ∈ compacts U
⊢ ContinuousOn (fun x => deriv x z₀) (𝓗 U)
Theorem: ContinuousOn_obs
Proof state before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
hU : IsOpen U
hz₀ : z₀ ∈ U
e1 : z₀ ∈ {z₀}
e2 : {z₀} ∈ compacts U
⊢ ContinuousOn (fun x => deriv x z₀) (𝓗 U)
Tactic:
exact (UniformOnFun.uniformContinuous_eval_of_mem _ _ e1 e2).continuous.comp_continuousOn
  (ContinuousOn_uderiv hU)
Proof state after:
no goals
Theorem: main
Proof state before:
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Tactic:
obtain ⟨z₀, hz₀⟩ : U.Nonempty := good_domain.is_nonempty
Proof state after:
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Theorem: main
Proof state before:
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Tactic:
have hU : IsOpen U := good_domain.is_open
Proof state after:
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Theorem: main
Proof state before:
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Tactic:
have hU' : IsPreconnected U := good_domain.is_preconnected
Proof state after:
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Theorem: main
Proof state before:
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Tactic:
have h1 : ContinuousOn (obs z₀) (𝓙 U) := ((ContinuousOn_obs hU hz₀).mono (λ f hf => hf.1.1))
Proof state after:
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Theorem: main
Proof state before:
case intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Tactic:
obtain ⟨f, hf, hfg⟩ := IsCompact_𝓙.exists_forall_ge (𝓘_nonempty.mono 𝓘_subset_𝓙) h1
Proof state after:
case intro.intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Theorem: main
Proof state before:
case intro.intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Tactic:
have h7 : ¬ ∃ w, EqOn f (λ _ => w) U := by
  obtain ⟨g, hg⟩ : (𝓘 U).Nonempty := 𝓘_nonempty
  specialize hfg g (𝓘_subset_𝓙 hg)
  have := norm_pos_iff.1 ((norm_pos_iff.2 (deriv_ne_zero_of_inj hU hg.1.1 hg.2 hz₀)).trans_le hfg)
  contrapose! this
  obtain ⟨w, hw : EqOn f (λ _ => w) U⟩ := this
  simpa only [deriv_const'] using (hw.eventuallyEq_of_mem (hU.mem_nhds hz₀)).deriv_eq
Proof state after:
case intro.intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Theorem: main
Proof state before:
case intro.intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Tactic:
have h5 : f ∈ 𝓘 U := ⟨hf.1, hf.2.resolve_right h7⟩
Proof state after:
case intro.intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Theorem: main
Proof state before:
case intro.intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
⊢ ∃ f ∈ 𝓘 U, f '' U = ball 0 1
Tactic:
refine ⟨f, h5, ?_⟩
Proof state after:
case intro.intro.intro
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀✝ : ℂ
inst✝ : good_domain U
z₀ : ℂ
hz₀ : z₀ ∈ U
hU : IsOpen U
hU' : IsPreconnected U
h1 : ContinuousOn (obs z₀) (𝓙 U)
f : 𝓒 U
hf : f ∈ 𝓙 U
hfg : ∀ y ∈ 𝓙 U, obs z₀ y ≤ obs z₀ f
h7 : ¬∃ w, EqOn f (fun x => w) U
h5 : f ∈ 𝓘 U
⊢ f '' U = ball 0 1