Theorem: RiemannSphere.holomorphicAt_toComplex (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
z : ℂ
⊢ HolomorphicAt I I OnePoint.toComplex ↑z
Tactic:
rw [holomorphicAt_iff]
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ ContinuousAt OnePoint.toComplex ↑z ∧
    AnalyticAt ℂ (↑(extChartAt I (↑z).toComplex) ∘ OnePoint.toComplex ∘ ↑(extChartAt I ↑z).symm) (↑(extChartAt I ↑z) ↑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
z : ℂ
⊢ ContinuousAt OnePoint.toComplex ↑z ∧
    AnalyticAt ℂ (↑(extChartAt I (↑z).toComplex) ∘ OnePoint.toComplex ∘ ↑(extChartAt I ↑z).symm) (↑(extChartAt I ↑z) ↑z)
Tactic:
use continuousAt_toComplex
State after:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (↑(extChartAt I (↑z).toComplex) ∘ OnePoint.toComplex ∘ ↑(extChartAt I ↑z).symm) (↑(extChartAt I ↑z) ↑z)

State before:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (↑(extChartAt I (↑z).toComplex) ∘ OnePoint.toComplex ∘ ↑(extChartAt I ↑z).symm) (↑(extChartAt I ↑z) ↑z)
Tactic:
simp only [toComplex_coe, Function.comp, extChartAt_coe, extChartAt_eq_refl, PartialEquiv.refl_coe,
  id, PartialEquiv.symm_symm, coePartialEquiv_apply, coePartialEquiv_symm_apply]
State after:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (fun x => x) z

State before:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (fun x => x) z
Tactic:
apply analyticAt_id
State after:
no goals