-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem ChartedSpace.t1Space [T1Space H] : T1Space M

Proof state:
case pos.refine_1
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : T1Space H
x y : M
hxy : x ≠ y
hy : y ∈ (chartAt H x).source
⊢ IsOpen ((chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) y}ᶜ)

Tactic:
exact PartialHomeomorph.isOpen_inter_preimage _ isOpen_compl_singleton

Result:
no goals

Proof state:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : T1Space H
x y : M
hxy : x ≠ y
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U

Tactic:
by_cases hy : y ∈ (chartAt H x).source

Result:
case pos
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : T1Space H
x y : M
hxy : x ≠ y
hy : y ∈ (chartAt H x).source
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U

case neg
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : T1Space H
x y : M
hxy : x ≠ y
hy : y ∉ (chartAt H x).source
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U

Proof state:
case pos
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : T1Space H
x y : M
hxy : x ≠ y
hy : y ∈ (chartAt H x).source
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U

Tactic:
refine ⟨(chartAt H x).source ∩ (chartAt H x)⁻¹' ({chartAt H x y}ᶜ), ?_, ?_, by simp⟩

Result:
case pos.refine_1
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : T1Space H
x y : M
hxy : x ≠ y
hy : y ∈ (chartAt H x).source
⊢ IsOpen ((chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) y}ᶜ)

case pos.refine_2
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : T1Space H
x y : M
hxy : x ≠ y
hy : y ∈ (chartAt H x).source
⊢ x ∈ (chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) y}ᶜ

Proof state:
case pos.refine_2
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : T1Space H
x y : M
hxy : x ≠ y
hy : y ∈ (chartAt H x).source
⊢ x ∈ (chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) y}ᶜ

Tactic:
simp only [preimage_compl, mem_inter_iff, mem_chart_source, mem_compl_iff, mem_preimage,
  mem_singleton_iff, true_and]

Result:
case pos.refine_2
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : T1Space H
x y : M
hxy : x ≠ y
hy : y ∈ (chartAt H x).source
⊢ ¬↑(chartAt H x) x = ↑(chartAt H x) y

Proof state:
case pos.refine_2
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : T1Space H
x y : M
hxy : x ≠ y
hy : y ∈ (chartAt H x).source
⊢ ¬↑(chartAt H x) x = ↑(chartAt H x) y

Tactic:
exact (chartAt H x).injOn.ne (ChartedSpace.mem_chart_source x) hy hxy

Result:
no goals

Proof state:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : T1Space H
x y : M
hxy : x ≠ y
hy : y ∈ (chartAt H x).source
⊢ y ∉ (chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) y}ᶜ

Tactic:
simp

Result:
no goals

Proof state:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : T1Space H
⊢ T1Space M

Tactic:
apply t1Space_iff_exists_open.2 (fun x y hxy ↦ ?_)

Result:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : T1Space H
x y : M
hxy : x ≠ y
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U

Proof state:
case neg
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : T1Space H
x y : M
hxy : x ≠ y
hy : y ∉ (chartAt H x).source
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U

Tactic:
exact ⟨(chartAt H x).source, (chartAt H x).open_source, ChartedSpace.mem_chart_source x, hy⟩

Result:
no goals