Theorem: RiemannSphere.holomorphic_lift (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 : AnalyticOn ℂ f univ
fi : Tendsto f atInf atInf
⊢ Holomorphic I I (lift f ∞)
Tactic:
intro z
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 : AnalyticOn ℂ f univ
fi : Tendsto f atInf atInf
z : 𝕊
⊢ HolomorphicAt I I (lift f ∞) 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 : AnalyticOn ℂ f univ
fi : Tendsto f atInf atInf
z : 𝕊
⊢ HolomorphicAt I I (lift f ∞) z
Tactic:
induction z using OnePoint.rec
State after:
case h₁
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 : AnalyticOn ℂ f univ
fi : Tendsto f atInf atInf
⊢ HolomorphicAt I I (lift f ∞) ∞

case h₂
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 : AnalyticOn ℂ f univ
fi : Tendsto f atInf atInf
x✝ : ℂ
⊢ HolomorphicAt I I (lift f ∞) ↑x✝

State before:
case h₁
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 : AnalyticOn ℂ f univ
fi : Tendsto f atInf atInf
⊢ HolomorphicAt I I (lift f ∞) ∞
Tactic:
exact holomorphicAt_lift_inf (eventually_of_forall fun z ↦ fa z (mem_univ _)) fi
State after:
no goals

State before:
case h₂
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 : AnalyticOn ℂ f univ
fi : Tendsto f atInf atInf
x✝ : ℂ
⊢ HolomorphicAt I I (lift f ∞) ↑x✝
Tactic:
exact holomorphicAt_lift_coe (fa _ (mem_univ _))
State after:
no goals