internlm/Lean-Github huggingface dataset:
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Tactic:
cases' ga.eventually_constant_or_nhds_le_map_nhds with h h
Proof state after:
case inl
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h : ∀ᶠ (z_1 : ℂ) in 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) z) z), g z_1 = g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)

case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h : 𝓝 (g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)) ≤ Filter.map g (𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) z) z))
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
⊢ AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Tactic:
rw [← hg]
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
⊢ AnalyticAt ℂ (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
⊢ AnalyticAt ℂ (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Tactic:
exact n.holomorphicAt.2
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
Proof state before:
case inl
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h : ∀ᶠ (z_1 : ℂ) in 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) z) z), g z_1 = g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Tactic:
contrapose h
Proof state after:
case inl
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h : ¬𝓝 (f z) ≤ Filter.map f (𝓝 z)
⊢ ¬∀ᶠ (z_1 : ℂ) in 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) z) z), g z_1 = g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
Proof state before:
case inl
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h : ¬𝓝 (f z) ≤ Filter.map f (𝓝 z)
⊢ ¬∀ᶠ (z_1 : ℂ) in 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) z) z), g z_1 = g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Tactic:
clear h
Proof state after:
case inl
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ ¬∀ᶠ (z_1 : ℂ) in 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) z) z), g z_1 = g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
Proof state before:
case inl
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ ¬∀ᶠ (z_1 : ℂ) in 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) z) z), g z_1 = g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Tactic:
simp only [Filter.not_eventually]
Proof state after:
case inl
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ ∃ᶠ (x : ℂ) in 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) z) z), ¬g x = g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
Proof state before:
case inl
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ ∃ᶠ (x : ℂ) in 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) z) z), ¬g x = g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Tactic:
apply n.inCharts.nonconst.mp
Proof state after:
case inl
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) z) z),
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x)) ≠
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z))) →
      ¬g x = g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
Proof state before:
case inl
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) z) z),
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x)) ≠
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z))) →
      ¬g x = g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Tactic:
simp only [← hg, Ne, imp_self, Filter.eventually_true]
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
Proof state before:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h : 𝓝 (g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)) ≤ Filter.map g (𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) z) z))
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Tactic:
simp only [← extChartAt_map_nhds' I z, Filter.map_map] at h
Proof state after:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h : 𝓝 (g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)) ≤ Filter.map (g ∘ ↑(extChartAt 𝓘(ℂ, ℂ) z)) (𝓝 z)
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
Proof state before:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h : 𝓝 (g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)) ≤ Filter.map (g ∘ ↑(extChartAt 𝓘(ℂ, ℂ) z)) (𝓝 z)
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Tactic:
replace h := @Filter.map_mono _ _ (extChartAt I (f z)).symm _ _ h
Proof state after:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  Filter.map (↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm) (𝓝 (g (↑(extChartAt 𝓘(ℂ, ℂ) z) z))) ≤
    Filter.map (↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm) (Filter.map (g ∘ ↑(extChartAt 𝓘(ℂ, ℂ) z)) (𝓝 z))
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
Proof state before:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  Filter.map (↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm) (𝓝 (g (↑(extChartAt 𝓘(ℂ, ℂ) z) z))) ≤
    Filter.map (↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm) (Filter.map (g ∘ ↑(extChartAt 𝓘(ℂ, ℂ) z)) (𝓝 z))
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Tactic:
simp only [← hg] at h
Proof state after:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  Filter.map (↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm)
      (𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z))))) ≤
    Filter.map (↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm)
      (Filter.map
        ((fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) ∘ ↑(extChartAt 𝓘(ℂ, ℂ) z)) (𝓝 z))
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
Proof state before:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  Filter.map (↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm)
      (𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z))))) ≤
    Filter.map (↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm)
      (Filter.map
        ((fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) ∘ ↑(extChartAt 𝓘(ℂ, ℂ) z)) (𝓝 z))
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Tactic:
rw [PartialEquiv.left_inv _ (mem_extChartAt_source I z)] at h
Proof state after:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  Filter.map (↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm) (𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f z))) ≤
    Filter.map (↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm)
      (Filter.map
        ((fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) ∘ ↑(extChartAt 𝓘(ℂ, ℂ) z)) (𝓝 z))
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
Proof state before:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  Filter.map (↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm) (𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f z))) ≤
    Filter.map (↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm)
      (Filter.map
        ((fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) ∘ ↑(extChartAt 𝓘(ℂ, ℂ) z)) (𝓝 z))
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Tactic:
simp only [extChartAt_symm_map_nhds' I (f z), Filter.map_map, Function.comp] at h
Proof state after:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  𝓝 (f z) ≤
    Filter.map
      (fun x =>
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x)))))
      (𝓝 z)
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
Proof state before:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  𝓝 (f z) ≤
    Filter.map
      (fun x =>
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x)))))
      (𝓝 z)
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Tactic:
have e : (fun w ↦ (extChartAt I (f z)).symm
    (extChartAt I (f z) (f ((extChartAt I z).symm (extChartAt I z w))))) =ᶠ[𝓝 z] f := by
  apply ((isOpen_extChartAt_source I z).eventually_mem (mem_extChartAt_source I z)).mp
  apply (n.holomorphicAt.continuousAt.eventually_mem (extChartAt_source_mem_nhds I (f z))).mp
  refine eventually_of_forall fun w fm m ↦ ?_
  simp only [PartialEquiv.left_inv _ m, PartialEquiv.left_inv _ fm]
Proof state after:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  𝓝 (f z) ≤
    Filter.map
      (fun x =>
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x)))))
      (𝓝 z)
e :
  (𝓝 z).EventuallyEq
    (fun w =>
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
        (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) w)))))
    f
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
Proof state before:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h :
  𝓝 (f z) ≤
    Filter.map
      (fun x =>
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x)))))
      (𝓝 z)
e :
  (𝓝 z).EventuallyEq
    (fun w =>
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
        (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) w)))))
    f
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Tactic:
rw [Filter.map_congr e] at h
Proof state after:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h : 𝓝 (f z) ≤ Filter.map f (𝓝 z)
e :
  (𝓝 z).EventuallyEq
    (fun w =>
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
        (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) w)))))
    f
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
Proof state before:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : S → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
h : 𝓝 (f z) ≤ Filter.map f (𝓝 z)
e :
  (𝓝 z).EventuallyEq
    (fun w =>
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
        (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) w)))))
    f
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Tactic:
exact h
Proof state after:
no goals