H : Type u
H' : Type ?u.45851
M : Type u_1
M' : Type ?u.45857
M'' : Type ?u.45860
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyConnectedSpace H
e : M → LocalHomeomorph M H := chartAt H
⊢ LocallyConnectedSpace M
H : Type u
H' : Type ?u.45851
M : Type u_1
M' : Type ?u.45857
M'' : Type ?u.45860
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyConnectedSpace H
⊢ LocallyConnectedSpace M
let e : M → LocalHomeomorph M H := chartAt H
case refine'_1
H : Type u
H' : Type ?u.45851
M : Type u_1
M' : Type ?u.45857
M'' : Type ?u.45860
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyConnectedSpace H
e : M → LocalHomeomorph M H := chartAt H
⊢ ∀ (x : M),
    HasBasis (𝓝 x) ((fun x s => (IsOpen s ∧ ↑(e x) x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) x)
      ((fun x s => ↑(LocalHomeomorph.symm (e x)) '' s) x)

case refine'_2
H : Type u
H' : Type ?u.45851
M : Type u_1
M' : Type ?u.45857
M'' : Type ?u.45860
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyConnectedSpace H
e : M → LocalHomeomorph M H := chartAt H
⊢ ∀ (x : M) (i : Set H),
    (fun x s => (IsOpen s ∧ ↑(e x) x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) x i →
      IsPreconnected ((fun x s => ↑(LocalHomeomorph.symm (e x)) '' s) x i)
H : Type u
H' : Type ?u.45851
M : Type u_1
M' : Type ?u.45857
M'' : Type ?u.45860
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyConnectedSpace H
e : M → LocalHomeomorph M H := chartAt H
⊢ LocallyConnectedSpace M
refine' locallyConnectedSpace_of_connected_bases (fun x s ↦ (e x).symm '' s)
    (fun x s ↦ (IsOpen s ∧ e x x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) _ _
case refine'_1
H : Type u
H' : Type ?u.45851
M : Type u_1
M' : Type ?u.45857
M'' : Type ?u.45860
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyConnectedSpace H
e : M → LocalHomeomorph M H := chartAt H
x : M
⊢ HasBasis (𝓝 x) ((fun x s => (IsOpen s ∧ ↑(e x) x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) x)
    ((fun x s => ↑(LocalHomeomorph.symm (e x)) '' s) x)
case refine'_1
H : Type u
H' : Type ?u.45851
M : Type u_1
M' : Type ?u.45857
M'' : Type ?u.45860
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyConnectedSpace H
e : M → LocalHomeomorph M H := chartAt H
⊢ ∀ (x : M),
    HasBasis (𝓝 x) ((fun x s => (IsOpen s ∧ ↑(e x) x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) x)
      ((fun x s => ↑(LocalHomeomorph.symm (e x)) '' s) x)
intro x
no goals
case refine'_1
H : Type u
H' : Type ?u.45851
M : Type u_1
M' : Type ?u.45857
M'' : Type ?u.45860
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyConnectedSpace H
e : M → LocalHomeomorph M H := chartAt H
x : M
⊢ HasBasis (𝓝 x) ((fun x s => (IsOpen s ∧ ↑(e x) x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) x)
    ((fun x s => ↑(LocalHomeomorph.symm (e x)) '' s) x)
simpa only [LocalHomeomorph.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
case refine'_2.intro.intro.intro
H : Type u
H' : Type ?u.45851
M : Type u_1
M' : Type ?u.45857
M'' : Type ?u.45860
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyConnectedSpace H
e : M → LocalHomeomorph M H := chartAt H
x : M
s : Set H
hssubset : s ⊆ (e x).target
hsconn : IsConnected s
⊢ IsPreconnected ((fun x s => ↑(LocalHomeomorph.symm (e x)) '' s) x s)
case refine'_2
H : Type u
H' : Type ?u.45851
M : Type u_1
M' : Type ?u.45857
M'' : Type ?u.45860
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyConnectedSpace H
e : M → LocalHomeomorph M H := chartAt H
⊢ ∀ (x : M) (i : Set H),
    (fun x s => (IsOpen s ∧ ↑(e x) x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) x i →
      IsPreconnected ((fun x s => ↑(LocalHomeomorph.symm (e x)) '' s) x i)
rintro x s ⟨⟨-, -, hsconn⟩, hssubset⟩
no goals
case refine'_2.intro.intro.intro
H : Type u
H' : Type ?u.45851
M : Type u_1
M' : Type ?u.45857
M'' : Type ?u.45860
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyConnectedSpace H
e : M → LocalHomeomorph M H := chartAt H
x : M
s : Set H
hssubset : s ⊆ (e x).target
hsconn : IsConnected s
⊢ IsPreconnected ((fun x s => ↑(LocalHomeomorph.symm (e x)) '' s) x s)
exact hsconn.isPreconnected.image _ ((e x).continuousOn_symm.mono hssubset)