case intro
X✝ : Type ?u.681883
Y : Type ?u.681886
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.681901
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
γ : Path (p 0) (p ↑n)
hγ : range ↑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ↑γ
⊢ ∃ γ t, (∀ (t : ↑I), ↑γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), ↑γ (t i) = p i
X✝ : Type ?u.681883
Y : Type ?u.681886
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.681901
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
⊢ ∃ γ t, (∀ (t : ↑I), ↑γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), ↑γ (t i) = p i
rcases h.exists_path_through_family p hp with ⟨γ, hγ⟩
case intro.intro
X✝ : Type ?u.681883
Y : Type ?u.681886
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.681901
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
γ : Path (p 0) (p ↑n)
h₁ : range ↑γ ⊆ s
h₂ : ∀ (i : Fin (n + 1)), p i ∈ range ↑γ
⊢ ∃ γ t, (∀ (t : ↑I), ↑γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), ↑γ (t i) = p i
case intro
X✝ : Type ?u.681883
Y : Type ?u.681886
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.681901
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
γ : Path (p 0) (p ↑n)
hγ : range ↑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ↑γ
⊢ ∃ γ t, (∀ (t : ↑I), ↑γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), ↑γ (t i) = p i
rcases hγ with ⟨h₁, h₂⟩
case intro.intro
X✝ : Type ?u.681883
Y : Type ?u.681886
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.681901
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
γ : Path (p 0) (p ↑n)
h₁ : range ↑γ ⊆ s
h₂ : ∀ (i : Fin (n + 1)), ∃ y, ↑γ y = p i
⊢ ∃ γ t, (∀ (t : ↑I), ↑γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), ↑γ (t i) = p i
case intro.intro
X✝ : Type ?u.681883
Y : Type ?u.681886
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.681901
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
γ : Path (p 0) (p ↑n)
h₁ : range ↑γ ⊆ s
h₂ : ∀ (i : Fin (n + 1)), p i ∈ range ↑γ
⊢ ∃ γ t, (∀ (t : ↑I), ↑γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), ↑γ (t i) = p i
simp only [range, mem_setOf_eq] at h₂
case intro.intro
X✝ : Type ?u.681883
Y : Type ?u.681886
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.681901
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
γ : Path (p 0) (p ↑n)
h₁ : ∀ (y : ↑I), ↑γ y ∈ s
h₂ : ∀ (i : Fin (n + 1)), ∃ y, ↑γ y = p i
⊢ ∃ γ t, (∀ (t : ↑I), ↑γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), ↑γ (t i) = p i
case intro.intro
X✝ : Type ?u.681883
Y : Type ?u.681886
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.681901
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
γ : Path (p 0) (p ↑n)
h₁ : range ↑γ ⊆ s
h₂ : ∀ (i : Fin (n + 1)), ∃ y, ↑γ y = p i
⊢ ∃ γ t, (∀ (t : ↑I), ↑γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), ↑γ (t i) = p i
rw [range_subset_iff] at h₁
case intro.intro
X✝ : Type ?u.681883
Y : Type ?u.681886
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.681901
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
γ : Path (p 0) (p ↑n)
h₁ : ∀ (y : ↑I), ↑γ y ∈ s
t : Fin (n + 1) → ↑I
ht : ∀ (i : Fin (n + 1)), ↑γ (t i) = p i
⊢ ∃ γ t, (∀ (t : ↑I), ↑γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), ↑γ (t i) = p i
case intro.intro
X✝ : Type ?u.681883
Y : Type ?u.681886
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.681901
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
γ : Path (p 0) (p ↑n)
h₁ : ∀ (y : ↑I), ↑γ y ∈ s
h₂ : ∀ (i : Fin (n + 1)), ∃ y, ↑γ y = p i
⊢ ∃ γ t, (∀ (t : ↑I), ↑γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), ↑γ (t i) = p i
choose! t ht using h₂
no goals
case intro.intro
X✝ : Type ?u.681883
Y : Type ?u.681886
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.681901
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
γ : Path (p 0) (p ↑n)
h₁ : ∀ (y : ↑I), ↑γ y ∈ s
t : Fin (n + 1) → ↑I
ht : ∀ (i : Fin (n + 1)), ↑γ (t i) = p i
⊢ ∃ γ t, (∀ (t : ↑I), ↑γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), ↑γ (t i) = p i
exact ⟨γ, t, h₁, ht⟩