awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
c : ZerothHomotopy X
obtain : ∀ (x : X), IsOpen (X := ZerothHomotopy X) {ZerothHomotopy.mk x}
⊢ IsOpen (X := ZerothHomotopy X) {c}

Tactic:
obtain ⟨x, rfl⟩ := ZerothHomotopy.mk_surjective c

Premises used: ZerothHomotopy.mk_surjective, rfl
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
x : X
rw : IsOpen[inst] (preimage (β := ZerothHomotopy X) ZerothHomotopy.mk {ZerothHomotopy.mk x})
⊢ IsOpen (X := ZerothHomotopy X) {ZerothHomotopy.mk x}

Tactic:
rw [← ZerothHomotopy.isQuotientMap_mk.isOpen_preimage]

Premises used: Topology.IsCoinducing.isOpen_preimage, Topology.IsQuotientMap.isCoinducing, ZerothHomotopy.isQuotientMap_mk
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
x : X
⊢ IsOpen[inst] (preimage (β := ZerothHomotopy X) ZerothHomotopy.mk {ZerothHomotopy.mk x})

Tactic:
grind [ZerothHomotopy.preimage_singleton_eq_pathComponent, IsOpen.pathComponent]

Premises used: ZerothHomotopy.preimage_singleton_eq_pathComponent, IsOpen.pathComponent
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : CompactSpace X
⊢ Finite.{u_1 + 1} (ZerothHomotopy X)

Tactic:
finite_of_compact_of_discrete

Premises used: finite_of_compact_of_discrete
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
⊢ LocallyConnectedSpace α ↔ ∀ (x : α), (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id

Tactic:
⟨@LocallyConnectedSpace.open_connected_basis _ _, LocallyConnectedSpace.mk⟩

Premises used: LocallyConnectedSpace.mk, Iff.intro, LocallyConnectedSpace.open_connected_basis
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
simp_rw :
  (∀ (x : α), (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id) ↔
    ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
⊢ LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V

Tactic:
simp_rw [locallyConnectedSpace_iff_hasBasis_isOpen_isConnected]

Premises used: locallyConnectedSpace_iff_hasBasis_isOpen_isConnected
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
⊢ (∀ (x : α), (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id) ↔
    ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V

Tactic:
forall_congr' fun _ => ?_

Premises used: forall_congr'
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
refine :
  ∀ (x : α),
    (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id ↔
      ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
⊢ (∀ (x : α), (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id) ↔
    ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V

Tactic:
refine forall_congr' fun _ => ?_

Premises used: forall_congr'
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
x : α
mp :
  (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id →
    ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
mpr :
  (∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V) →
    (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id
⊢ (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id ↔
    ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V

Tactic:
constructor
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
x : α
h : (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id
U : Set α
hU : U ∈ 𝓝 x
mp :
  ∀ (V : Set α) (hV : IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V) (hVU : id V ⊆ U),
    ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
⊢ ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V

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

Premises used: Filter.HasBasis.mem_iff, Iff.mp
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
x : α
h : (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id
U : Set α
hU : U ∈ 𝓝 x
V : Set α
hV : IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
hVU : id V ⊆ U
⊢ ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V

Tactic:
⟨V, hVU, hV⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
x : α
h : (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id
U : Set α
hU : U ∈ 𝓝 x
V : Set α
hV : IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
hVU : id V ⊆ U
⊢ ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V

Tactic:
exact ⟨V, hVU, hV⟩
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
x : α
⊢ (∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V) →
    (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id

Tactic:
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⟩⟩⟩

Premises used: Iff.mpr, IsConnected, mem_nhds_iff, Membership.mem, Exists, nhds, id, HasSubset.Subset, And, _private.0.locallyConnectedSpace_iff_subsets_isOpen_isConnected.match_1, _private.0.locallyConnectedSpace_iff_subsets_isOpen_isConnected.match_2, Filter.HasBasis.mk, And.intro, Iff.intro, Exists.intro, IsOpen
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
x : α
⊢ (∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V) →
    (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] 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⟩⟩⟩
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α_1 : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α_1
s t u v : Set α_1
α : Type u_3
inst_1 : TopologicalSpace α
inst_2 : DiscreteTopology α
⊢ LocallyConnectedSpace α

Tactic:
locallyConnectedSpace_iff_subsets_isOpen_isConnected.2 fun x _U hU =>
    ⟨{x}, singleton_subset_iff.2 <| mem_of_mem_nhds hU, isOpen_discrete _, rfl,
      isConnected_singleton⟩

Premises used: Iff.mpr, Set.singleton_subset_iff, isConnected_singleton, mem_of_mem_nhds, And.intro, isOpen_discrete, Exists.intro, locallyConnectedSpace_iff_subsets_isOpen_isConnected, Singleton.singleton, rfl
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
F : Set α
x : α
h : F ∈ 𝓝 x
⊢ ∃ (i : Set α), (IsOpen[inst] i ∧ x ∈ i ∧ IsConnected i) ∧ id i ⊆ F

Tactic:
rw [(LocallyConnectedSpace.open_connected_basis x).mem_iff] at h

Premises used: Filter.HasBasis.mem_iff, LocallyConnectedSpace.open_connected_basis
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
F : Set α
x : α
h : ∃ (i : Set α), (IsOpen[inst] i ∧ x ∈ i ∧ IsConnected i) ∧ id i ⊆ F
rcases :
  ∀ (s : Set α) (hsF : id s ⊆ F) (h1s : IsOpen[inst] s) (hxs : x ∈ s) (h2s : IsConnected s),
    connectedComponentIn F x ∈ 𝓝 x
⊢ connectedComponentIn F x ∈ 𝓝 x

Tactic:
rcases h with ⟨s, ⟨h1s, hxs, h2s⟩, hsF⟩
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
F : Set α
x : α
s : Set α
hsF : id s ⊆ F
h1s : IsOpen[inst] s
hxs : x ∈ s
h2s : IsConnected s
⊢ connectedComponentIn F x ∈ 𝓝 x

Tactic:
mem_nhds_iff.mpr ⟨s, h2s.isPreconnected.subset_connectedComponentIn hxs hsF, h1s, hxs⟩

Premises used: Iff.mpr, mem_nhds_iff, IsConnected.isPreconnected, And.intro, Exists.intro, IsPreconnected.subset_connectedComponentIn
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
F : Set α
x : α
s : Set α
hsF : id s ⊆ F
h1s : IsOpen[inst] s
hxs : x ∈ s
h2s : IsConnected s
⊢ connectedComponentIn F x ∈ 𝓝 x

Tactic:
exact mem_nhds_iff.mpr ⟨s, h2s.isPreconnected.subset_connectedComponentIn hxs hsF, h1s, hxs⟩

Premises used: Iff.mpr, mem_nhds_iff, IsConnected.isPreconnected, And.intro, Exists.intro, IsPreconnected.subset_connectedComponentIn
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen[inst] F
rw : ∀ x_1 ∈ connectedComponentIn F x, connectedComponentIn F x ∈ 𝓝 x_1
⊢ IsOpen[inst] (connectedComponentIn F x)

Tactic:
rw [isOpen_iff_mem_nhds]

Premises used: isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen[inst] F
y : α
hy : y ∈ connectedComponentIn F x
rw : connectedComponentIn F y ∈ 𝓝 y
⊢ connectedComponentIn F x ∈ 𝓝 y

Tactic:
rw [connectedComponentIn_eq hy]

Premises used: connectedComponentIn_eq
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen[inst] F
y : α
hy : y ∈ connectedComponentIn F x
⊢ connectedComponentIn F y ∈ 𝓝 y

Tactic:
connectedComponentIn_mem_nhds (hF.mem_nhds <| connectedComponentIn_subset F x hy)

Premises used: connectedComponentIn_subset, connectedComponentIn_mem_nhds, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen[inst] F
y : α
hy : y ∈ connectedComponentIn F x
⊢ connectedComponentIn F y ∈ 𝓝 y

Tactic:
exact connectedComponentIn_mem_nhds (hF.mem_nhds <| connectedComponentIn_subset F x hy)

Premises used: connectedComponentIn_subset, connectedComponentIn_mem_nhds, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
x : α
rw : IsOpen[inst] (connectedComponentIn univ x)
⊢ IsOpen[inst] (connectedComponent x)

Tactic:
rw [← connectedComponentIn_univ]

Premises used: connectedComponentIn_univ
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
x : α
⊢ IsOpen[inst] (connectedComponentIn univ x)

Tactic:
isOpen_univ.connectedComponentIn

Premises used: isOpen_univ, IsOpen.connectedComponentIn
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
x : α
⊢ IsOpen[inst] (connectedComponentIn univ x)

Tactic:
exact isOpen_univ.connectedComponentIn

Premises used: isOpen_univ, IsOpen.connectedComponentIn
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
x : α
⊢ IsClopen (connectedComponent x)

Tactic:
⟨isClosed_connectedComponent, isOpen_connectedComponent⟩

Premises used: isOpen_connectedComponent, And.intro, isClosed_connectedComponent, IsClopen
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
mp : LocallyConnectedSpace α → ∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)
mpr : (∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)) → LocallyConnectedSpace α
⊢ LocallyConnectedSpace α ↔ ∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)

Tactic:
constructor
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
h : LocallyConnectedSpace α
⊢ ∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)

Tactic:
fun F hF x _ => hF.connectedComponentIn

Premises used: IsOpen.connectedComponentIn
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
h : LocallyConnectedSpace α
⊢ ∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)

Tactic:
exact fun F hF x _ => hF.connectedComponentIn
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)
mpr : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
⊢ LocallyConnectedSpace α

Tactic:
rw [locallyConnectedSpace_iff_subsets_isOpen_isConnected]

Premises used: locallyConnectedSpace_iff_subsets_isOpen_isConnected
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)
⊢ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V

Tactic:
fun x U hU =>
        ⟨connectedComponentIn (interior U) x,
          (connectedComponentIn_subset _ _).trans interior_subset, h _ isOpen_interior x ?_,
          mem_connectedComponentIn ?_, isConnected_connectedComponentIn_iff.mpr ?_⟩

Premises used: Iff.mpr, connectedComponentIn_subset, interior_subset, isOpen_interior, mem_connectedComponentIn, HasSubset.Subset.trans, isConnected_connectedComponentIn_iff, And.intro, interior, Exists.intro, connectedComponentIn
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)
mpr mpr₁ mpr₂ : ∀ (x : α) (U : Set α) (hU : U ∈ 𝓝 x), x ∈ interior U
⊢ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V

Tactic:
refine fun x U hU =>
        ⟨connectedComponentIn (interior U) x,
          (connectedComponentIn_subset _ _).trans interior_subset, h _ isOpen_interior x ?_,
          mem_connectedComponentIn ?_, isConnected_connectedComponentIn_iff.mpr ?_⟩
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)
x : α
U : Set α
hU : U ∈ 𝓝 x
⊢ x ∈ interior U

Tactic:
mem_interior_iff_mem_nhds.mpr hU

Premises used: Iff.mpr, mem_interior_iff_mem_nhds
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)
x : α
U : Set α
hU : U ∈ 𝓝 x
⊢ x ∈ interior U

Tactic:
exact mem_interior_iff_mem_nhds.mpr hU

Premises used: Iff.mpr, mem_interior_iff_mem_nhds
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
mp : LocallyConnectedSpace α → ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
mpr : (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) → LocallyConnectedSpace α
⊢ LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U

Tactic:
constructor
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
mp :
  (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V) →
    ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
⊢ LocallyConnectedSpace α → ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U

Tactic:
rw [locallyConnectedSpace_iff_subsets_isOpen_isConnected]

Premises used: locallyConnectedSpace_iff_subsets_isOpen_isConnected
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
x : α
U : Set α
hxU : U ∈ 𝓝 x
mp :
  ∀ (V : Set α) (hVU : V ⊆ U) (hV₁ : IsOpen[inst] V) (hxV : x ∈ V) (hV₂ : IsConnected V),
    ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
⊢ ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U

Tactic:
rcases h x U hxU with ⟨V, hVU, hV₁, hxV, hV₂⟩
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
x : α
U : Set α
hxU : U ∈ 𝓝 x
V : Set α
hVU : V ⊆ U
hV₁ : IsOpen[inst] V
hxV : x ∈ V
hV₂ : IsConnected V
⊢ ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U

Tactic:
⟨V, hV₁.mem_nhds hxV, hV₂.isPreconnected, hVU⟩

Premises used: IsConnected.isPreconnected, And.intro, IsOpen.mem_nhds, Exists.intro
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
x : α
U : Set α
hxU : U ∈ 𝓝 x
V : Set α
hVU : V ⊆ U
hV₁ : IsOpen[inst] V
hxV : x ∈ V
hV₂ : IsConnected V
⊢ ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U

Tactic:
exact ⟨V, hV₁.mem_nhds hxV, hV₂.isPreconnected, hVU⟩
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
mpr :
  (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) →
    ∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)
⊢ (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) → LocallyConnectedSpace α

Tactic:
rw [locallyConnectedSpace_iff_connectedComponentIn_open]

Premises used: locallyConnectedSpace_iff_connectedComponentIn_open
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
⊢ (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) →
    ∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)

Tactic:
fun h U hU x _ => isOpen_iff_mem_nhds.mpr fun y hy => ?_

Premises used: Iff.mpr, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
mpr :
  ∀ (h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) (U : Set α) (hU : IsOpen[inst] U),
    ∀ x ∈ U, ∀ (y : α) (hy : y ∈ connectedComponentIn U x), connectedComponentIn U x ∈ 𝓝 y
⊢ (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) →
    ∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)

Tactic:
refine fun h U hU x _ => isOpen_iff_mem_nhds.mpr fun y hy => ?_

Premises used: Iff.mpr, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
U : Set α
hU : IsOpen[inst] U
x : α
h_1 : x ∈ U
y : α
hy : y ∈ connectedComponentIn U x
mpr : connectedComponentIn U y ∈ 𝓝 y
⊢ connectedComponentIn U x ∈ 𝓝 y

Tactic:
rw [connectedComponentIn_eq hy]

Premises used: connectedComponentIn_eq
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
U : Set α
hU : IsOpen[inst] U
x : α
h_1 : x ∈ U
y : α
hy : y ∈ connectedComponentIn U x
mpr : ∀ (V : Set α) (hVy : V ∈ 𝓝 y) (hV : IsPreconnected V) (hVU : V ⊆ U), connectedComponentIn U y ∈ 𝓝 y
⊢ connectedComponentIn U y ∈ 𝓝 y

Tactic:
rcases h y U (hU.mem_nhds <| (connectedComponentIn_subset _ _) hy) with ⟨V, hVy, hV, hVU⟩

Premises used: connectedComponentIn_subset, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
U : Set α
hU : IsOpen[inst] U
x : α
h_1 : x ∈ U
y : α
hy : y ∈ connectedComponentIn U x
V : Set α
hVy : V ∈ 𝓝 y
hV : IsPreconnected V
hVU : V ⊆ U
⊢ connectedComponentIn U y ∈ 𝓝 y

Tactic:
Filter.mem_of_superset hVy (hV.subset_connectedComponentIn (mem_of_mem_nhds hVy) hVU)

Premises used: mem_of_mem_nhds, IsPreconnected.subset_connectedComponentIn, Filter.mem_of_superset
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
U : Set α
hU : IsOpen[inst] U
x : α
h_1 : x ∈ U
y : α
hy : y ∈ connectedComponentIn U x
V : Set α
hVy : V ∈ 𝓝 y
hV : IsPreconnected V
hVU : V ⊆ U
⊢ connectedComponentIn U y ∈ 𝓝 y

Tactic:
exact Filter.mem_of_superset hVy (hV.subset_connectedComponentIn (mem_of_mem_nhds hVy) hVU)

Premises used: mem_of_mem_nhds, IsPreconnected.subset_connectedComponentIn, Filter.mem_of_superset
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
rw :
  (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) ↔
    ∀ (x : α), (𝓝 x).HasBasis (fun (s : Set α) ↦ s ∈ 𝓝 x ∧ IsPreconnected s) id
⊢ LocallyConnectedSpace α ↔ ∀ (x : α), (𝓝 x).HasBasis (fun (s : Set α) ↦ s ∈ 𝓝 x ∧ IsPreconnected s) id

Tactic:
rw [locallyConnectedSpace_iff_connected_subsets]

Premises used: locallyConnectedSpace_iff_connected_subsets
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
⊢ (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) ↔
    ∀ (x : α), (𝓝 x).HasBasis (fun (s : Set α) ↦ s ∈ 𝓝 x ∧ IsPreconnected s) id

Tactic:
forall_congr' fun x => Filter.hasBasis_self.symm

Premises used: Filter.hasBasis_self, forall_congr', Iff.symm
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
⊢ (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) ↔
    ∀ (x : α), (𝓝 x).HasBasis (fun (s : Set α) ↦ s ∈ 𝓝 x ∧ IsPreconnected s) id

Tactic:
exact forall_congr' fun x => Filter.hasBasis_self.symm

Premises used: Filter.hasBasis_self, forall_congr', Iff.symm
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
b : α → ι → Set α
p : α → ι → Prop
hbasis : ∀ (x : α), (𝓝 x).HasBasis (p x) (b x)
hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)
rw : ∀ (x : α), (𝓝 x).HasBasis (fun (s : Set α) ↦ s ∈ 𝓝 x ∧ IsPreconnected s) id
⊢ LocallyConnectedSpace α

Tactic:
rw [locallyConnectedSpace_iff_connected_basis]

Premises used: locallyConnectedSpace_iff_connected_basis
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
b : α → ι → Set α
p : α → ι → Prop
hbasis : ∀ (x : α), (𝓝 x).HasBasis (p x) (b x)
hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)
⊢ ∀ (x : α), (𝓝 x).HasBasis (fun (s : Set α) ↦ s ∈ 𝓝 x ∧ IsPreconnected s) id

Tactic:
fun x =>
    (hbasis x).to_hasBasis
      (fun i hi => ⟨b x i, ⟨(hbasis x).mem_of_mem hi, hconnected x i hi⟩, subset_rfl⟩) fun s hs =>
      ⟨(hbasis x).index s hs.1, ⟨(hbasis x).property_index hs.1, (hbasis x).set_index_subset hs.1⟩⟩

Premises used: Filter.HasBasis.index, Filter.HasBasis.property_index, Filter.HasBasis.set_index_subset, And.left, And.intro, Exists.intro, Subtype.val, Filter.HasBasis.to_hasBasis, subset_rfl, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
b : α → ι → Set α
p : α → ι → Prop
hbasis : ∀ (x : α), (𝓝 x).HasBasis (p x) (b x)
hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)
⊢ ∀ (x : α), (𝓝 x).HasBasis (fun (s : Set α) ↦ s ∈ 𝓝 x ∧ IsPreconnected s) id

Tactic:
exact fun x =>
    (hbasis x).to_hasBasis
      (fun i hi => ⟨b x i, ⟨(hbasis x).mem_of_mem hi, hconnected x i hi⟩, subset_rfl⟩) fun s hs =>
      ⟨(hbasis x).index s hs.1, ⟨(hbasis x).property_index hs.1, (hbasis x).set_index_subset hs.1⟩⟩

Premises used: Filter.HasBasis.index, Filter.HasBasis.property_index, Filter.HasBasis.set_index_subset, And.intro, Exists.intro, Subtype.val, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
x : α
⊢ ∀ (i : Set α),
    IsOpen[inst] i ∧ x ∈ i ∧ IsConnected i ↔
      Membership.mem (γ := Set (Set α)) {s : Set α | IsOpen[inst] s ∧ IsPreconnected s} i ∧ x ∈ i

Tactic:
grind [IsConnected, Set.Nonempty]

Premises used: IsConnected, Set.Nonempty