X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
⊢ ∃ γ, range ↑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ↑γ
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
⊢ ∃ γ, range ↑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ↑γ
let p' : ℕ → X := fun k => if h : k < n + 1 then p ⟨k, h⟩ else p ⟨0, n.zero_lt_succ⟩
case intro
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hpp' : ∀ (k : ℕ), k < n + 1 → p ↑k = p' k
⊢ ∃ γ, range ↑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ↑γ
case intro
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
⊢ ∃ γ, range ↑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ↑γ
have hpp' : ∀ k < n + 1, p k = p' k := by
  intro k hk
  simp only [hk, dif_pos]
  congr
  ext
  rw [Fin.val_cast_of_lt hk]
case intro
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hpp' : ∀ (k : ℕ), k < n + 1 → p ↑k = p' k
⊢ range ↑(Path.cast γ (_ : p ↑0 = p' 0) (_ : p ↑n = p' n)) ⊆ s ∧
    ∀ (i : Fin (n + 1)), p i ∈ range ↑(Path.cast γ (_ : p ↑0 = p' 0) (_ : p ↑n = p' n))
case intro
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hpp' : ∀ (k : ℕ), k < n + 1 → p ↑k = p' k
⊢ ∃ γ, range ↑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ↑γ
use γ.cast (hpp' 0 n.zero_lt_succ) (hpp' n n.lt_succ_self)
case intro
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hpp' : ∀ (k : ℕ), k < n + 1 → p ↑k = p' k
⊢ range ↑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ↑γ
case intro
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hpp' : ∀ (k : ℕ), k < n + 1 → p ↑k = p' k
⊢ range ↑(Path.cast γ (_ : p ↑0 = p' 0) (_ : p ↑n = p' n)) ⊆ s ∧
    ∀ (i : Fin (n + 1)), p i ∈ range ↑(Path.cast γ (_ : p ↑0 = p' 0) (_ : p ↑n = p' n))
simp only [γ.cast_coe]
case intro
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hpp' : ∀ (k : ℕ), k < n + 1 → p ↑k = p' k
⊢ ∀ (i : Fin (n + 1)), p i ∈ range ↑γ
case intro
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hpp' : ∀ (k : ℕ), k < n + 1 → p ↑k = p' k
⊢ range ↑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ↑γ
refine' And.intro hγ.2 _
case intro.mk
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hpp' : ∀ (k : ℕ), k < n + 1 → p ↑k = p' k
i : ℕ
hi : i < n + 1
⊢ p { val := i, isLt := hi } ∈ range ↑γ
case intro
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hpp' : ∀ (k : ℕ), k < n + 1 → p ↑k = p' k
⊢ ∀ (i : Fin (n + 1)), p i ∈ range ↑γ
rintro ⟨i, hi⟩
case intro.mk
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hpp' : ∀ (k : ℕ), k < n + 1 → p ↑k = p' k
i : ℕ
hi : i < n + 1
⊢ p { val := i, isLt := hi } = p' i
case intro.mk
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hpp' : ∀ (k : ℕ), k < n + 1 → p ↑k = p' k
i : ℕ
hi : i < n + 1
⊢ p { val := i, isLt := hi } ∈ range ↑γ
suffices p ⟨i, hi⟩ = p' i by convert hγ.1 i (Nat.le_of_lt_succ hi)
case intro.mk
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hpp' : ∀ (k : ℕ), k < n + 1 → p ↑k = p' k
i : ℕ
hi : i < n + 1
⊢ p { val := i, isLt := hi } = p ↑i
case intro.mk
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hpp' : ∀ (k : ℕ), k < n + 1 → p ↑k = p' k
i : ℕ
hi : i < n + 1
⊢ p { val := i, isLt := hi } = p' i
rw [← hpp' i hi]
case intro.mk
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hpp' : ∀ (k : ℕ), k < n + 1 → p ↑k = p' k
i : ℕ
hi : i < n + 1
⊢ i = i % Nat.succ n
case intro.mk
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hpp' : ∀ (k : ℕ), k < n + 1 → p ↑k = p' k
i : ℕ
hi : i < n + 1
⊢ p { val := i, isLt := hi } = p ↑i
suffices i = i % n.succ by congr
no goals
case intro.mk
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hpp' : ∀ (k : ℕ), k < n + 1 → p ↑k = p' k
i : ℕ
hi : i < n + 1
⊢ i = i % Nat.succ n
rw [Nat.mod_eq_of_lt hi]
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
hp' : ∀ (i : ℕ), i ≤ n → p' i ∈ s
⊢ ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
⊢ ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
have hp' : ∀ i ≤ n, p' i ∈ s := by
  intro i hi
  simp [Nat.lt_succ_of_le hi, hp]
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X
hp' : ∀ (i : ℕ), i ≤ n → p' i ∈ s
⊢ ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
hp' : ∀ (i : ℕ), i ≤ n → p' i ∈ s
⊢ ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
clear_value p'
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp' : ∀ (i : ℕ), i ≤ n → p' i ∈ s
⊢ ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X
hp' : ∀ (i : ℕ), i ≤ n → p' i ∈ s
⊢ ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
clear hp p
case zero
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n → p' i ∈ s
hp' : ∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ s
⊢ ∃ γ, (∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s

case succ
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
⊢ ∃ γ, (∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp' : ∀ (i : ℕ), i ≤ n → p' i ∈ s
⊢ ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
induction' n with n hn
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
i : ℕ
hi : i ≤ n
⊢ p' i ∈ s
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
⊢ ∀ (i : ℕ), i ≤ n → p' i ∈ s
intro i hi
no goals
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
i : ℕ
hi : i ≤ n
⊢ p' i ∈ s
simp [Nat.lt_succ_of_le hi, hp]
case zero
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n → p' i ∈ s
hp' : ∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ s
⊢ (∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ range ↑(Path.refl (p' 0))) ∧ range ↑(Path.refl (p' 0)) ⊆ s
case zero
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n → p' i ∈ s
hp' : ∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ s
⊢ ∃ γ, (∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
use Path.refl (p' 0)
case zero.left
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n → p' i ∈ s
hp' : ∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ s
⊢ ∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ range ↑(Path.refl (p' 0))

case zero.right
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n → p' i ∈ s
hp' : ∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ s
⊢ range ↑(Path.refl (p' 0)) ⊆ s
case zero
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n → p' i ∈ s
hp' : ∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ s
⊢ (∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ range ↑(Path.refl (p' 0))) ∧ range ↑(Path.refl (p' 0)) ⊆ s
constructor
case zero.left
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n → p' i ∈ s
hp' : ∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ s
i : ℕ
hi : i ≤ Nat.zero
⊢ p' i ∈ range ↑(Path.refl (p' 0))
case zero.left
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n → p' i ∈ s
hp' : ∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ s
⊢ ∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ range ↑(Path.refl (p' 0))
rintro i hi
case zero.left
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n → p' i ∈ s
hp' : ∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ s
i : ℕ
hi : i ≤ Nat.zero
⊢ p' 0 ∈ range ↑(Path.refl (p' 0))
case zero.left
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n → p' i ∈ s
hp' : ∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ s
i : ℕ
hi : i ≤ Nat.zero
⊢ p' i ∈ range ↑(Path.refl (p' 0))
rw [le_zero_iff.mp hi]
no goals
case zero.left
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n → p' i ∈ s
hp' : ∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ s
i : ℕ
hi : i ≤ Nat.zero
⊢ p' 0 ∈ range ↑(Path.refl (p' 0))
exact ⟨0, rfl⟩
case zero.right
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n → p' i ∈ s
hp' : ∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ s
⊢ ∀ (y : ↑I), ↑(Path.refl (p' 0)) y ∈ s
case zero.right
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n → p' i ∈ s
hp' : ∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ s
⊢ range ↑(Path.refl (p' 0)) ⊆ s
rw [range_subset_iff]
case zero.right
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n → p' i ∈ s
hp' : ∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ s
_x : ↑I
⊢ ↑(Path.refl (p' 0)) _x ∈ s
case zero.right
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n → p' i ∈ s
hp' : ∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ s
⊢ ∀ (y : ↑I), ↑(Path.refl (p' 0)) y ∈ s
rintro _x
no goals
case zero.right
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n → p' i ∈ s
hp' : ∀ (i : ℕ), i ≤ Nat.zero → p' i ∈ s
_x : ↑I
⊢ ↑(Path.refl (p' 0)) _x ∈ s
exact hp' 0 le_rfl
case succ.intro
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
⊢ ∃ γ, (∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
case succ
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
⊢ ∃ γ, (∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
rcases hn fun i hi => hp' i <| Nat.le_succ_of_le hi with ⟨γ₀, hγ₀⟩
case succ.intro.intro
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
⊢ ∃ γ, (∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
case succ.intro
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
⊢ ∃ γ, (∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
rcases h.joinedIn (p' n) (hp' n n.le_succ) (p' <| n + 1) (hp' (n + 1) <| le_rfl) with
  ⟨γ₁, hγ₁⟩
case succ.intro.intro
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
⊢ ∃ γ, (∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
case succ.intro.intro
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
⊢ ∃ γ, (∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
let γ : Path (p' 0) (p' <| n + 1) := γ₀.trans γ₁
case succ.intro.intro
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
⊢ (∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
case succ.intro.intro
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
⊢ ∃ γ, (∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
use γ
case succ.intro.intro
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
⊢ (∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
case succ.intro.intro
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
⊢ (∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
have range_eq : range γ = range γ₀ ∪ range γ₁ := γ₀.trans_range γ₁
case succ.intro.intro.left
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
⊢ ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ range ↑γ

case succ.intro.intro.right
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
⊢ range ↑γ ⊆ s
case succ.intro.intro
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
⊢ (∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
constructor
case succ.intro.intro.left
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
i : ℕ
hi : i ≤ Nat.succ n
⊢ p' i ∈ range ↑γ
case succ.intro.intro.left
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
⊢ ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ range ↑γ
rintro i hi
case pos
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
i : ℕ
hi : i ≤ Nat.succ n
hi' : i ≤ n
⊢ p' i ∈ range ↑γ

case neg
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
i : ℕ
hi : i ≤ Nat.succ n
hi' : ¬i ≤ n
⊢ p' i ∈ range ↑γ
case succ.intro.intro.left
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
i : ℕ
hi : i ≤ Nat.succ n
⊢ p' i ∈ range ↑γ
by_cases hi' : i ≤ n
case pos
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
i : ℕ
hi : i ≤ Nat.succ n
hi' : i ≤ n
⊢ p' i ∈ range ↑γ₀ ∪ range ↑γ₁
case pos
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
i : ℕ
hi : i ≤ Nat.succ n
hi' : i ≤ n
⊢ p' i ∈ range ↑γ
rw [range_eq]
case pos.h
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
i : ℕ
hi : i ≤ Nat.succ n
hi' : i ≤ n
⊢ p' i ∈ range ↑γ₀
case pos
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
i : ℕ
hi : i ≤ Nat.succ n
hi' : i ≤ n
⊢ p' i ∈ range ↑γ₀ ∪ range ↑γ₁
left
no goals
case pos.h
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
i : ℕ
hi : i ≤ Nat.succ n
hi' : i ≤ n
⊢ p' i ∈ range ↑γ₀
exact hγ₀.1 i hi'
case neg
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
i : ℕ
hi : i ≤ Nat.succ n
hi' : Nat.succ n ≤ i
⊢ p' i ∈ range ↑γ
case neg
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
i : ℕ
hi : i ≤ Nat.succ n
hi' : ¬i ≤ n
⊢ p' i ∈ range ↑γ
rw [not_le, ← Nat.succ_le_iff] at hi'
case neg
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
i : ℕ
hi : i ≤ Nat.succ n
hi' : Nat.succ n ≤ i
this : i = Nat.succ n
⊢ p' i ∈ range ↑γ
case neg
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
i : ℕ
hi : i ≤ Nat.succ n
hi' : Nat.succ n ≤ i
⊢ p' i ∈ range ↑γ
have : i = n.succ := le_antisymm hi hi'
case neg
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
i : ℕ
hi : i ≤ Nat.succ n
hi' : Nat.succ n ≤ i
this : i = Nat.succ n
⊢ p' (Nat.succ n) ∈ range ↑γ
case neg
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
i : ℕ
hi : i ≤ Nat.succ n
hi' : Nat.succ n ≤ i
this : i = Nat.succ n
⊢ p' i ∈ range ↑γ
rw [this]
case neg
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
i : ℕ
hi : i ≤ Nat.succ n
hi' : Nat.succ n ≤ i
this : i = Nat.succ n
⊢ ↑γ 1 = p' (Nat.succ n)
case neg
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
i : ℕ
hi : i ≤ Nat.succ n
hi' : Nat.succ n ≤ i
this : i = Nat.succ n
⊢ p' (Nat.succ n) ∈ range ↑γ
use 1
no goals
case neg
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
i : ℕ
hi : i ≤ Nat.succ n
hi' : Nat.succ n ≤ i
this : i = Nat.succ n
⊢ ↑γ 1 = p' (Nat.succ n)
exact γ.target
case succ.intro.intro.right
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
⊢ range ↑γ₀ ∪ range ↑γ₁ ⊆ s
case succ.intro.intro.right
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
⊢ range ↑γ ⊆ s
rw [range_eq]
case succ.intro.intro.right
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
⊢ range ↑γ₁ ⊆ s
case succ.intro.intro.right
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
⊢ range ↑γ₀ ∪ range ↑γ₁ ⊆ s
apply union_subset hγ₀.2
case succ.intro.intro.right
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
⊢ ∀ (y : ↑I), ↑γ₁ y ∈ s
case succ.intro.intro.right
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
⊢ range ↑γ₁ ⊆ s
rw [range_subset_iff]
no goals
case succ.intro.intro.right
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
F : Set X✝
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp'✝ : ∀ (i : ℕ), i ≤ n✝ → p' i ∈ s
n : ℕ
hn : (∀ (i : ℕ), i ≤ n → p' i ∈ s) → ∃ γ, (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hp' : ∀ (i : ℕ), i ≤ Nat.succ n → p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ₀) ∧ range ↑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), ↑γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := Path.trans γ₀ γ₁
range_eq : range ↑γ = range ↑γ₀ ∪ range ↑γ₁
⊢ ∀ (y : ↑I), ↑γ₁ y ∈ s
exact hγ₁
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
k : ℕ
hk : k < n + 1
⊢ p ↑k = p' k
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
⊢ ∀ (k : ℕ), k < n + 1 → p ↑k = p' k
intro k hk
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
k : ℕ
hk : k < n + 1
⊢ p ↑k = p { val := k, isLt := (_ : k < n + 1) }
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
k : ℕ
hk : k < n + 1
⊢ p ↑k = p' k
simp only [hk, dif_pos]
case e_a
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
k : ℕ
hk : k < n + 1
⊢ ↑k = { val := k, isLt := (_ : k < n + 1) }
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
k : ℕ
hk : k < n + 1
⊢ p ↑k = p { val := k, isLt := (_ : k < n + 1) }
congr
case e_a.h
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
k : ℕ
hk : k < n + 1
⊢ ↑↑k = ↑{ val := k, isLt := (_ : k < n + 1) }
case e_a
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
k : ℕ
hk : k < n + 1
⊢ ↑k = { val := k, isLt := (_ : k < n + 1) }
ext
no goals
case e_a.h
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
k : ℕ
hk : k < n + 1
⊢ ↑↑k = ↑{ val := k, isLt := (_ : k < n + 1) }
rw [Fin.val_cast_of_lt hk]
no goals
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hpp' : ∀ (k : ℕ), k < n + 1 → p ↑k = p' k
i : ℕ
hi : i < n + 1
this : p { val := i, isLt := hi } = p' i
⊢ p { val := i, isLt := hi } ∈ range ↑γ
convert hγ.1 i (Nat.le_of_lt_succ hi)
no goals
X✝ : Type ?u.658803
Y : Type ?u.658806
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.658821
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
p' : ℕ → X := fun k => if h : k < n + 1 then p { val := k, isLt := h } else p { val := 0, isLt := (_ : 0 < Nat.succ n) }
γ : Path (p' 0) (p' n)
hγ : (∀ (i : ℕ), i ≤ n → p' i ∈ range ↑γ) ∧ range ↑γ ⊆ s
hpp' : ∀ (k : ℕ), k < n + 1 → p ↑k = p' k
i : ℕ
hi : i < n + 1
this : i = i % Nat.succ n
⊢ p { val := i, isLt := hi } = p ↑i
congr