Theorem: RiemannSphere.holomorphicAt_lift_inf (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 : ∀ᶠ (z : ℂ) in atInf, AnalyticAt ℂ f z
fi : Tendsto f atInf atInf
⊢ HolomorphicAt I I (lift f ∞) ∞
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 : ∀ᶠ (z : ℂ) in atInf, AnalyticAt ℂ f z
fi : Tendsto f atInf atInf
⊢ HolomorphicAt I I (fill (fun z => ↑(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 : ∀ᶠ (z : ℂ) in atInf, AnalyticAt ℂ f z
fi : Tendsto f atInf atInf
⊢ HolomorphicAt I I (fill (fun z => ↑(f z)) ∞) ∞
Tactic:
apply holomorphicAt_fill_inf
State after:
case fa
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 : ∀ᶠ (z : ℂ) in atInf, AnalyticAt ℂ f z
fi : Tendsto f atInf atInf
⊢ ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I (fun z => ↑(f z)) z

case fi
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 : ∀ᶠ (z : ℂ) in atInf, AnalyticAt ℂ f z
fi : Tendsto f atInf atInf
⊢ Tendsto (fun z => ↑(f z)) atInf (𝓝 ∞)

State before:
case fa
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 : ∀ᶠ (z : ℂ) in atInf, AnalyticAt ℂ f z
fi : Tendsto f atInf atInf
⊢ ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I (fun z => ↑(f z)) z

case fi
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 : ∀ᶠ (z : ℂ) in atInf, AnalyticAt ℂ f z
fi : Tendsto f atInf atInf
⊢ Tendsto (fun z => ↑(f z)) atInf (𝓝 ∞)
Tactic:
exact fa.mp (eventually_of_forall fun z fa ↦ (holomorphic_coe _).comp (fa.holomorphicAt I I))
State after:
case fi
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 : ∀ᶠ (z : ℂ) in atInf, AnalyticAt ℂ f z
fi : Tendsto f atInf atInf
⊢ Tendsto (fun z => ↑(f z)) atInf (𝓝 ∞)

State before:
case fi
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 : ∀ᶠ (z : ℂ) in atInf, AnalyticAt ℂ f z
fi : Tendsto f atInf atInf
⊢ Tendsto (fun z => ↑(f z)) atInf (𝓝 ∞)
Tactic:
exact coe_tendsto_inf.comp fi
State after:
no goals