-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem ChartedSpace.discreteTopology [DiscreteTopology H] : DiscreteTopology M

Proof state:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : DiscreteTopology H
x : M
this : IsOpen ((chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) x})
⊢ {x} ⊆ (chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) x}

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✝ : DiscreteTopology H
x : M
this : IsOpen ((chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) x})
⊢ IsOpen {x}

Tactic:
convert this

Result:
case h.e'_3
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : DiscreteTopology H
x : M
this : IsOpen ((chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) x})
⊢ {x} = (chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) x}

Proof state:
case h.e'_3
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : DiscreteTopology H
x : M
this : IsOpen ((chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) x})
⊢ (chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) x} ⊆ {x}

Tactic:
simp only [subset_singleton_iff, mem_inter_iff, mem_preimage, mem_singleton_iff, and_imp]

Result:
case h.e'_3
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : DiscreteTopology H
x : M
this : IsOpen ((chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) x})
⊢ ∀ y ∈ (chartAt H x).source, ↑(chartAt H x) y = ↑(chartAt H x) x → y = x

Proof state:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : DiscreteTopology H
x : M
⊢ IsOpen {x}

Tactic:
have : IsOpen ((chartAt H x).source ∩ (chartAt H x) ⁻¹' {chartAt H x x}) :=
  isOpen_inter_preimage _ (isOpen_discrete _)

Result:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : DiscreteTopology H
x : M
this : IsOpen ((chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) x})
⊢ IsOpen {x}

Proof state:
case h.e'_3
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : DiscreteTopology H
x : M
this : IsOpen ((chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) x})
⊢ {x} = (chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) x}

Tactic:
refine Subset.antisymm (by simp) ?_

Result:
case h.e'_3
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : DiscreteTopology H
x : M
this : IsOpen ((chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) x})
⊢ (chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) x} ⊆ {x}

Proof state:
case h.e'_3
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : DiscreteTopology H
x : M
this : IsOpen ((chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) x})
⊢ ∀ y ∈ (chartAt H x).source, ↑(chartAt H x) y = ↑(chartAt H x) x → y = x

Tactic:
intro y hy h'y

Result:
case h.e'_3
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : DiscreteTopology H
x : M
this : IsOpen ((chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) x})
y : M
hy : y ∈ (chartAt H x).source
h'y : ↑(chartAt H x) y = ↑(chartAt H x) x
⊢ y = x

Proof state:
case h.e'_3
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : DiscreteTopology H
x : M
this : IsOpen ((chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) x})
y : M
hy : y ∈ (chartAt H x).source
h'y : ↑(chartAt H x) y = ↑(chartAt H x) x
⊢ y = x

Tactic:
exact (chartAt H x).injOn hy (mem_chart_source _ x) h'y

Result:
no goals

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

Tactic:
apply singletons_open_iff_discrete.1 (fun x ↦ ?_)

Result:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : DiscreteTopology H
x : M
⊢ IsOpen {x}