-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem ChartedSpace.locallyConnectedSpace [LocallyConnectedSpace H] : LocallyConnectedSpace M

Proof state:
case refine_1
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyConnectedSpace H
e : M → PartialHomeomorph M H := chartAt H
x : M
⊢ (𝓝 x).HasBasis ((fun x s => (IsOpen s ∧ ↑(e x) x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) x)
    ((fun x s => ↑(e x).symm '' s) x)

Tactic:
simpa only [e, PartialHomeomorph.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

Result:
no goals

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

Tactic:
let e : M → PartialHomeomorph M H := chartAt H

Result:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyConnectedSpace H
e : M → PartialHomeomorph M H := chartAt H
⊢ LocallyConnectedSpace M

Proof state:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyConnectedSpace H
e : M → PartialHomeomorph M H := chartAt H
⊢ LocallyConnectedSpace M

Tactic:
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) ?_ ?_

Result:
case refine_1
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyConnectedSpace H
e : M → PartialHomeomorph M H := chartAt H
⊢ ∀ (x : M),
    (𝓝 x).HasBasis ((fun x s => (IsOpen s ∧ ↑(e x) x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) x)
      ((fun x s => ↑(e x).symm '' s) x)

case refine_2
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyConnectedSpace H
e : M → PartialHomeomorph 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 => ↑(e x).symm '' s) x i)

Proof state:
case refine_2.intro.intro.intro
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyConnectedSpace H
e : M → PartialHomeomorph M H := chartAt H
x : M
s : Set H
hssubset : s ⊆ (e x).target
hsconn : IsConnected s
⊢ IsPreconnected ((fun x s => ↑(e x).symm '' s) x s)

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

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✝ : LocallyConnectedSpace H
e : M → PartialHomeomorph 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 => ↑(e x).symm '' s) x i)

Tactic:
rintro x s ⟨⟨-, -, hsconn⟩, hssubset⟩

Result:
case refine_2.intro.intro.intro
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyConnectedSpace H
e : M → PartialHomeomorph M H := chartAt H
x : M
s : Set H
hssubset : s ⊆ (e x).target
hsconn : IsConnected s
⊢ IsPreconnected ((fun x s => ↑(e x).symm '' s) x s)

Proof state:
case refine_1
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyConnectedSpace H
e : M → PartialHomeomorph M H := chartAt H
⊢ ∀ (x : M),
    (𝓝 x).HasBasis ((fun x s => (IsOpen s ∧ ↑(e x) x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) x)
      ((fun x s => ↑(e x).symm '' s) x)

Tactic:
intro x

Result:
case refine_1
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyConnectedSpace H
e : M → PartialHomeomorph M H := chartAt H
x : M
⊢ (𝓝 x).HasBasis ((fun x s => (IsOpen s ∧ ↑(e x) x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) x)
    ((fun x s => ↑(e x).symm '' s) x)