Theorem: RiemannSphere.holomorphicAt_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 : ℂ
fa : AnalyticAt ℂ f z
⊢ HolomorphicAt I I (lift f y) ↑z
Tactic:
rw [lift_eq_fill]
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 : ℂ
fa : AnalyticAt ℂ f z
⊢ HolomorphicAt I I (fill (fun z => ↑(f z)) y) ↑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 : ℂ
fa : AnalyticAt ℂ f z
⊢ HolomorphicAt I I (fill (fun z => ↑(f z)) y) ↑z
Tactic:
exact holomorphicAt_fill_coe ((holomorphic_coe _).comp (fa.holomorphicAt I I))
State after:
no goals