case mp
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
⊢ PathConnectedSpace X → ConnectedSpace X

case mpr
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
⊢ ConnectedSpace X → PathConnectedSpace X
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
⊢ PathConnectedSpace X ↔ ConnectedSpace X
constructor
case mp
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
h : PathConnectedSpace X
⊢ ConnectedSpace X
case mp
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
⊢ PathConnectedSpace X → ConnectedSpace X
intro h
no goals
case mp
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
h : PathConnectedSpace X
⊢ ConnectedSpace X
infer_instance
case mpr
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
⊢ PathConnectedSpace X
case mpr
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
⊢ ConnectedSpace X → PathConnectedSpace X
intro hX
case mpr
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
⊢ ∃ x, pathComponent x = univ
case mpr
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
⊢ PathConnectedSpace X
rw [pathConnectedSpace_iff_eq]
case mpr
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
⊢ pathComponent (Classical.arbitrary X) = univ
case mpr
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
⊢ ∃ x, pathComponent x = univ
use Classical.arbitrary X
case mpr.refine'_1
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
⊢ IsOpen (pathComponent (Classical.arbitrary X))

case mpr.refine'_2
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
⊢ IsClosed (pathComponent (Classical.arbitrary X))
case mpr
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
⊢ pathComponent (Classical.arbitrary X) = univ
refine' IsClopen.eq_univ ⟨_, _⟩ (by simp)
no goals
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
⊢ Set.Nonempty (pathComponent (Classical.arbitrary X))
simp
case mpr.refine'_1
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
⊢ ∀ (a : X), a ∈ pathComponent (Classical.arbitrary X) → pathComponent (Classical.arbitrary X) ∈ 𝓝 a
case mpr.refine'_1
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
⊢ IsOpen (pathComponent (Classical.arbitrary X))
rw [isOpen_iff_mem_nhds]
case mpr.refine'_1
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y✝ z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
y : X
y_in : y ∈ pathComponent (Classical.arbitrary X)
⊢ pathComponent (Classical.arbitrary X) ∈ 𝓝 y
case mpr.refine'_1
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
⊢ ∀ (a : X), a ∈ pathComponent (Classical.arbitrary X) → pathComponent (Classical.arbitrary X) ∈ 𝓝 a
intro y y_in
case mpr.refine'_1.intro.intro
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y✝ z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
y : X
y_in : y ∈ pathComponent (Classical.arbitrary X)
U : Set X
U_in : U ∈ 𝓝 y
hU : IsPathConnected U
⊢ pathComponent (Classical.arbitrary X) ∈ 𝓝 y
case mpr.refine'_1
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y✝ z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
y : X
y_in : y ∈ pathComponent (Classical.arbitrary X)
⊢ pathComponent (Classical.arbitrary X) ∈ 𝓝 y
rcases(path_connected_basis y).ex_mem with ⟨U, ⟨U_in, hU⟩⟩
case mpr.refine'_1.intro.intro
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y✝ z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
y : X
y_in : y ∈ pathComponent (Classical.arbitrary X)
U : Set X
U_in : U ∈ 𝓝 y
hU : IsPathConnected U
⊢ U ⊆ pathComponent (Classical.arbitrary X)
case mpr.refine'_1.intro.intro
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y✝ z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
y : X
y_in : y ∈ pathComponent (Classical.arbitrary X)
U : Set X
U_in : U ∈ 𝓝 y
hU : IsPathConnected U
⊢ pathComponent (Classical.arbitrary X) ∈ 𝓝 y
apply mem_of_superset U_in
case mpr.refine'_1.intro.intro
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y✝ z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
y : X
y_in : y ∈ pathComponent (Classical.arbitrary X)
U : Set X
U_in : U ∈ 𝓝 y
hU : IsPathConnected U
⊢ U ⊆ pathComponent y
case mpr.refine'_1.intro.intro
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y✝ z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
y : X
y_in : y ∈ pathComponent (Classical.arbitrary X)
U : Set X
U_in : U ∈ 𝓝 y
hU : IsPathConnected U
⊢ U ⊆ pathComponent (Classical.arbitrary X)
rw [← pathComponent_congr y_in]
no goals
case mpr.refine'_1.intro.intro
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y✝ z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
y : X
y_in : y ∈ pathComponent (Classical.arbitrary X)
U : Set X
U_in : U ∈ 𝓝 y
hU : IsPathConnected U
⊢ U ⊆ pathComponent y
exact hU.subset_pathComponent (mem_of_mem_nhds U_in)
case mpr.refine'_2
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
⊢ ∀ (x : X),
    (∀ (U : Set X), U ∈ 𝓝 x → Set.Nonempty (U ∩ pathComponent (Classical.arbitrary X))) →
      x ∈ pathComponent (Classical.arbitrary X)
case mpr.refine'_2
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
⊢ IsClosed (pathComponent (Classical.arbitrary X))
rw [isClosed_iff_nhds]
case mpr.refine'_2
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y✝ z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
y : X
H : ∀ (U : Set X), U ∈ 𝓝 y → Set.Nonempty (U ∩ pathComponent (Classical.arbitrary X))
⊢ y ∈ pathComponent (Classical.arbitrary X)
case mpr.refine'_2
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
⊢ ∀ (x : X),
    (∀ (U : Set X), U ∈ 𝓝 x → Set.Nonempty (U ∩ pathComponent (Classical.arbitrary X))) →
      x ∈ pathComponent (Classical.arbitrary X)
intro y H
case mpr.refine'_2.intro.intro
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y✝ z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
y : X
H : ∀ (U : Set X), U ∈ 𝓝 y → Set.Nonempty (U ∩ pathComponent (Classical.arbitrary X))
U : Set X
U_in : U ∈ 𝓝 y
hU : IsPathConnected U
⊢ y ∈ pathComponent (Classical.arbitrary X)
case mpr.refine'_2
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y✝ z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
y : X
H : ∀ (U : Set X), U ∈ 𝓝 y → Set.Nonempty (U ∩ pathComponent (Classical.arbitrary X))
⊢ y ∈ pathComponent (Classical.arbitrary X)
rcases(path_connected_basis y).ex_mem with ⟨U, ⟨U_in, hU⟩⟩
case mpr.refine'_2.intro.intro.intro.intro
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y✝ z✝ : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
y : X
H : ∀ (U : Set X), U ∈ 𝓝 y → Set.Nonempty (U ∩ pathComponent (Classical.arbitrary X))
U : Set X
U_in : U ∈ 𝓝 y
hU : IsPathConnected U
z : X
hz : z ∈ U
hz' : z ∈ pathComponent (Classical.arbitrary X)
⊢ y ∈ pathComponent (Classical.arbitrary X)
case mpr.refine'_2.intro.intro
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y✝ z : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
y : X
H : ∀ (U : Set X), U ∈ 𝓝 y → Set.Nonempty (U ∩ pathComponent (Classical.arbitrary X))
U : Set X
U_in : U ∈ 𝓝 y
hU : IsPathConnected U
⊢ y ∈ pathComponent (Classical.arbitrary X)
rcases H U U_in with ⟨z, hz, hz'⟩
no goals
case mpr.refine'_2.intro.intro.intro.intro
X : Type u_1
Y : Type ?u.703689
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y✝ z✝ : X
ι : Type ?u.703704
F : Set X
inst✝ : LocPathConnectedSpace X
hX : ConnectedSpace X
y : X
H : ∀ (U : Set X), U ∈ 𝓝 y → Set.Nonempty (U ∩ pathComponent (Classical.arbitrary X))
U : Set X
U_in : U ∈ 𝓝 y
hU : IsPathConnected U
z : X
hz : z ∈ U
hz' : z ∈ pathComponent (Classical.arbitrary X)
⊢ y ∈ pathComponent (Classical.arbitrary X)
exact (hU.joinedIn z hz y <| mem_of_mem_nhds U_in).joined.mem_pathComponent hz'