Theorem: RiemannSphere.prod_nhds_eq (Ray/AnalyticManifold/RiemannSphere.lean)

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
x : X
z : ℂ
⊢ 𝓝 (x, ↑z) = Filter.map (fun p => (p.1, ↑p.2)) (𝓝 (x, z))
Tactic:
refine le_antisymm ?_ (continuousAt_fst.prod (continuous_coe.continuousAt.comp continuousAt_snd))
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
x : X
z : ℂ
⊢ 𝓝 (x, ↑z) ≤ Filter.map (fun p => (p.1, ↑p.2)) (𝓝 (x, z))

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
x : X
z : ℂ
⊢ 𝓝 (x, ↑z) ≤ Filter.map (fun p => (p.1, ↑p.2)) (𝓝 (x, z))
Tactic:
apply IsOpenMap.nhds_le
State after:
case hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
x : X
z : ℂ
⊢ IsOpenMap fun p => (p.1, ↑p.2)

State before:
case hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
x : X
z : ℂ
⊢ IsOpenMap fun p => (p.1, ↑p.2)
Tactic:
exact IsOpenMap.id.prod isOpenMap_coe
State after:
no goals