case mp.intro.intro
X : Type u_1
Y : Type ?u.641555
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.641570
F : Set X
x : X
x_in : x ∈ F
h : ∀ {y : X}, y ∈ F → JoinedIn F x y
⊢ pathComponentIn x F = F

case mpr.intro.intro
X : Type u_1
Y : Type ?u.641555
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.641570
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn x F = F
⊢ ∀ {y : X}, y ∈ F → JoinedIn F x y
X : Type u_1
Y : Type ?u.641555
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.641570
F : Set X
⊢ IsPathConnected F ↔ ∃ x, x ∈ F ∧ pathComponentIn x F = F
constructor <;> rintro ⟨x, x_in, h⟩ <;> use x, x_in
case mp.intro.intro.h
X : Type u_1
Y : Type ?u.641555
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z : X
ι : Type ?u.641570
F : Set X
x : X
x_in : x ∈ F
h : ∀ {y : X}, y ∈ F → JoinedIn F x y
y : X
⊢ y ∈ pathComponentIn x F ↔ y ∈ F
case mp.intro.intro
X : Type u_1
Y : Type ?u.641555
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.641570
F : Set X
x : X
x_in : x ∈ F
h : ∀ {y : X}, y ∈ F → JoinedIn F x y
⊢ pathComponentIn x F = F
ext y
no goals
case mp.intro.intro.h
X : Type u_1
Y : Type ?u.641555
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z : X
ι : Type ?u.641570
F : Set X
x : X
x_in : x ∈ F
h : ∀ {y : X}, y ∈ F → JoinedIn F x y
y : X
⊢ y ∈ pathComponentIn x F ↔ y ∈ F
exact ⟨fun hy => hy.mem.2, h⟩
case mpr.intro.intro
X : Type u_1
Y : Type ?u.641555
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z : X
ι : Type ?u.641570
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn x F = F
y : X
y_in : y ∈ F
⊢ JoinedIn F x y
case mpr.intro.intro
X : Type u_1
Y : Type ?u.641555
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.641570
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn x F = F
⊢ ∀ {y : X}, y ∈ F → JoinedIn F x y
intro y y_in
no goals
case mpr.intro.intro
X : Type u_1
Y : Type ?u.641555
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z : X
ι : Type ?u.641570
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn x F = F
y : X
y_in : y ∈ F
⊢ JoinedIn F x y
rwa [← h] at y_in