case h
X : Type u_1
Y : Type ?u.624861
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z✝ : X
ι : Type ?u.624876
F : Set X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent x ↔ z ∈ pathComponent y
X : Type u_1
Y : Type ?u.624861
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.624876
F : Set X
h : x ∈ pathComponent y
⊢ pathComponent x = pathComponent y
ext z
case h.mp
X : Type u_1
Y : Type ?u.624861
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z✝ : X
ι : Type ?u.624876
F : Set X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent x → z ∈ pathComponent y

case h.mpr
X : Type u_1
Y : Type ?u.624861
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z✝ : X
ι : Type ?u.624876
F : Set X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent y → z ∈ pathComponent x
case h
X : Type u_1
Y : Type ?u.624861
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z✝ : X
ι : Type ?u.624876
F : Set X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent x ↔ z ∈ pathComponent y
constructor
case h.mp
X : Type u_1
Y : Type ?u.624861
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z✝ : X
ι : Type ?u.624876
F : Set X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent x
⊢ z ∈ pathComponent y
case h.mp
X : Type u_1
Y : Type ?u.624861
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z✝ : X
ι : Type ?u.624876
F : Set X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent x → z ∈ pathComponent y
intro h'
case h.mp
X : Type u_1
Y : Type ?u.624861
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z✝ : X
ι : Type ?u.624876
F : Set X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent x
⊢ y ∈ pathComponent z
case h.mp
X : Type u_1
Y : Type ?u.624861
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z✝ : X
ι : Type ?u.624876
F : Set X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent x
⊢ z ∈ pathComponent y
rw [pathComponent_symm]
no goals
case h.mp
X : Type u_1
Y : Type ?u.624861
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z✝ : X
ι : Type ?u.624876
F : Set X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent x
⊢ y ∈ pathComponent z
exact (h.trans h').symm
case h.mpr
X : Type u_1
Y : Type ?u.624861
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z✝ : X
ι : Type ?u.624876
F : Set X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent y
⊢ z ∈ pathComponent x
case h.mpr
X : Type u_1
Y : Type ?u.624861
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z✝ : X
ι : Type ?u.624876
F : Set X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent y → z ∈ pathComponent x
intro h'
case h.mpr
X : Type u_1
Y : Type ?u.624861
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z✝ : X
ι : Type ?u.624876
F : Set X
h : x ∈ pathComponent y
z : X
h' : y ∈ pathComponent z
⊢ x ∈ pathComponent z
case h.mpr
X : Type u_1
Y : Type ?u.624861
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z✝ : X
ι : Type ?u.624876
F : Set X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent y
⊢ z ∈ pathComponent x
rw [pathComponent_symm] at h'⊢
no goals
case h.mpr
X : Type u_1
Y : Type ?u.624861
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z✝ : X
ι : Type ?u.624876
F : Set X
h : x ∈ pathComponent y
z : X
h' : y ∈ pathComponent z
⊢ x ∈ pathComponent z
exact h'.trans h