Theorem: RiemannSphere.continuousAt_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 : ℂ
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]
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, ∞)

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
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, ∞)

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
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, ∞)

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
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, ∞)

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
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, ∞)

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
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, ∞)

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]
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, ∞)

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

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

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

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

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

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