Theorem: RiemannSphere.isOpenMap_coe (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
⊢ IsOpenMap fun z => ↑z
Tactic:
intro s o
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 ℂ
o : IsOpen s
⊢ IsOpen ((fun z => ↑z) '' s)

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 ℂ
o : IsOpen s
⊢ IsOpen ((fun z => ↑z) '' s)
Tactic:
have e : (fun z : ℂ ↦ (z : 𝕊)) '' s = {∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s := by
  apply Set.ext; intro z
  simp only [mem_image, mem_inter_iff, mem_compl_singleton_iff, mem_preimage]
  constructor
  intro ⟨x, m, e⟩; simp only [← e, toComplex_coe, m, and_true_iff]; exact inf_ne_coe.symm
  intro ⟨n, m⟩; use z.toComplex, m, coe_toComplex n
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 ℂ
o : IsOpen s
e : (fun z => ↑z) '' s = {∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s
⊢ IsOpen ((fun z => ↑z) '' s)

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 ℂ
o : IsOpen s
e : (fun z => ↑z) '' s = {∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s
⊢ IsOpen ((fun z => ↑z) '' s)
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
s : Set ℂ
o : IsOpen s
e : (fun z => ↑z) '' s = {∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s
⊢ IsOpen ({∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s)

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 ℂ
o : IsOpen s
e : (fun z => ↑z) '' s = {∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s
⊢ IsOpen ({∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s)
Tactic:
exact continuousOn_toComplex.isOpen_inter_preimage isOpen_compl_singleton o
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
s : Set ℂ
o : IsOpen s
⊢ (fun z => ↑z) '' s = {∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s
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
s : Set ℂ
o : IsOpen s
⊢ ∀ (x : 𝕊), x ∈ (fun z => ↑z) '' s ↔ x ∈ {∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s

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
s : Set ℂ
o : IsOpen s
⊢ ∀ (x : 𝕊), x ∈ (fun z => ↑z) '' s ↔ x ∈ {∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s
Tactic:
intro 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
s : Set ℂ
o : IsOpen s
z : 𝕊
⊢ z ∈ (fun z => ↑z) '' s ↔ z ∈ {∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s

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
s : Set ℂ
o : IsOpen s
z : 𝕊
⊢ z ∈ (fun z => ↑z) '' s ↔ z ∈ {∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s
Tactic:
simp only [mem_image, mem_inter_iff, mem_compl_singleton_iff, mem_preimage]
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
s : Set ℂ
o : IsOpen s
z : 𝕊
⊢ (∃ x ∈ s, ↑x = z) ↔ z ≠ ∞ ∧ z.toComplex ∈ s

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
s : Set ℂ
o : IsOpen s
z : 𝕊
⊢ (∃ x ∈ s, ↑x = z) ↔ z ≠ ∞ ∧ z.toComplex ∈ s
Tactic:
constructor
State after:
case h.mp
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 : 𝕊
⊢ (∃ x ∈ s, ↑x = z) → z ≠ ∞ ∧ z.toComplex ∈ s

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

State before:
case h.mp
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 : 𝕊
⊢ (∃ x ∈ s, ↑x = z) → z ≠ ∞ ∧ z.toComplex ∈ s

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 ⟨x, m, e⟩
State after:
case h.mp
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 : 𝕊
x : ℂ
m : x ∈ s
e : ↑x = z
⊢ z ≠ ∞ ∧ z.toComplex ∈ s

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

State before:
case h.mp
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 : 𝕊
x : ℂ
m : x ∈ s
e : ↑x = z
⊢ z ≠ ∞ ∧ z.toComplex ∈ s

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:
simp only [← e, toComplex_coe, m, and_true_iff]
State after:
case h.mp
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 : 𝕊
x : ℂ
m : x ∈ s
e : ↑x = z
⊢ ↑x ≠ ∞

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

State before:
case h.mp
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 : 𝕊
x : ℂ
m : x ∈ s
e : ↑x = z
⊢ ↑x ≠ ∞

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:
exact inf_ne_coe.symm
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 : 𝕊
⊢ z ≠ ∞ ∧ z.toComplex ∈ s → ∃ x ∈ s, ↑x = z

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

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