internlm/Lean-Github huggingface dataset:
Theorem: RiemannSphere.isOpenMap_coe
Proof state before:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
z : 𝕊
⊢ z ≠ ∞ ∧ z.toComplex ∈ s → ∃ x ∈ s, ↑x = z
Tactic:
intro ⟨n, m⟩
Proof state after:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
z : 𝕊
n : z ≠ ∞
m : z.toComplex ∈ s
⊢ ∃ x ∈ s, ↑x = z
Theorem: RiemannSphere.isOpenMap_coe
Proof state before:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
z : 𝕊
n : z ≠ ∞
m : z.toComplex ∈ s
⊢ ∃ x ∈ s, ↑x = z
Tactic:
use z.toComplex, m, coe_toComplex n
Proof state after:
no goals
Theorem: RiemannSphere.prod_nhds_eq
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
x : X
z : ℂ
⊢ 𝓝 (x, ↑z) = Filter.map (fun p => (p.1, ↑p.2)) (𝓝 (x, z))
Tactic:
refine le_antisymm ?_ (continuousAt_fst.prod (continuous_coe.continuousAt.comp continuousAt_snd))
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
x : X
z : ℂ
⊢ 𝓝 (x, ↑z) ≤ Filter.map (fun p => (p.1, ↑p.2)) (𝓝 (x, z))
Theorem: RiemannSphere.prod_nhds_eq
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
x : X
z : ℂ
⊢ 𝓝 (x, ↑z) ≤ Filter.map (fun p => (p.1, ↑p.2)) (𝓝 (x, z))
Tactic:
apply IsOpenMap.nhds_le
Proof state after:
case hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
x : X
z : ℂ
⊢ IsOpenMap fun p => (p.1, ↑p.2)
Theorem: RiemannSphere.prod_nhds_eq
Proof state before:
case hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
x : X
z : ℂ
⊢ IsOpenMap fun p => (p.1, ↑p.2)
Tactic:
exact IsOpenMap.id.prod isOpenMap_coe
Proof state after:
no goals
Theorem: RiemannSphere.mem_inf_of_mem_atInf
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
s : Set ℂ
f : s ∈ atInf
⊢ (fun z => ↑z) '' s ∪ {∞} ∈ 𝓝 ∞
Tactic:
simp only [OnePoint.nhds_infty_eq, Filter.mem_sup, Filter.coclosedCompact_eq_cocompact, ←
  atInf_eq_cocompact, 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
s : Set ℂ
f : s ∈ atInf
⊢ OnePoint.some ⁻¹' ((fun z => ↑z) '' s ∪ {∞}) ∈ atInf ∧ (fun z => ↑z) '' s ∪ {∞} ∈ pure ∞
Theorem: RiemannSphere.mem_inf_of_mem_atInf
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
s : Set ℂ
f : s ∈ atInf
⊢ OnePoint.some ⁻¹' ((fun z => ↑z) '' s ∪ {∞}) ∈ atInf ∧ (fun z => ↑z) '' s ∪ {∞} ∈ pure ∞
Tactic:
exact ⟨Filter.mem_of_superset f fun _ m ↦ Or.inl (mem_image_of_mem _ m), Or.inr rfl⟩
Proof state after:
no goals
Theorem: RiemannSphere.prod_mem_inf_of_mem_atInf
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
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
⊢ (fun p => (p.1, ↑p.2)) '' s ∪ univ ×ˢ {∞} ∈ 𝓝 (x, ∞)
Tactic:
rcases Filter.mem_prod_iff.mp f with ⟨t, tx, u, ui, sub⟩
Proof state after:
case intro.intro.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
⊢ (fun p => (p.1, ↑p.2)) '' s ∪ univ ×ˢ {∞} ∈ 𝓝 (x, ∞)
Theorem: RiemannSphere.prod_mem_inf_of_mem_atInf
Proof state before:
case intro.intro.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
⊢ (fun p => (p.1, ↑p.2)) '' s ∪ univ ×ˢ {∞} ∈ 𝓝 (x, ∞)
Tactic:
rw [nhds_prod_eq]
Proof state after:
case intro.intro.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
⊢ (fun p => (p.1, ↑p.2)) '' s ∪ univ ×ˢ {∞} ∈ 𝓝 x ×ˢ 𝓝 ∞
Theorem: RiemannSphere.prod_mem_inf_of_mem_atInf
Proof state before:
case intro.intro.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
⊢ (fun p => (p.1, ↑p.2)) '' s ∪ univ ×ˢ {∞} ∈ 𝓝 x ×ˢ 𝓝 ∞
Tactic:
refine Filter.mem_prod_iff.mpr ⟨t, tx, (fun z : ℂ ↦ (z : 𝕊)) '' u ∪ {∞}, mem_inf_of_mem_atInf ui,
  ?_⟩
Proof state after:
case intro.intro.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
⊢ t ×ˢ ((fun z => ↑z) '' u ∪ {∞}) ⊆ (fun p => (p.1, ↑p.2)) '' s ∪ univ ×ˢ {∞}
Theorem: RiemannSphere.prod_mem_inf_of_mem_atInf
Proof state before:
case intro.intro.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
⊢ t ×ˢ ((fun z => ↑z) '' u ∪ {∞}) ⊆ (fun p => (p.1, ↑p.2)) '' s ∪ univ ×ˢ {∞}
Tactic:
intro ⟨y, z⟩ ⟨yt, m⟩
Proof state after:
case intro.intro.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
y : X
z : 𝕊
yt : (y, z).1 ∈ t
m : (y, z).2 ∈ (fun z => ↑z) '' u ∪ {∞}
⊢ (y, z) ∈ (fun p => (p.1, ↑p.2)) '' s ∪ univ ×ˢ {∞}
Theorem: RiemannSphere.prod_mem_inf_of_mem_atInf
Proof state before:
case intro.intro.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
y : X
z : 𝕊
yt : (y, z).1 ∈ t
m : (y, z).2 ∈ (fun z => ↑z) '' u ∪ {∞}
⊢ (y, z) ∈ (fun p => (p.1, ↑p.2)) '' s ∪ univ ×ˢ {∞}
Tactic:
simp only [mem_prod_eq, mem_image, mem_union, mem_singleton_iff, mem_univ, true_and_iff,
  Prod.ext_iff] at yt m ⊢
Proof state after:
case intro.intro.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
y : X
z : 𝕊
yt : y ∈ t
m : (∃ x ∈ u, ↑x = z) ∨ z = ∞
⊢ (∃ x ∈ s, x.1 = y ∧ ↑x.2 = z) ∨ z = ∞
Theorem: RiemannSphere.prod_mem_inf_of_mem_atInf
Proof state before:
case intro.intro.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
y : X
z : 𝕊
yt : y ∈ t
m : (∃ x ∈ u, ↑x = z) ∨ z = ∞
⊢ (∃ x ∈ s, x.1 = y ∧ ↑x.2 = z) ∨ z = ∞
Tactic:
induction' z using OnePoint.rec with z
Proof state after:
case intro.intro.intro.intro.h₁
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
y : X
yt : y ∈ t
m : (∃ x ∈ u, ↑x = ∞) ∨ ∞ = ∞
⊢ (∃ x ∈ s, x.1 = y ∧ ↑x.2 = ∞) ∨ ∞ = ∞

case intro.intro.intro.intro.h₂
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
y : X
yt : y ∈ t
z : ℂ
m : (∃ x ∈ u, ↑x = ↑z) ∨ ↑z = ∞
⊢ (∃ x ∈ s, x.1 = y ∧ ↑x.2 = ↑z) ∨ ↑z = ∞
Theorem: RiemannSphere.prod_mem_inf_of_mem_atInf
Proof state before:
case intro.intro.intro.intro.h₁
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
y : X
yt : y ∈ t
m : (∃ x ∈ u, ↑x = ∞) ∨ ∞ = ∞
⊢ (∃ x ∈ s, x.1 = y ∧ ↑x.2 = ∞) ∨ ∞ = ∞
Tactic:
simp only [eq_self_iff_true, or_true_iff]
Proof state after:
no goals
Theorem: RiemannSphere.prod_mem_inf_of_mem_atInf
Proof state before:
case intro.intro.intro.intro.h₂
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
y : X
yt : y ∈ t
z : ℂ
m : (∃ x ∈ u, ↑x = ↑z) ∨ ↑z = ∞
⊢ (∃ x ∈ s, x.1 = y ∧ ↑x.2 = ↑z) ∨ ↑z = ∞
Tactic:
simp only [coe_eq_inf_iff, or_false_iff, coe_eq_coe] at m ⊢
Proof state after:
case intro.intro.intro.intro.h₂
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
y : X
yt : y ∈ t
z : ℂ
m : ∃ x ∈ u, x = z
⊢ ∃ x ∈ s, x.1 = y ∧ x.2 = z
Theorem: RiemannSphere.prod_mem_inf_of_mem_atInf
Proof state before:
case intro.intro.intro.intro.h₂
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
y : X
yt : y ∈ t
z : ℂ
m : ∃ x ∈ u, x = z
⊢ ∃ x ∈ s, x.1 = y ∧ x.2 = z
Tactic:
rcases m with ⟨w, wu, wz⟩
Proof state after:
case intro.intro.intro.intro.h₂.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
y : X
yt : y ∈ t
z w : ℂ
wu : w ∈ u
wz : w = z
⊢ ∃ x ∈ s, x.1 = y ∧ x.2 = z
Theorem: RiemannSphere.prod_mem_inf_of_mem_atInf
Proof state before:
case intro.intro.intro.intro.h₂.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
y : X
yt : y ∈ t
z w : ℂ
wu : w ∈ u
wz : w = z
⊢ ∃ x ∈ s, x.1 = y ∧ x.2 = z
Tactic:
refine ⟨⟨y, z⟩, sub (mk_mem_prod yt ?_), rfl, rfl⟩
Proof state after:
case intro.intro.intro.intro.h₂.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
y : X
yt : y ∈ t
z w : ℂ
wu : w ∈ u
wz : w = z
⊢ z ∈ u
Theorem: RiemannSphere.prod_mem_inf_of_mem_atInf
Proof state before:
case intro.intro.intro.intro.h₂.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
y : X
yt : y ∈ t
z w : ℂ
wu : w ∈ u
wz : w = z
⊢ z ∈ u
Tactic:
rw [← wz]
Proof state after:
case intro.intro.intro.intro.h₂.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
y : X
yt : y ∈ t
z w : ℂ
wu : w ∈ u
wz : w = z
⊢ w ∈ u
Theorem: RiemannSphere.prod_mem_inf_of_mem_atInf
Proof state before:
case intro.intro.intro.intro.h₂.intro.intro
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set (X × ℂ)
x : X
f : s ∈ (𝓝 x).prod atInf
t : Set X
tx : t ∈ 𝓝 x
u : Set ℂ
ui : u ∈ atInf
sub : t ×ˢ u ⊆ s
y : X
yt : y ∈ t
z w : ℂ
wu : w ∈ u
wz : w = z
⊢ w ∈ u
Tactic:
exact wu
Proof state after:
no goals
Theorem: RiemannSphere.holomorphic_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
⊢ Holomorphic I I fun z => ↑z
Tactic:
rw [holomorphic_iff]
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
⊢ (Continuous fun z => ↑z) ∧
    ∀ (x : ℂ), AnalyticAt ℂ (↑(extChartAt I ↑x) ∘ (fun z => ↑z) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)
Theorem: RiemannSphere.holomorphic_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
⊢ (Continuous fun z => ↑z) ∧
    ∀ (x : ℂ), AnalyticAt ℂ (↑(extChartAt I ↑x) ∘ (fun z => ↑z) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)
Tactic:
use continuous_coe
Proof state after:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
⊢ ∀ (x : ℂ), AnalyticAt ℂ (↑(extChartAt I ↑x) ∘ (fun z => ↑z) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)
Theorem: RiemannSphere.holomorphic_coe
Proof state before:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
⊢ ∀ (x : ℂ), AnalyticAt ℂ (↑(extChartAt I ↑x) ∘ (fun z => ↑z) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)
Tactic:
intro z
Proof state after:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (↑(extChartAt I ↑z) ∘ (fun z => ↑z) ∘ ↑(extChartAt I z).symm) (↑(extChartAt I z) z)
Theorem: RiemannSphere.holomorphic_coe
Proof state before:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (↑(extChartAt I ↑z) ∘ (fun z => ↑z) ∘ ↑(extChartAt I z).symm) (↑(extChartAt I z) z)
Tactic:
simp only [extChartAt_coe, extChartAt_eq_refl, PartialEquiv.refl_symm, PartialEquiv.refl_coe,
  Function.comp_id, id_eq, Function.comp, PartialEquiv.invFun_as_coe]
Proof state after:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (fun x => ↑coePartialEquiv.symm ↑x) z
Theorem: RiemannSphere.holomorphic_coe
Proof state before:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (fun x => ↑coePartialEquiv.symm ↑x) z
Tactic:
rw [← PartialEquiv.invFun_as_coe]
Proof state after:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (fun x => coePartialEquiv.invFun ↑x) z
Theorem: RiemannSphere.holomorphic_coe
Proof state before:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (fun x => coePartialEquiv.invFun ↑x) z
Tactic:
simp only [coePartialEquiv, toComplex_coe]
Proof state after:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (fun x => x) z
Theorem: RiemannSphere.holomorphic_coe
Proof state before:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (fun x => x) z
Tactic:
apply analyticAt_id
Proof state after:
no goals
Theorem: RiemannSphere.holomorphicAt_toComplex
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
z : ℂ
⊢ HolomorphicAt I I OnePoint.toComplex ↑z
Tactic:
rw [holomorphicAt_iff]
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
z : ℂ
⊢ ContinuousAt OnePoint.toComplex ↑z ∧
    AnalyticAt ℂ (↑(extChartAt I (↑z).toComplex) ∘ OnePoint.toComplex ∘ ↑(extChartAt I ↑z).symm) (↑(extChartAt I ↑z) ↑z)
Theorem: RiemannSphere.holomorphicAt_toComplex
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
z : ℂ
⊢ ContinuousAt OnePoint.toComplex ↑z ∧
    AnalyticAt ℂ (↑(extChartAt I (↑z).toComplex) ∘ OnePoint.toComplex ∘ ↑(extChartAt I ↑z).symm) (↑(extChartAt I ↑z) ↑z)
Tactic:
use continuousAt_toComplex
Proof state after:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (↑(extChartAt I (↑z).toComplex) ∘ OnePoint.toComplex ∘ ↑(extChartAt I ↑z).symm) (↑(extChartAt I ↑z) ↑z)
Theorem: RiemannSphere.holomorphicAt_toComplex
Proof state before:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (↑(extChartAt I (↑z).toComplex) ∘ OnePoint.toComplex ∘ ↑(extChartAt I ↑z).symm) (↑(extChartAt I ↑z) ↑z)
Tactic:
simp only [toComplex_coe, Function.comp, extChartAt_coe, extChartAt_eq_refl, PartialEquiv.refl_coe,
  id, PartialEquiv.symm_symm, coePartialEquiv_apply, coePartialEquiv_symm_apply]
Proof state after:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (fun x => x) z
Theorem: RiemannSphere.holomorphicAt_toComplex
Proof state before:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (fun x => x) z
Tactic:
apply analyticAt_id
Proof state after:
no goals
Theorem: RiemannSphere.holomorphic_inv
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
⊢ Holomorphic I I fun z => z⁻¹
Tactic:
rw [holomorphic_iff]
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
⊢ (Continuous fun z => z⁻¹) ∧
    ∀ (x : 𝕊), AnalyticAt ℂ (↑(extChartAt I x⁻¹) ∘ (fun z => z⁻¹) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)
Theorem: RiemannSphere.holomorphic_inv
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
⊢ (Continuous fun z => z⁻¹) ∧
    ∀ (x : 𝕊), AnalyticAt ℂ (↑(extChartAt I x⁻¹) ∘ (fun z => z⁻¹) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)
Tactic:
use continuous_inv
Proof state after:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
⊢ ∀ (x : 𝕊), AnalyticAt ℂ (↑(extChartAt I x⁻¹) ∘ (fun z => z⁻¹) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)
Theorem: RiemannSphere.holomorphic_inv
Proof state before:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
⊢ ∀ (x : 𝕊), AnalyticAt ℂ (↑(extChartAt I x⁻¹) ∘ (fun z => z⁻¹) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)
Tactic:
intro z
Proof state after:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : 𝕊
⊢ AnalyticAt ℂ (↑(extChartAt I z⁻¹) ∘ (fun z => z⁻¹) ∘ ↑(extChartAt I z).symm) (↑(extChartAt I z) z)
Theorem: RiemannSphere.holomorphic_inv
Proof state before:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : 𝕊
⊢ AnalyticAt ℂ (↑(extChartAt I z⁻¹) ∘ (fun z => z⁻¹) ∘ ↑(extChartAt I z).symm) (↑(extChartAt I z) z)
Tactic:
induction' z using OnePoint.rec with z
Proof state after:
case right.h₁
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
⊢ AnalyticAt ℂ (↑(extChartAt I ∞⁻¹) ∘ (fun z => z⁻¹) ∘ ↑(extChartAt I ∞).symm) (↑(extChartAt I ∞) ∞)

case right.h₂
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (↑(extChartAt I (↑z)⁻¹) ∘ (fun z => z⁻¹) ∘ ↑(extChartAt I ↑z).symm) (↑(extChartAt I ↑z) ↑z)