Theorem: RiemannSphere.prod_mem_inf_of_mem_atInf (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
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⟩
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, ∞)

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]
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 ×ˢ 𝓝 ∞

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,
  ?_⟩
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 ×ˢ {∞}

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⟩
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 ×ˢ {∞}

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 ⊢
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 = ∞

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
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 = ∞

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]
State after:
no goals

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 ⊢
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

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⟩
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

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⟩
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

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]
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

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
State after:
no goals