internlm/Lean-Github huggingface dataset:
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right.hc.refine_2.hfg
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 : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ x ∈ {0}ᶜ, f x⁻¹ = if x = 0 then y else f x⁻¹

case right.hc.refine_2.hf
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 : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ Tendsto (fun z => f z⁻¹) (𝓝[≠] 0) (𝓝 (if True then y else f 0⁻¹))
Tactic:
intro z z0
Proof state after:
case right.hc.refine_2.hfg
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 : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
z0 : z ∈ {0}ᶜ
⊢ f z⁻¹ = if z = 0 then y else f z⁻¹

case right.hc.refine_2.hf
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 : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ Tendsto (fun z => f z⁻¹) (𝓝[≠] 0) (𝓝 (if True then y else f 0⁻¹))
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right.hc.refine_2.hfg
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 : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
z0 : z ∈ {0}ᶜ
⊢ f z⁻¹ = if z = 0 then y else f z⁻¹

case right.hc.refine_2.hf
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 : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ Tendsto (fun z => f z⁻¹) (𝓝[≠] 0) (𝓝 (if True then y else f 0⁻¹))
Tactic:
simp only [Set.mem_compl_iff, Set.mem_singleton_iff] at z0
Proof state after:
case right.hc.refine_2.hfg
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 : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
z0 : ¬z = 0
⊢ f z⁻¹ = if z = 0 then y else f z⁻¹

case right.hc.refine_2.hf
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 : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ Tendsto (fun z => f z⁻¹) (𝓝[≠] 0) (𝓝 (if True then y else f 0⁻¹))
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right.hc.refine_2.hfg
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 : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
z0 : ¬z = 0
⊢ f z⁻¹ = if z = 0 then y else f z⁻¹

case right.hc.refine_2.hf
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 : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ Tendsto (fun z => f z⁻¹) (𝓝[≠] 0) (𝓝 (if True then y else f 0⁻¹))
Tactic:
simp only [z0, if_false]
Proof state after:
case right.hc.refine_2.hf
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 : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ Tendsto (fun z => f z⁻¹) (𝓝[≠] 0) (𝓝 (if True then y else f 0⁻¹))
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right.hc.refine_2.hf
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 : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ Tendsto (fun z => f z⁻¹) (𝓝[≠] 0) (𝓝 (if True then y else f 0⁻¹))
Tactic:
exact Filter.Tendsto.comp fi inv_tendsto_atInf
Proof state after:
no goals
Theorem: RiemannSphere.holomorphic_fill
Proof 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 : ℂ → T
y : T
fa : Holomorphic I I f
fi : Tendsto f atInf (𝓝 y)
⊢ Holomorphic I I (fill f y)
Tactic:
intro z
Proof 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✝ : ℂ
f : ℂ → T
y : T
fa : Holomorphic I I f
fi : Tendsto f atInf (𝓝 y)
z : 𝕊
⊢ HolomorphicAt I I (fill f y) z
Theorem: RiemannSphere.holomorphic_fill
Proof 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 : ℂ → T
y : T
fa : Holomorphic I I f
fi : Tendsto f atInf (𝓝 y)
z : 𝕊
⊢ HolomorphicAt I I (fill f y) z
Tactic:
induction z using OnePoint.rec
Proof 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 : ℂ
f : ℂ → T
y : T
fa : Holomorphic I I f
fi : Tendsto f atInf (𝓝 y)
⊢ HolomorphicAt I I (fill f y) ∞

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 : ℂ
f : ℂ → T
y : T
fa : Holomorphic I I f
fi : Tendsto f atInf (𝓝 y)
x✝ : ℂ
⊢ HolomorphicAt I I (fill f y) ↑x✝
Theorem: RiemannSphere.holomorphic_fill
Proof 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 : ℂ
f : ℂ → T
y : T
fa : Holomorphic I I f
fi : Tendsto f atInf (𝓝 y)
⊢ HolomorphicAt I I (fill f y) ∞
Tactic:
exact holomorphicAt_fill_inf (eventually_of_forall fa) fi
Proof state after:
no goals
Theorem: RiemannSphere.holomorphic_fill
Proof 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 : ℂ
f : ℂ → T
y : T
fa : Holomorphic I I f
fi : Tendsto f atInf (𝓝 y)
x✝ : ℂ
⊢ HolomorphicAt I I (fill f y) ↑x✝
Tactic:
exact holomorphicAt_fill_coe (fa _)
Proof state after:
no goals
Theorem: RiemannSphere.continuousAt_lift_coe'
Proof 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 : ℂ
gc : ContinuousAt (uncurry g) (x, z)
⊢ ContinuousAt (uncurry (lift' g y)) (x, ↑z)
Tactic:
simp only [lift', ContinuousAt, uncurry, rec_coe, OnePoint.nhds_coe_eq, prod_nhds_eq,
  Filter.tendsto_map'_iff, Function.comp]
Proof 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 : ℂ
gc : ContinuousAt (uncurry g) (x, z)
⊢ Tendsto (fun x => ↑(g x.1 x.2)) (𝓝 (x, z)) (Filter.map OnePoint.some (𝓝 (g x z)))
Theorem: RiemannSphere.continuousAt_lift_coe'
Proof 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 : ℂ
gc : ContinuousAt (uncurry g) (x, z)
⊢ Tendsto (fun x => ↑(g x.1 x.2)) (𝓝 (x, z)) (Filter.map OnePoint.some (𝓝 (g x z)))
Tactic:
exact Filter.Tendsto.comp Filter.tendsto_map gc
Proof state after:
no goals
Theorem: RiemannSphere.continuousAt_lift_inf'
Proof 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 : ℂ
gi : Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
⊢ ContinuousAt (uncurry (lift' g ∞)) (x, ∞)
Tactic:
simp only [ContinuousAt, Filter.Tendsto, Filter.le_def, Filter.mem_map]
Proof 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 : ℂ
gi : Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
⊢ ∀ x_1 ∈ 𝓝 (uncurry (lift' g ∞) (x, ∞)), uncurry (lift' g ∞) ⁻¹' x_1 ∈ 𝓝 (x, ∞)
Theorem: RiemannSphere.continuousAt_lift_inf'
Proof 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 : ℂ
gi : Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
⊢ ∀ x_1 ∈ 𝓝 (uncurry (lift' g ∞) (x, ∞)), uncurry (lift' g ∞) ⁻¹' x_1 ∈ 𝓝 (x, ∞)
Tactic:
intro s m
Proof 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 : ℂ
gi : Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
s : Set 𝕊
m : s ∈ 𝓝 (uncurry (lift' g ∞) (x, ∞))
⊢ uncurry (lift' g ∞) ⁻¹' s ∈ 𝓝 (x, ∞)
Theorem: RiemannSphere.continuousAt_lift_inf'
Proof 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 : ℂ
gi : Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
s : Set 𝕊
m : s ∈ 𝓝 (uncurry (lift' g ∞) (x, ∞))
⊢ uncurry (lift' g ∞) ⁻¹' s ∈ 𝓝 (x, ∞)
Tactic:
simp only [OnePoint.nhds_infty_eq, Filter.coclosedCompact_eq_cocompact, Filter.mem_sup,
  Filter.mem_map, Filter.mem_pure, ← atInf_eq_cocompact, lift', rec_inf, uncurry] at m
Proof 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 : ℂ
gi : Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
s : Set 𝕊
m : OnePoint.some ⁻¹' s ∈ atInf ∧ ∞ ∈ s
⊢ uncurry (lift' g ∞) ⁻¹' s ∈ 𝓝 (x, ∞)
Theorem: RiemannSphere.continuousAt_lift_inf'
Proof 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 : ℂ
gi : Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
s : Set 𝕊
m : OnePoint.some ⁻¹' s ∈ atInf ∧ ∞ ∈ s
⊢ uncurry (lift' g ∞) ⁻¹' s ∈ 𝓝 (x, ∞)
Tactic:
simp only [true_imp_iff, mem_setOf, uncurry, Tendsto] at gi
Proof 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 : ℂ
gi : Filter.map (uncurry g) ((𝓝 x).prod atInf) ≤ atInf
s : Set 𝕊
m : OnePoint.some ⁻¹' s ∈ atInf ∧ ∞ ∈ s
⊢ uncurry (lift' g ∞) ⁻¹' s ∈ 𝓝 (x, ∞)
Theorem: RiemannSphere.continuousAt_lift_inf'
Proof 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 : ℂ
gi : Filter.map (uncurry g) ((𝓝 x).prod atInf) ≤ atInf
s : Set 𝕊
m : OnePoint.some ⁻¹' s ∈ atInf ∧ ∞ ∈ s
⊢ uncurry (lift' g ∞) ⁻¹' s ∈ 𝓝 (x, ∞)
Tactic:
specialize gi m.1
Proof 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 : ℂ
s : Set 𝕊
m : OnePoint.some ⁻¹' s ∈ atInf ∧ ∞ ∈ s
gi : OnePoint.some ⁻¹' s ∈ Filter.map (uncurry g) ((𝓝 x).prod atInf)
⊢ uncurry (lift' g ∞) ⁻¹' s ∈ 𝓝 (x, ∞)
Theorem: RiemannSphere.continuousAt_lift_inf'
Proof 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 : ℂ
s : Set 𝕊
m : OnePoint.some ⁻¹' s ∈ atInf ∧ ∞ ∈ s
gi : OnePoint.some ⁻¹' s ∈ Filter.map (uncurry g) ((𝓝 x).prod atInf)
⊢ uncurry (lift' g ∞) ⁻¹' s ∈ 𝓝 (x, ∞)
Tactic:
simp only [Filter.mem_map, preimage_preimage] at gi
Proof 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 : ℂ
s : Set 𝕊
m : OnePoint.some ⁻¹' s ∈ atInf ∧ ∞ ∈ s
gi : (fun x => ↑(uncurry g x)) ⁻¹' s ∈ (𝓝 x).prod atInf
⊢ uncurry (lift' g ∞) ⁻¹' s ∈ 𝓝 (x, ∞)
Theorem: RiemannSphere.continuousAt_lift_inf'
Proof 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 : ℂ
s : Set 𝕊
m : OnePoint.some ⁻¹' s ∈ atInf ∧ ∞ ∈ s
gi : (fun x => ↑(uncurry g x)) ⁻¹' s ∈ (𝓝 x).prod atInf
e : uncurry (lift' g ∞) ⁻¹' s = (fun x => (x.1, ↑x.2)) '' ((fun x => ↑(g x.1 x.2)) ⁻¹' s) ∪ univ ×ˢ {∞}
⊢ uncurry (lift' g ∞) ⁻¹' s ∈ 𝓝 (x, ∞)
Tactic:
rw [e]
Proof 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 : ℂ
s : Set 𝕊
m : OnePoint.some ⁻¹' s ∈ atInf ∧ ∞ ∈ s
gi : (fun x => ↑(uncurry g x)) ⁻¹' s ∈ (𝓝 x).prod atInf
e : uncurry (lift' g ∞) ⁻¹' s = (fun x => (x.1, ↑x.2)) '' ((fun x => ↑(g x.1 x.2)) ⁻¹' s) ∪ univ ×ˢ {∞}
⊢ (fun x => (x.1, ↑x.2)) '' ((fun x => ↑(g x.1 x.2)) ⁻¹' s) ∪ univ ×ˢ {∞} ∈ 𝓝 (x, ∞)
Theorem: RiemannSphere.continuousAt_lift_inf'
Proof 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 : ℂ
s : Set 𝕊
m : OnePoint.some ⁻¹' s ∈ atInf ∧ ∞ ∈ s
gi : (fun x => ↑(uncurry g x)) ⁻¹' s ∈ (𝓝 x).prod atInf
e : uncurry (lift' g ∞) ⁻¹' s = (fun x => (x.1, ↑x.2)) '' ((fun x => ↑(g x.1 x.2)) ⁻¹' s) ∪ univ ×ˢ {∞}
⊢ (fun x => (x.1, ↑x.2)) '' ((fun x => ↑(g x.1 x.2)) ⁻¹' s) ∪ univ ×ˢ {∞} ∈ 𝓝 (x, ∞)
Tactic:
exact prod_mem_inf_of_mem_atInf gi
Proof state after:
no goals
Theorem: RiemannSphere.continuousAt_lift_inf'
Proof 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 : ℂ
s : Set 𝕊
m : OnePoint.some ⁻¹' s ∈ atInf ∧ ∞ ∈ s
gi : (fun x => ↑(uncurry g x)) ⁻¹' s ∈ (𝓝 x).prod atInf
⊢ uncurry (lift' g ∞) ⁻¹' s = (fun x => (x.1, ↑x.2)) '' ((fun x => ↑(g x.1 x.2)) ⁻¹' s) ∪ univ ×ˢ {∞}
Tactic:
apply Set.ext
Proof 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 : ℂ
s : Set 𝕊
m : OnePoint.some ⁻¹' s ∈ atInf ∧ ∞ ∈ s
gi : (fun x => ↑(uncurry g x)) ⁻¹' s ∈ (𝓝 x).prod atInf
⊢ ∀ (x : X × 𝕊),
    x ∈ uncurry (lift' g ∞) ⁻¹' s ↔ x ∈ (fun x => (x.1, ↑x.2)) '' ((fun x => ↑(g x.1 x.2)) ⁻¹' s) ∪ univ ×ˢ {∞}
Theorem: RiemannSphere.continuousAt_lift_inf'
Proof 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 : ℂ
s : Set 𝕊
m : OnePoint.some ⁻¹' s ∈ atInf ∧ ∞ ∈ s
gi : (fun x => ↑(uncurry g x)) ⁻¹' s ∈ (𝓝 x).prod atInf
⊢ ∀ (x : X × 𝕊),
    x ∈ uncurry (lift' g ∞) ⁻¹' s ↔ x ∈ (fun x => (x.1, ↑x.2)) '' ((fun x => ↑(g x.1 x.2)) ⁻¹' s) ∪ univ ×ˢ {∞}
Tactic:
intro ⟨x, z⟩
Proof 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✝ : ℂ
s : Set 𝕊
m : OnePoint.some ⁻¹' s ∈ atInf ∧ ∞ ∈ s
gi : (fun x => ↑(uncurry g x)) ⁻¹' s ∈ (𝓝 x✝).prod atInf
x : X
z : 𝕊
⊢ (x, z) ∈ uncurry (lift' g ∞) ⁻¹' s ↔ (x, z) ∈ (fun x => (x.1, ↑x.2)) '' ((fun x => ↑(g x.1 x.2)) ⁻¹' s) ∪ univ ×ˢ {∞}
Theorem: RiemannSphere.continuousAt_lift_inf'
Proof 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✝ : ℂ
s : Set 𝕊
m : OnePoint.some ⁻¹' s ∈ atInf ∧ ∞ ∈ s
gi : (fun x => ↑(uncurry g x)) ⁻¹' s ∈ (𝓝 x✝).prod atInf
x : X
z : 𝕊
⊢ (x, z) ∈ uncurry (lift' g ∞) ⁻¹' s ↔ (x, z) ∈ (fun x => (x.1, ↑x.2)) '' ((fun x => ↑(g x.1 x.2)) ⁻¹' s) ∪ univ ×ˢ {∞}
Tactic:
induction z using OnePoint.rec
Proof state after:
case h.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 : ℂ
s : Set 𝕊
m : OnePoint.some ⁻¹' s ∈ atInf ∧ ∞ ∈ s
gi : (fun x => ↑(uncurry g x)) ⁻¹' s ∈ (𝓝 x✝).prod atInf
x : X
⊢ (x, ∞) ∈ uncurry (lift' g ∞) ⁻¹' s ↔ (x, ∞) ∈ (fun x => (x.1, ↑x.2)) '' ((fun x => ↑(g x.1 x.2)) ⁻¹' s) ∪ univ ×ˢ {∞}

case h.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 : ℂ
s : Set 𝕊
m : OnePoint.some ⁻¹' s ∈ atInf ∧ ∞ ∈ s
gi : (fun x => ↑(uncurry g x)) ⁻¹' s ∈ (𝓝 x✝¹).prod atInf
x : X
x✝ : ℂ
⊢ (x, ↑x✝) ∈ uncurry (lift' g ∞) ⁻¹' s ↔
    (x, ↑x✝) ∈ (fun x => (x.1, ↑x.2)) '' ((fun x => ↑(g x.1 x.2)) ⁻¹' s) ∪ univ ×ˢ {∞}
Theorem: RiemannSphere.continuousAt_lift_inf'
Proof state before:
case h.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 : ℂ
s : Set 𝕊
m : OnePoint.some ⁻¹' s ∈ atInf ∧ ∞ ∈ s
gi : (fun x => ↑(uncurry g x)) ⁻¹' s ∈ (𝓝 x✝).prod atInf
x : X
⊢ (x, ∞) ∈ uncurry (lift' g ∞) ⁻¹' s ↔ (x, ∞) ∈ (fun x => (x.1, ↑x.2)) '' ((fun x => ↑(g x.1 x.2)) ⁻¹' s) ∪ univ ×ˢ {∞}
Tactic:
simp only [mem_preimage, mem_image, mem_union, mem_prod_eq, mem_univ, true_and_iff,
  mem_singleton_iff, eq_self_iff_true, or_true_iff, iff_true_iff, uncurry, lift', rec_inf,
  m.2]
Proof state after:
no goals
Theorem: RiemannSphere.continuousAt_lift_inf'
Proof state before:
case h.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 : ℂ
s : Set 𝕊
m : OnePoint.some ⁻¹' s ∈ atInf ∧ ∞ ∈ s
gi : (fun x => ↑(uncurry g x)) ⁻¹' s ∈ (𝓝 x✝¹).prod atInf
x : X
x✝ : ℂ
⊢ (x, ↑x✝) ∈ uncurry (lift' g ∞) ⁻¹' s ↔
    (x, ↑x✝) ∈ (fun x => (x.1, ↑x.2)) '' ((fun x => ↑(g x.1 x.2)) ⁻¹' s) ∪ univ ×ˢ {∞}
Tactic:
simp only [uncurry, lift', mem_preimage, rec_coe, prod_singleton, image_univ, mem_union,
  mem_image, Prod.ext_iff, coe_eq_coe, Prod.exists, exists_eq_right_right, exists_eq_right,
  mem_range, OnePoint.infty_ne_coe, and_false, exists_false, or_false]
Proof state after:
no goals
Theorem: RiemannSphere.continuous_lift'
Proof 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 : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
⊢ Continuous (uncurry (lift' g ∞))
Tactic:
rw [continuous_iff_continuousOn_univ]
Proof 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 : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
⊢ ContinuousOn (uncurry (lift' g ∞)) univ
Theorem: RiemannSphere.continuous_lift'
Proof 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 : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
⊢ ContinuousOn (uncurry (lift' g ∞)) univ
Tactic:
intro ⟨x, z⟩ _
Proof 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✝ : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
x : X
z : 𝕊
a✝ : (x, z) ∈ univ
⊢ ContinuousWithinAt (uncurry (lift' g ∞)) univ (x, z)
Theorem: RiemannSphere.continuous_lift'
Proof 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✝ : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
x : X
z : 𝕊
a✝ : (x, z) ∈ univ
⊢ ContinuousWithinAt (uncurry (lift' g ∞)) univ (x, z)
Tactic:
apply ContinuousAt.continuousWithinAt
Proof 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✝ : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
x : X
z : 𝕊
a✝ : (x, z) ∈ univ
⊢ ContinuousAt (uncurry (lift' g ∞)) (x, z)