-- Mathlib/Topology/Connected/LocallyConnected.lean
theorem locallyConnectedSpace_iff_subsets_isOpen_isConnected :
    LocallyConnectedSpace α ↔
      ∀ x, ∀ U ∈ 𝓝 x, ∃ V : Set α, V ⊆ U ∧ IsOpen V ∧ x ∈ V ∧ IsConnected V

Proof state:
case mpr
α : Type u
inst✝ : TopologicalSpace α
x✝ : α
⊢ (∀ U ∈ 𝓝 x✝, ∃ V ⊆ U, IsOpen V ∧ x✝ ∈ V ∧ IsConnected V) →
    (𝓝 x✝).HasBasis (fun s => IsOpen s ∧ x✝ ∈ s ∧ IsConnected s) id

Tactic:
exact fun h => ⟨fun U => ⟨fun hU =>
  let ⟨V, hVU, hV⟩ := h U hU
  ⟨V, hV, hVU⟩, fun ⟨V, ⟨hV, hxV, _⟩, hVU⟩ => mem_nhds_iff.mpr ⟨V, hVU, hV, hxV⟩⟩⟩

Result:
no goals

Proof state:
case mp
α : Type u
inst✝ : TopologicalSpace α
x✝ : α
⊢ (𝓝 x✝).HasBasis (fun s => IsOpen s ∧ x✝ ∈ s ∧ IsConnected s) id →
    ∀ U ∈ 𝓝 x✝, ∃ V ⊆ U, IsOpen V ∧ x✝ ∈ V ∧ IsConnected V

Tactic:
intro h U hU

Result:
case mp
α : Type u
inst✝ : TopologicalSpace α
x✝ : α
h : (𝓝 x✝).HasBasis (fun s => IsOpen s ∧ x✝ ∈ s ∧ IsConnected s) id
U : Set α
hU : U ∈ 𝓝 x✝
⊢ ∃ V ⊆ U, IsOpen V ∧ x✝ ∈ V ∧ IsConnected V

Proof state:
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), (𝓝 x).HasBasis (fun s => IsOpen s ∧ x ∈ s ∧ IsConnected s) id) ↔
    ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen V ∧ x ∈ V ∧ IsConnected V

Tactic:
refine forall_congr' fun _ => ?_

Result:
α : Type u
inst✝ : TopologicalSpace α
x✝ : α
⊢ (𝓝 x✝).HasBasis (fun s => IsOpen s ∧ x✝ ∈ s ∧ IsConnected s) id ↔
    ∀ U ∈ 𝓝 x✝, ∃ V ⊆ U, IsOpen V ∧ x✝ ∈ V ∧ IsConnected V

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x✝ : α
⊢ (𝓝 x✝).HasBasis (fun s => IsOpen s ∧ x✝ ∈ s ∧ IsConnected s) id ↔
    ∀ U ∈ 𝓝 x✝, ∃ V ⊆ U, IsOpen V ∧ x✝ ∈ V ∧ IsConnected V

Tactic:
constructor

Result:
case mp
α : Type u
inst✝ : TopologicalSpace α
x✝ : α
⊢ (𝓝 x✝).HasBasis (fun s => IsOpen s ∧ x✝ ∈ s ∧ IsConnected s) id →
    ∀ U ∈ 𝓝 x✝, ∃ V ⊆ U, IsOpen V ∧ x✝ ∈ V ∧ IsConnected V

case mpr
α : Type u
inst✝ : TopologicalSpace α
x✝ : α
⊢ (∀ U ∈ 𝓝 x✝, ∃ V ⊆ U, IsOpen V ∧ x✝ ∈ V ∧ IsConnected V) →
    (𝓝 x✝).HasBasis (fun s => IsOpen s ∧ x✝ ∈ s ∧ IsConnected s) id

Proof state:
case mp
α : Type u
inst✝ : TopologicalSpace α
x✝ : α
h : (𝓝 x✝).HasBasis (fun s => IsOpen s ∧ x✝ ∈ s ∧ IsConnected s) id
U : Set α
hU : U ∈ 𝓝 x✝
⊢ ∃ V ⊆ U, IsOpen V ∧ x✝ ∈ V ∧ IsConnected V

Tactic:
rcases h.mem_iff.mp hU with ⟨V, hV, hVU⟩

Result:
case mp.intro.intro
α : Type u
inst✝ : TopologicalSpace α
x✝ : α
h : (𝓝 x✝).HasBasis (fun s => IsOpen s ∧ x✝ ∈ s ∧ IsConnected s) id
U : Set α
hU : U ∈ 𝓝 x✝
V : Set α
hV : IsOpen V ∧ x✝ ∈ V ∧ IsConnected V
hVU : id V ⊆ U
⊢ ∃ V ⊆ U, IsOpen V ∧ x✝ ∈ V ∧ IsConnected V

Proof state:
α : Type u
inst✝ : TopologicalSpace α
⊢ LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen V ∧ x ∈ V ∧ IsConnected V

Tactic:
simp_rw [locallyConnectedSpace_iff_hasBasis_isOpen_isConnected]

Result:
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), (𝓝 x).HasBasis (fun s => IsOpen s ∧ x ∈ s ∧ IsConnected s) id) ↔
    ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen V ∧ x ∈ V ∧ IsConnected V

Proof state:
case mp.intro.intro
α : Type u
inst✝ : TopologicalSpace α
x✝ : α
h : (𝓝 x✝).HasBasis (fun s => IsOpen s ∧ x✝ ∈ s ∧ IsConnected s) id
U : Set α
hU : U ∈ 𝓝 x✝
V : Set α
hV : IsOpen V ∧ x✝ ∈ V ∧ IsConnected V
hVU : id V ⊆ U
⊢ ∃ V ⊆ U, IsOpen V ∧ x✝ ∈ V ∧ IsConnected V

Tactic:
exact ⟨V, hVU, hV⟩

Result:
no goals