Theorem: ChartedSpace.t1Space (Ray/Misc/ChartedSpace.lean)

State before:
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
⊢ ∀ (x : M), IsClosed {x}
Tactic:
intro x
State after:
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x : M
⊢ IsClosed {x}

State before:
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x : M
⊢ IsClosed {x}
Tactic:
rw [←compl_compl ({x} : Set M)]
State after:
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x : M
⊢ IsClosed {x}ᶜᶜ

State before:
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x : M
⊢ IsClosed {x}ᶜᶜ
Tactic:
apply IsOpen.isClosed_compl
State after:
case a
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x : M
⊢ IsOpen {x}ᶜ

State before:
case a
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x : M
⊢ IsOpen {x}ᶜ
Tactic:
rw [isOpen_iff_mem_nhds]
State after:
case a
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x : M
⊢ ∀ x_1 ∈ {x}ᶜ, {x}ᶜ ∈ 𝓝 x_1

State before:
case a
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x : M
⊢ ∀ x_1 ∈ {x}ᶜ, {x}ᶜ ∈ 𝓝 x_1
Tactic:
intro y m
State after:
case a
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ∈ {x}ᶜ
⊢ {x}ᶜ ∈ 𝓝 y

State before:
case a
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ∈ {x}ᶜ
⊢ {x}ᶜ ∈ 𝓝 y
Tactic:
simp only [mem_compl_singleton_iff] at m
State after:
case a
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
⊢ {x}ᶜ ∈ 𝓝 y

State before:
case a
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
⊢ {x}ᶜ ∈ 𝓝 y
Tactic:
simp only [mem_nhds_iff, subset_compl_singleton_iff]
State after:
case a
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
⊢ ∃ t, x ∉ t ∧ IsOpen t ∧ y ∈ t

State before:
case a
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
⊢ ∃ t, x ∉ t ∧ IsOpen t ∧ y ∈ t
Tactic:
by_cases xm : x ∈ (chartAt A y).source
State after:
case pos
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
⊢ ∃ t, x ∉ t ∧ IsOpen t ∧ y ∈ t

case neg
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∉ (_root_.chartAt A y).source
⊢ ∃ t, x ∉ t ∧ IsOpen t ∧ y ∈ t

State before:
case pos
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
⊢ ∃ t, x ∉ t ∧ IsOpen t ∧ y ∈ t
Tactic:
set t := (chartAt A y).source \ {x}
State after:
case pos
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
⊢ ∃ t, x ∉ t ∧ IsOpen t ∧ y ∈ t

State before:
case pos
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
⊢ ∃ t, x ∉ t ∧ IsOpen t ∧ y ∈ t
Tactic:
have e : t = (chartAt A y).source ∩ chartAt A y ⁻¹'
    ((chartAt A y).target \ {chartAt A y x}) := by
  apply Set.ext; intro z
  simp only [mem_diff, mem_singleton_iff, mem_inter_iff, mem_preimage]; constructor
  intro ⟨zm, zx⟩; use zm, PartialEquiv.map_source _ zm, (PartialEquiv.injOn _).ne zm xm zx
  intro ⟨zm, _, zx⟩; use zm, ((PartialEquiv.injOn _).ne_iff zm xm).mp zx
State after:
case pos
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
e :
  t = (_root_.chartAt A y).source ∩ ↑(_root_.chartAt A y) ⁻¹' ((_root_.chartAt A y).target \ {↑(_root_.chartAt A y) x})
⊢ ∃ t, x ∉ t ∧ IsOpen t ∧ y ∈ t

State before:
case pos
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
e :
  t = (_root_.chartAt A y).source ∩ ↑(_root_.chartAt A y) ⁻¹' ((_root_.chartAt A y).target \ {↑(_root_.chartAt A y) x})
⊢ ∃ t, x ∉ t ∧ IsOpen t ∧ y ∈ t
Tactic:
use t
State after:
case h
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
e :
  t = (_root_.chartAt A y).source ∩ ↑(_root_.chartAt A y) ⁻¹' ((_root_.chartAt A y).target \ {↑(_root_.chartAt A y) x})
⊢ x ∉ t ∧ IsOpen t ∧ y ∈ t

State before:
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
⊢ t = (_root_.chartAt A y).source ∩ ↑(_root_.chartAt A y) ⁻¹' ((_root_.chartAt A y).target \ {↑(_root_.chartAt A y) x})
Tactic:
apply Set.ext
State after:
case h
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
⊢ ∀ (x_1 : M),
    x_1 ∈ t ↔
      x_1 ∈
        (_root_.chartAt A y).source ∩
          ↑(_root_.chartAt A y) ⁻¹' ((_root_.chartAt A y).target \ {↑(_root_.chartAt A y) x})

State before:
case h
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
⊢ ∀ (x_1 : M),
    x_1 ∈ t ↔
      x_1 ∈
        (_root_.chartAt A y).source ∩
          ↑(_root_.chartAt A y) ⁻¹' ((_root_.chartAt A y).target \ {↑(_root_.chartAt A y) x})
Tactic:
intro z
State after:
case h
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ t ↔
    z ∈
      (_root_.chartAt A y).source ∩ ↑(_root_.chartAt A y) ⁻¹' ((_root_.chartAt A y).target \ {↑(_root_.chartAt A y) x})

State before:
case h
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ t ↔
    z ∈
      (_root_.chartAt A y).source ∩ ↑(_root_.chartAt A y) ⁻¹' ((_root_.chartAt A y).target \ {↑(_root_.chartAt A y) x})
Tactic:
simp only [mem_diff, mem_singleton_iff, mem_inter_iff, mem_preimage]
State after:
case h
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ t ↔
    z ∈ (_root_.chartAt A y).source ∧
      ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x

State before:
case h
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ t ↔
    z ∈ (_root_.chartAt A y).source ∧
      ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x
Tactic:
constructor
State after:
case h.mp
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ t →
    z ∈ (_root_.chartAt A y).source ∧
      ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x

case h.mpr
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ (_root_.chartAt A y).source ∧
      ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x →
    z ∈ t

State before:
case h.mp
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ t →
    z ∈ (_root_.chartAt A y).source ∧
      ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x

case h.mpr
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ (_root_.chartAt A y).source ∧
      ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x →
    z ∈ t
Tactic:
intro ⟨zm, zx⟩
State after:
case h.mp
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
zm : z ∈ (_root_.chartAt A y).source
zx : z ∉ {x}
⊢ z ∈ (_root_.chartAt A y).source ∧
    ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x

case h.mpr
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ (_root_.chartAt A y).source ∧
      ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x →
    z ∈ t

State before:
case h.mp
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
zm : z ∈ (_root_.chartAt A y).source
zx : z ∉ {x}
⊢ z ∈ (_root_.chartAt A y).source ∧
    ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x

case h.mpr
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ (_root_.chartAt A y).source ∧
      ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x →
    z ∈ t
Tactic:
use zm, PartialEquiv.map_source _ zm, (PartialEquiv.injOn _).ne zm xm zx
State after:
case h.mpr
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ (_root_.chartAt A y).source ∧
      ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x →
    z ∈ t

State before:
case h.mpr
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ (_root_.chartAt A y).source ∧
      ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x →
    z ∈ t
Tactic:
intro ⟨zm, _, zx⟩
State after:
case h.mpr
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
zm : z ∈ (_root_.chartAt A y).source
left✝ : ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target
zx : ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x
⊢ z ∈ t

State before:
case h.mpr
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
zm : z ∈ (_root_.chartAt A y).source
left✝ : ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target
zx : ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x
⊢ z ∈ t
Tactic:
use zm, ((PartialEquiv.injOn _).ne_iff zm xm).mp zx
State after:
no goals

State before:
case neg
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∉ (_root_.chartAt A y).source
⊢ ∃ t, x ∉ t ∧ IsOpen t ∧ y ∈ t
Tactic:
use(chartAt A y).source, xm, (chartAt A y).open_source, mem_chart_source A y
State after:
no goals