-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem ChartedSpace.locPathConnectedSpace [LocPathConnectedSpace H] : LocPathConnectedSpace M

Proof state:
case refine_1
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ ↑e.symm '' pathComponentIn (↑e x) (↑e '' t) ∈ 𝓝 x

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

Result:
case refine_1
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ ↑e.symm '' pathComponentIn (↑e x) (↑e '' t) ∈ 𝓝 (↑e.symm (↑e x))

Proof state:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ ↑e x ∈ e.symm.source

Tactic:
simp [e]

Result:
no goals

Proof state:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

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

Result:
case refine_1
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ ↑e.symm '' pathComponentIn (↑e x) (↑e '' t) ∈ 𝓝 x

case refine_2
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ IsPathConnected (↑e.symm '' pathComponentIn (↑e x) (↑e '' t))

case refine_3
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ id (↑e.symm '' pathComponentIn (↑e x) (↑e '' t)) ⊆ t

Proof state:
case refine_1
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ ↑e.symm '' pathComponentIn (↑e x) (↑e '' t) ∈ 𝓝 (↑e.symm (↑e x))

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

Result:
case refine_1
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ pathComponentIn (↑e x) (↑e '' t) ∈ 𝓝 (↑e x)

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

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

Result:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Proof state:
case refine_2
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ pathComponentIn (↑e x) (↑e '' t) ⊆ ↑e '' e.source

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

Result:
no goals

Proof state:
case refine_1
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ pathComponentIn (↑e x) (↑e '' t) ∈ 𝓝 (↑e x)

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

Result:
no goals

Proof state:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
have ht : t ∈ 𝓝 x := Filter.inter_mem hs (chart_source_mem_nhds _ _)

Result:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Proof state:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
let t := s ∩ e.source

Result:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Proof state:
case refine_2
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ ContinuousOn (↑e.symm) (pathComponentIn (↑e x) (↑e '' t))

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

Result:
case refine_2
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ pathComponentIn (↑e x) (↑e '' t) ⊆ ↑e '' e.source

Proof state:
case refine_3
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ id (↑e.symm '' pathComponentIn (↑e x) (↑e '' t)) ⊆ t

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

Result:
no goals

Proof state:
case refine_2
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ IsPathConnected (↑e.symm '' pathComponentIn (↑e x) (↑e '' t))

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

Result:
case refine_2
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : PartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ ContinuousOn (↑e.symm) (pathComponentIn (↑e x) (↑e '' t))