Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds (Ray/AnalyticManifold/OpenMapping.lean)

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
⊢ 𝓝 (f z) = Filter.map f (𝓝 z)
Tactic:
refine le_antisymm ?_ n.holomorphicAt.continuousAt
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
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)

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
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Tactic:
generalize hg : (fun x ↦ extChartAt I (f z) (f ((extChartAt I z).symm x))) = g
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
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)

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
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Tactic:
have ga : AnalyticAt ℂ g (extChartAt I z z) := by rw [← hg]; exact n.holomorphicAt.2
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
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)

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
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)

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]
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)

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
State after:
no goals

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
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)

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
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)

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]
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)

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
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)

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]
State after:
no goals

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
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)

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
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)

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
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)

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
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)

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
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)

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]
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)

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
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)

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
State after:
no goals

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)
h :
  𝓝 (f z) ≤
    Filter.map
      (fun x =>
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x)))))
      (𝓝 z)
⊢ (𝓝 z).EventuallyEq
    (fun w =>
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
        (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) w)))))
    f
Tactic:
apply ((isOpen_extChartAt_source I z).eventually_mem (mem_extChartAt_source I z)).mp
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
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)
⊢ ∀ᶠ (x : S) in 𝓝 z,
    x ∈ (extChartAt 𝓘(ℂ, ℂ) z).source →
      (fun w =>
            ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
              (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) w)))))
          x =
        f x

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)
h :
  𝓝 (f z) ≤
    Filter.map
      (fun x =>
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x)))))
      (𝓝 z)
⊢ ∀ᶠ (x : S) in 𝓝 z,
    x ∈ (extChartAt 𝓘(ℂ, ℂ) z).source →
      (fun w =>
            ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
              (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) w)))))
          x =
        f x
Tactic:
apply (n.holomorphicAt.continuousAt.eventually_mem (extChartAt_source_mem_nhds I (f z))).mp
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
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)
⊢ ∀ᶠ (x : S) in 𝓝 z,
    f x ∈ (extChartAt 𝓘(ℂ, ℂ) (f z)).source →
      x ∈ (extChartAt 𝓘(ℂ, ℂ) z).source →
        (fun w =>
              ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
                (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) w)))))
            x =
          f x

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)
h :
  𝓝 (f z) ≤
    Filter.map
      (fun x =>
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x)))))
      (𝓝 z)
⊢ ∀ᶠ (x : S) in 𝓝 z,
    f x ∈ (extChartAt 𝓘(ℂ, ℂ) (f z)).source →
      x ∈ (extChartAt 𝓘(ℂ, ℂ) z).source →
        (fun w =>
              ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
                (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) w)))))
            x =
          f x
Tactic:
refine eventually_of_forall fun w fm m ↦ ?_
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
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)
w : S
fm : f w ∈ (extChartAt 𝓘(ℂ, ℂ) (f z)).source
m : w ∈ (extChartAt 𝓘(ℂ, ℂ) z).source
⊢ (fun w =>
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) w)))))
      w =
    f w

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)
h :
  𝓝 (f z) ≤
    Filter.map
      (fun x =>
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x)))))
      (𝓝 z)
w : S
fm : f w ∈ (extChartAt 𝓘(ℂ, ℂ) (f z)).source
m : w ∈ (extChartAt 𝓘(ℂ, ℂ) z).source
⊢ (fun w =>
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) w)))))
      w =
    f w
Tactic:
simp only [PartialEquiv.left_inv _ m, PartialEquiv.left_inv _ fm]
State after:
no goals