Theorem: RiemannSphere.continuousAt_lift_coe' (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
f : ℂ → ℂ
g : X → ℂ → ℂ
y : 𝕊
x : X
z : ℂ
gc : ContinuousAt (uncurry g) (x, z)
⊢ ContinuousAt (uncurry (lift' g y)) (x, ↑z)
Tactic:
simp only [lift', ContinuousAt, uncurry, rec_coe, OnePoint.nhds_coe_eq, prod_nhds_eq,
  Filter.tendsto_map'_iff, Function.comp]
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
g : X → ℂ → ℂ
y : 𝕊
x : X
z : ℂ
gc : ContinuousAt (uncurry g) (x, z)
⊢ Tendsto (fun x => ↑(g x.1 x.2)) (𝓝 (x, z)) (Filter.map OnePoint.some (𝓝 (g 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
f : ℂ → ℂ
g : X → ℂ → ℂ
y : 𝕊
x : X
z : ℂ
gc : ContinuousAt (uncurry g) (x, z)
⊢ Tendsto (fun x => ↑(g x.1 x.2)) (𝓝 (x, z)) (Filter.map OnePoint.some (𝓝 (g x z)))
Tactic:
exact Filter.Tendsto.comp Filter.tendsto_map gc
State after:
no goals