Theorem: RiemannSphere.holomorphic_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
⊢ Holomorphic I I fun z => ↑z
Tactic:
rw [holomorphic_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
⊢ (Continuous fun z => ↑z) ∧
    ∀ (x : ℂ), AnalyticAt ℂ (↑(extChartAt I ↑x) ∘ (fun z => ↑z) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
⊢ (Continuous fun z => ↑z) ∧
    ∀ (x : ℂ), AnalyticAt ℂ (↑(extChartAt I ↑x) ∘ (fun z => ↑z) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)
Tactic:
use continuous_coe
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
⊢ ∀ (x : ℂ), AnalyticAt ℂ (↑(extChartAt I ↑x) ∘ (fun z => ↑z) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)

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
⊢ ∀ (x : ℂ), AnalyticAt ℂ (↑(extChartAt I ↑x) ∘ (fun z => ↑z) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)
Tactic:
intro z
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) ∘ (fun z => ↑z) ∘ ↑(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) ∘ (fun z => ↑z) ∘ ↑(extChartAt I z).symm) (↑(extChartAt I z) z)
Tactic:
simp only [extChartAt_coe, extChartAt_eq_refl, PartialEquiv.refl_symm, PartialEquiv.refl_coe,
  Function.comp_id, id_eq, Function.comp, PartialEquiv.invFun_as_coe]
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 => ↑coePartialEquiv.symm ↑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 => ↑coePartialEquiv.symm ↑x) z
Tactic:
rw [← PartialEquiv.invFun_as_coe]
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 => coePartialEquiv.invFun ↑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 => coePartialEquiv.invFun ↑x) z
Tactic:
simp only [coePartialEquiv, toComplex_coe]
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