Theorem: RiemannSphere.holomorphicLift' (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 : ℂ
f : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
⊢ Holomorphic (I.prod I) I (uncurry (lift' f ∞))
Tactic:
apply osgoodManifold (continuous_lift' fa.continuous fi)
State after:
case f0
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 : ℂ
f : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
⊢ ∀ (x : ℂ) (y : 𝕊), HolomorphicAt I I (fun x => uncurry (lift' f ∞) (x, y)) x

case f1
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 : ℂ
f : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
⊢ ∀ (x : ℂ) (y : 𝕊), HolomorphicAt I I (fun y => uncurry (lift' f ∞) (x, y)) y

State before:
case f0
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 : ℂ
f : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
⊢ ∀ (x : ℂ) (y : 𝕊), HolomorphicAt I I (fun x => uncurry (lift' f ∞) (x, y)) x
Tactic:
intro x z
State after:
case f0
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✝ : ℂ
f : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
x : ℂ
z : 𝕊
⊢ HolomorphicAt I I (fun x => uncurry (lift' f ∞) (x, z)) x

State before:
case f0
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✝ : ℂ
f : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
x : ℂ
z : 𝕊
⊢ HolomorphicAt I I (fun x => uncurry (lift' f ∞) (x, z)) x
Tactic:
induction z using OnePoint.rec
State after:
case f0.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 : ℂ
f : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
x : ℂ
⊢ HolomorphicAt I I (fun x => uncurry (lift' f ∞) (x, ∞)) x

case f0.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 : ℂ
f : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
x x✝ : ℂ
⊢ HolomorphicAt I I (fun x => uncurry (lift' f ∞) (x, ↑x✝)) x

State before:
case f0.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 : ℂ
f : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
x : ℂ
⊢ HolomorphicAt I I (fun x => uncurry (lift' f ∞) (x, ∞)) x
Tactic:
simp only [uncurry, lift_inf']
State after:
case f0.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 : ℂ
f : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
x : ℂ
⊢ HolomorphicAt I I (fun x => ∞) x

State before:
case f0.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 : ℂ
f : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
x : ℂ
⊢ HolomorphicAt I I (fun x => ∞) x
Tactic:
exact holomorphicAt_const
State after:
no goals

State before:
case f0.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 : ℂ
f : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
x x✝ : ℂ
⊢ HolomorphicAt I I (fun x => uncurry (lift' f ∞) (x, ↑x✝)) x
Tactic:
exact (holomorphic_coe _).comp ((fa _ (mem_univ ⟨_,_⟩)).along_fst.holomorphicAt _ _)
State after:
no goals

State before:
case f1
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 : ℂ
f : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
⊢ ∀ (x : ℂ) (y : 𝕊), HolomorphicAt I I (fun y => uncurry (lift' f ∞) (x, y)) y
Tactic:
intro x z
State after:
case f1
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✝ : ℂ
f : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
x : ℂ
z : 𝕊
⊢ HolomorphicAt I I (fun y => uncurry (lift' f ∞) (x, y)) z

State before:
case f1
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✝ : ℂ
f : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
x : ℂ
z : 𝕊
⊢ HolomorphicAt I I (fun y => uncurry (lift' f ∞) (x, y)) z
Tactic:
exact holomorphic_lift (fun _ _ ↦ (fa _ (mem_univ ⟨_,_⟩)).along_snd)
  ((fi x).comp (tendsto_const_nhds.prod_mk Filter.tendsto_id)) z
State after:
no goals