awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocallyConnectedSpace H
e : M → OpenPartialHomeomorph M H := chartAt H
x : M
⊢ Filter.HasBasis.{u_2, u + 1} (ι := Set H) (𝓝 x)
    ((fun (x : M) (s : Set H) ↦ (IsOpen[inst] s ∧ (↑(e x) : M → H) x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) x)
    ((fun (x : M) (s : Set H) ↦ (↑(e x).symm : H → M) '' s) x)

Tactic:
simpa only [e, OpenPartialHomeomorph.symm_map_nhds_eq, mem_chart_source] using
      ((LocallyConnectedSpace.open_connected_basis (e x x)).restrict_subset
        ((e x).open_target.mem_nhds (mem_chart_target H x))).map (e x).symm

Premises used: OpenPartialHomeomorph.symm_map_nhds_eq, mem_chart_source, OpenPartialHomeomorph.toFun', Filter.HasBasis.map, Filter.HasBasis.restrict_subset, IsOpen.mem_nhds, LocallyConnectedSpace.open_connected_basis, OpenPartialHomeomorph.open_target, mem_chart_target, OpenPartialHomeomorph.symm
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocallyConnectedSpace H
e : M → OpenPartialHomeomorph M H := chartAt H
x : M
s : Set H
hssubset : s ⊆ (e x).target
hsconn : IsConnected s
⊢ IsPreconnected.{u_2} (α := M) ((fun (x : M) (s : Set H) ↦ (↑(e x).symm : H → M) '' s) x s)

Tactic:
hsconn.isPreconnected.image _ ((e x).continuousOn_symm.mono hssubset)

Premises used: IsPreconnected.image, IsConnected.isPreconnected, ContinuousOn.mono, OpenPartialHomeomorph.continuousOn_symm
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocallyConnectedSpace H
e : M → OpenPartialHomeomorph M H := chartAt H
x : M
s : Set H
hssubset : s ⊆ (e x).target
hsconn : IsConnected s
⊢ IsPreconnected.{u_2} (α := M) ((fun (x : M) (s : Set H) ↦ (↑(e x).symm : H → M) '' s) x s)

Tactic:
exact hsconn.isPreconnected.image _ ((e x).continuousOn_symm.mono hssubset)

Premises used: IsPreconnected.image, IsConnected.isPreconnected, ContinuousOn.mono, OpenPartialHomeomorph.continuousOn_symm
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
⊢ LocPathConnectedSpace M

Tactic:
⟨fun x ↦ ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨u, hu⟩ ↦ Filter.mem_of_superset hu.1.1 hu.2⟩⟩⟩

Premises used: Membership.mem, nhds, LocPathConnectedSpace.mk, And.right, And.left, Filter.HasBasis.mk, Iff.intro, _private.0.ChartedSpace.locPathConnectedSpace.match_1, Filter.mem_of_superset
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
refine : ∀ (x : M) (s : Set M) (hs : s ∈ 𝓝 x), ∃ (i : Set M), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
⊢ LocPathConnectedSpace M

Tactic:
refine ⟨fun x ↦ ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨u, hu⟩ ↦ Filter.mem_of_superset hu.1.1 hu.2⟩⟩⟩
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
⊢ t ∈ 𝓝 x

Tactic:
have ht : t ∈ 𝓝 x := Filter.inter_mem hs (chart_source_mem_nhds _ _)
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ ∃ (i : Set M), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
⟨e.symm '' pathComponentIn (e '' t) (e x), ⟨?_, ?_⟩, (?_ : _ ⊆ t).trans inter_subset_left⟩

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, OpenPartialHomeomorph.toFun', pathComponentIn, And.intro, Exists.intro, Set.image, OpenPartialHomeomorph.symm
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
refine_1 : (↑e.symm : H → M) '' pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x) ∈ 𝓝 x
refine_2 : IsPathConnected ((↑e.symm : H → M) '' pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x))
refine_3 : id ((↑e.symm : H → M) '' pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x)) ⊆ t
⊢ ∃ (i : Set M), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
refine ⟨e.symm '' pathComponentIn (e '' t) (e x), ⟨?_, ?_⟩, (?_ : _ ⊆ t).trans inter_subset_left⟩
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
refine_1 :
  (↑e.symm : H → M) '' pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x) ∈ 𝓝 ((↑e.symm : H → M) ((↑e : M → H) x))
⊢ (↑e.symm : H → M) '' pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x) ∈ 𝓝 x

Tactic:
nth_rewrite 1 [← e.left_inv (mem_chart_source _ _)]

Premises used: mem_chart_source, OpenPartialHomeomorph.left_inv
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ (↑e : M → H) x ∈ e.symm.source

Tactic:
simp [e]
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
refine_1 : pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x) ∈ 𝓝 ((↑e : M → H) x)
⊢ (↑e.symm : H → M) '' pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x) ∈ 𝓝 ((↑e.symm : H → M) ((↑e : M → H) x))

Tactic:
apply e.symm.image_mem_nhds (by simp [e])

Premises used: OpenPartialHomeomorph.image_mem_nhds, OpenPartialHomeomorph.symm
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x) ∈ 𝓝 ((↑e : M → H) x)

Tactic:
pathComponentIn_mem_nhds <| e.image_mem_nhds (mem_chart_source _ _) ht

Premises used: mem_chart_source, OpenPartialHomeomorph.image_mem_nhds, pathComponentIn_mem_nhds
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x) ∈ 𝓝 ((↑e : M → H) x)

Tactic:
exact pathComponentIn_mem_nhds <| e.image_mem_nhds (mem_chart_source _ _) ht

Premises used: mem_chart_source, OpenPartialHomeomorph.image_mem_nhds, pathComponentIn_mem_nhds
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ IsPathConnected ((↑e.symm : H → M) '' pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x))

Tactic:
(isPathConnected_pathComponentIn <| mem_image_of_mem e (mem_of_mem_nhds ht)).image' ?_

Premises used: OpenPartialHomeomorph.toFun', mem_of_mem_nhds, isPathConnected_pathComponentIn, Set.mem_image_of_mem, IsPathConnected.image'
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
refine_2 : ContinuousOn (↑e.symm : H → M) (pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x))
⊢ IsPathConnected ((↑e.symm : H → M) '' pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x))

Tactic:
refine (isPathConnected_pathComponentIn <| mem_image_of_mem e (mem_of_mem_nhds ht)).image' ?_

Premises used: OpenPartialHomeomorph.toFun', mem_of_mem_nhds, isPathConnected_pathComponentIn, Set.mem_image_of_mem, IsPathConnected.image'
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ ContinuousOn (↑e.symm : H → M) (pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x))

Tactic:
e.continuousOn_symm.mono <| subset_trans ?_ e.map_source''

Premises used: subset_trans, ContinuousOn.mono, OpenPartialHomeomorph.map_source'', OpenPartialHomeomorph.continuousOn_symm
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
refine_2 : pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x) ⊆ (↑e : M → H) '' e.source
⊢ ContinuousOn (↑e.symm : H → M) (pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x))

Tactic:
refine e.continuousOn_symm.mono <| subset_trans ?_ e.map_source''

Premises used: subset_trans, ContinuousOn.mono, OpenPartialHomeomorph.map_source'', OpenPartialHomeomorph.continuousOn_symm
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x) ⊆ (↑e : M → H) '' e.source

Tactic:
(pathComponentIn_mono <| image_mono inter_subset_right).trans pathComponentIn_subset

Premises used: Set.image_mono, HasSubset.Subset.trans, pathComponentIn_mono, pathComponentIn_subset, Set.inter_subset_right
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x) ⊆ (↑e : M → H) '' e.source

Tactic:
exact (pathComponentIn_mono <| image_mono inter_subset_right).trans pathComponentIn_subset

Premises used: Set.image_mono, HasSubset.Subset.trans, pathComponentIn_mono, pathComponentIn_subset, Set.inter_subset_right
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ id ((↑e.symm : H → M) '' pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x)) ⊆ t

Tactic:
(image_mono pathComponentIn_subset).trans
      (PartialEquiv.symm_image_image_of_subset_source _ inter_subset_right).subset

Premises used: Set.image_mono, setOf, HasSubset.Subset.trans, Eq.subset, Set.image, PartialEquiv.symm_image_image_of_subset_source, pathComponentIn_subset, Set.inter_subset_right
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ id ((↑e.symm : H → M) '' pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x)) ⊆ t

Tactic:
exact (image_mono pathComponentIn_subset).trans
      (PartialEquiv.symm_image_image_of_subset_source _ inter_subset_right).subset

Premises used: Set.image_mono, HasSubset.Subset.trans, Eq.subset, PartialEquiv.symm_image_image_of_subset_source, pathComponentIn_subset, Set.inter_subset_right
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H_1 : Type u
H'_1 : Type u_1
M_1 : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H_1
inst_1 : TopologicalSpace M_1
inst_2 : ChartedSpace H_1 M_1
H : Type u_5
inst_3 : TopologicalSpace H
H' : Type u_6
inst_4 : TopologicalSpace H'
M : Type u_7
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H H'
inst_7 : ChartedSpace H' M
p : M
⊢ p ∈ (toPartialEquiv (chartAt H' p ≫ₕ chartAt H ((↑(chartAt H' p) : M → H') p))).source

Tactic:
simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u_5
inst : TopologicalSpace H
H' : Type u_6
inst_1 : TopologicalSpace H'
M : Type u_7
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H H'
inst_4 : ChartedSpace H' M
x : M
⊢ Eq (α := OpenPartialHomeomorph M H) (chartAt H x) (chartAt H' x ≫ₕ chartAt H ((↑(chartAt H' x) : M → H') x))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : T1Space H
apply : ∀ (x y : M) (hxy : x ≠ y), ∃ (U : Set M), IsOpen[inst_1] U ∧ x ∈ U ∧ y ∉ U
⊢ T1Space M

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

Premises used: Iff.mpr, t1Space_iff_exists_open
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : T1Space H
x y : M
hxy : x ≠ y
pos : ∀ (hy : y ∈ (toPartialEquiv (chartAt H x)).source), ∃ (U : Set M), IsOpen[inst_1] U ∧ x ∈ U ∧ y ∉ U
neg : ∀ (hy : y ∉ (toPartialEquiv (chartAt H x)).source), ∃ (U : Set M), IsOpen[inst_1] U ∧ x ∈ U ∧ y ∉ U
⊢ ∃ (U : Set M), IsOpen[inst_1] U ∧ x ∈ U ∧ y ∉ U

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

Premises used: chartAt, PartialEquiv.source, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : T1Space H
x y : M
hxy : x ≠ y
hy : y ∈ (toPartialEquiv (chartAt H x)).source
⊢ y ∉ (toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) y}ᶜ

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : T1Space H
x y : M
hxy : x ≠ y
hy : y ∈ (toPartialEquiv (chartAt H x)).source
pos :
  IsOpen[inst_1] ((toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) y}ᶜ)
pos₁ : x ∈ (toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) y}ᶜ
⊢ ∃ (U : Set M), IsOpen[inst_1] U ∧ x ∈ U ∧ y ∉ U

Tactic:
refine ⟨(chartAt H x).source ∩ (chartAt H x)⁻¹' ({chartAt H x y}ᶜ), ?_, ?_, by simp⟩
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : T1Space H
x y : M
hxy : x ≠ y
hy : y ∈ (toPartialEquiv (chartAt H x)).source
⊢ IsOpen[inst_1] ((toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) y}ᶜ)

Tactic:
OpenPartialHomeomorph.isOpen_inter_preimage _ isOpen_compl_singleton

Premises used: isOpen_compl_singleton, OpenPartialHomeomorph.isOpen_inter_preimage
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : T1Space H
x y : M
hxy : x ≠ y
hy : y ∈ (toPartialEquiv (chartAt H x)).source
⊢ IsOpen[inst_1] ((toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) y}ᶜ)

Tactic:
exact OpenPartialHomeomorph.isOpen_inter_preimage _ isOpen_compl_singleton

Premises used: isOpen_compl_singleton, OpenPartialHomeomorph.isOpen_inter_preimage
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : T1Space H
x y : M
hxy : x ≠ y
hy : y ∈ (toPartialEquiv (chartAt H x)).source
pos : ¬(↑(chartAt H x) : M → H) x = (↑(chartAt H x) : M → H) y
⊢ x ∈ (toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) y}ᶜ

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

Premises used: mem_chart_source, Set.mem_inter_iff, Set.mem_singleton_iff, Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, true_and
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : T1Space H
x y : M
hxy : x ≠ y
hy : y ∈ (toPartialEquiv (chartAt H x)).source
⊢ ¬(↑(chartAt H x) : M → H) x = (↑(chartAt H x) : M → H) y

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

Premises used: chartAt, ChartedSpace.mem_chart_source, OpenPartialHomeomorph.injOn, Set.InjOn.ne
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : T1Space H
x y : M
hxy : x ≠ y
hy : y ∈ (toPartialEquiv (chartAt H x)).source
⊢ ¬(↑(chartAt H x) : M → H) x = (↑(chartAt H x) : M → H) y

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

Premises used: chartAt, ChartedSpace.mem_chart_source, OpenPartialHomeomorph.injOn, Set.InjOn.ne
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : T1Space H
x y : M
hxy : x ≠ y
hy : y ∉ (toPartialEquiv (chartAt H x)).source
⊢ ∃ (U : Set M), IsOpen[inst_1] U ∧ x ∈ U ∧ y ∉ U

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

Premises used: chartAt, OpenPartialHomeomorph.open_source, ChartedSpace.mem_chart_source, And.intro, Exists.intro, PartialEquiv.source, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : T1Space H
x y : M
hxy : x ≠ y
hy : y ∉ (toPartialEquiv (chartAt H x)).source
⊢ ∃ (U : Set M), IsOpen[inst_1] U ∧ x ∈ U ∧ y ∉ U

Tactic:
exact ⟨(chartAt H x).source, (chartAt H x).open_source, ChartedSpace.mem_chart_source x, hy⟩
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : DiscreteTopology H
apply : ∀ (x : M), IsOpen[inst_1] {x}
⊢ DiscreteTopology M

Tactic:
apply discreteTopology_iff_isOpen_singleton.2 (fun x ↦ ?_)

Premises used: Iff.mpr, discreteTopology_iff_isOpen_singleton
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : DiscreteTopology H
x : M
⊢ IsOpen[inst_1] ((toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x})

Tactic:
have : IsOpen ((chartAt H x).source ∩ (chartAt H x) ⁻¹' {chartAt H x x}) :=
    isOpen_inter_preimage _ (isOpen_discrete _)
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : DiscreteTopology H
x : M
this :
  IsOpen[inst_1] ((toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x})
⊢ IsOpen[inst_1] ((toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x})

Tactic:
this
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : DiscreteTopology H
x : M
this :
  IsOpen[inst_1] ((toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x})
h : {x} = (toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x}
⊢ IsOpen[inst_1] {x}

Tactic:
convert! this
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : DiscreteTopology H
x : M
this :
  IsOpen[inst_1] ((toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x})
⊢ {x} ⊆ (toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x}

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : DiscreteTopology H
x : M
this :
  IsOpen[inst_1] ((toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x})
h : (toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x} ⊆ {x}
⊢ {x} = (toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x}

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

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : DiscreteTopology H
x : M
this :
  IsOpen[inst_1] ((toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x})
h : ∀ y ∈ (toPartialEquiv (chartAt H x)).source, (↑(chartAt H x) : M → H) y = (↑(chartAt H x) : M → H) x → y = x
⊢ (toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x} ⊆ {x}

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

Premises used: Set.subset_singleton_iff, and_imp, Set.mem_inter_iff, Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : DiscreteTopology H
x : M
this :
  IsOpen[inst_1] ((toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x})
y : M
hy : y ∈ (toPartialEquiv (chartAt H x)).source
h'y : (↑(chartAt H x) : M → H) y = (↑(chartAt H x) : M → H) x
⊢ y = x

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

Premises used: mem_chart_source, chartAt, OpenPartialHomeomorph.injOn
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : DiscreteTopology H
x : M
this :
  IsOpen[inst_1] ((toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x})
y : M
hy : y ∈ (toPartialEquiv (chartAt H x)).source
h'y : (↑(chartAt H x) : M → H) y = (↑(chartAt H x) : M → H) x
⊢ y = x

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

Premises used: mem_chart_source, chartAt, OpenPartialHomeomorph.injOn