-- Mathlib/Topology/Connected/PathConnected.lean
theorem IsPathConnected.exists_path_through_family {n : ℕ}
    {s : Set X} (h : IsPathConnected s) (p : Fin (n + 1) → X) (hp : ∀ i, p i ∈ s) :
    ∃ γ : Path (p 0) (p n), range γ ⊆ s ∧ ∀ i, p i ∈ range γ

Proof state:
case neg
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPathConnected s
p' : ℕ → X
n : ℕ
hn : (∀ i ≤ n, p' i ∈ s) → ∃ γ, (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s
hp' : ∀ i ≤ n + 1, p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ i ≤ n, p' i ∈ range ⇑γ₀) ∧ range ⇑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := γ₀.trans γ₁
range_eq : range ⇑γ = range ⇑γ₀ ∪ range ⇑γ₁
i : ℕ
hi : i ≤ n + 1
hi' : ¬i ≤ n
⊢ p' i ∈ range ⇑γ

Tactic:
rw [not_le, ← Nat.succ_le_iff] at hi'

Result:
case neg
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPathConnected s
p' : ℕ → X
n : ℕ
hn : (∀ i ≤ n, p' i ∈ s) → ∃ γ, (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s
hp' : ∀ i ≤ n + 1, p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ i ≤ n, p' i ∈ range ⇑γ₀) ∧ range ⇑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := γ₀.trans γ₁
range_eq : range ⇑γ = range ⇑γ₀ ∪ range ⇑γ₁
i : ℕ
hi : i ≤ n + 1
hi' : n.succ ≤ i
⊢ p' i ∈ range ⇑γ

Proof state:
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 ⟨k, h⟩ else p ⟨0, ⋯⟩
γ : Path (p' 0) (p' n)
hγ : (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s
k : ℕ
hk : k < n + 1
⊢ p ↑k = p' k

Tactic:
simp only [p', hk, dif_pos]

Result:
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 ⟨k, h⟩ else p ⟨0, ⋯⟩
γ : Path (p' 0) (p' n)
hγ : (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s
k : ℕ
hk : k < n + 1
⊢ p ↑k = p ⟨k, hk⟩

Proof state:
case e_a
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 ⟨k, h⟩ else p ⟨0, ⋯⟩
γ : Path (p' 0) (p' n)
hγ : (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s
k : ℕ
hk : k < n + 1
⊢ ↑k = ⟨k, hk⟩

Tactic:
ext

Result:
case e_a.h
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 ⟨k, h⟩ else p ⟨0, ⋯⟩
γ : Path (p' 0) (p' n)
hγ : (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s
k : ℕ
hk : k < n + 1
⊢ ↑↑k = ↑⟨k, hk⟩

Proof state:
case h.right
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPathConnected s
p' : ℕ → X
n : ℕ
hn : (∀ i ≤ n, p' i ∈ s) → ∃ γ, (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s
hp' : ∀ i ≤ n + 1, p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ i ≤ n, p' i ∈ range ⇑γ₀) ∧ range ⇑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := γ₀.trans γ₁
range_eq : range ⇑γ = range ⇑γ₀ ∪ range ⇑γ₁
⊢ range ⇑γ ⊆ s

Tactic:
rw [range_eq]

Result:
case h.right
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPathConnected s
p' : ℕ → X
n : ℕ
hn : (∀ i ≤ n, p' i ∈ s) → ∃ γ, (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s
hp' : ∀ i ≤ n + 1, p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ i ≤ n, p' i ∈ range ⇑γ₀) ∧ range ⇑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := γ₀.trans γ₁
range_eq : range ⇑γ = range ⇑γ₀ ∪ range ⇑γ₁
⊢ range ⇑γ₀ ∪ range ⇑γ₁ ⊆ s

Proof state:
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 ⟨k, h⟩ else p ⟨0, ⋯⟩
i : ℕ
hi : i ≤ n
⊢ p' i ∈ s

Tactic:
simp [p', Nat.lt_succ_of_le hi, hp]

Result:
no goals

Proof state:
case h.mk
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 ⟨k, h⟩ else p ⟨0, ⋯⟩
γ : Path (p' 0) (p' n)
hγ : (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s
hpp' : ∀ k < n + 1, p ↑k = p' k
i : ℕ
hi : i < n + 1
⊢ p ⟨i, hi⟩ ∈ range ⇑γ

Tactic:
suffices p ⟨i, hi⟩ = p' i by convert hγ.1 i (Nat.le_of_lt_succ hi)

Result:
case h.mk
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 ⟨k, h⟩ else p ⟨0, ⋯⟩
γ : Path (p' 0) (p' n)
hγ : (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s
hpp' : ∀ k < n + 1, p ↑k = p' k
i : ℕ
hi : i < n + 1
⊢ p ⟨i, hi⟩ = p' i

Proof state:
case h.left
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPathConnected s
p' : ℕ → X
n : ℕ
hn : (∀ i ≤ n, p' i ∈ s) → ∃ γ, (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s
hp' : ∀ i ≤ n + 1, p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ i ≤ n, p' i ∈ range ⇑γ₀) ∧ range ⇑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := γ₀.trans γ₁
range_eq : range ⇑γ = range ⇑γ₀ ∪ range ⇑γ₁
⊢ ∀ i ≤ n + 1, p' i ∈ range ⇑γ

Tactic:
rintro i hi

Result:
case h.left
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPathConnected s
p' : ℕ → X
n : ℕ
hn : (∀ i ≤ n, p' i ∈ s) → ∃ γ, (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s
hp' : ∀ i ≤ n + 1, p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ i ≤ n, p' i ∈ range ⇑γ₀) ∧ range ⇑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := γ₀.trans γ₁
range_eq : range ⇑γ = range ⇑γ₀ ∪ range ⇑γ₁
i : ℕ
hi : i ≤ n + 1
⊢ p' i ∈ range ⇑γ

Proof state:
case h.right
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPathConnected s
p' : ℕ → X
n : ℕ
hn : (∀ i ≤ n, p' i ∈ s) → ∃ γ, (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s
hp' : ∀ i ≤ n + 1, p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ i ≤ n, p' i ∈ range ⇑γ₀) ∧ range ⇑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := γ₀.trans γ₁
range_eq : range ⇑γ = range ⇑γ₀ ∪ range ⇑γ₁
⊢ range ⇑γ₁ ⊆ s

Tactic:
rw [range_subset_iff]

Result:
case h.right
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPathConnected s
p' : ℕ → X
n : ℕ
hn : (∀ i ≤ n, p' i ∈ s) → ∃ γ, (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s
hp' : ∀ i ≤ n + 1, p' i ∈ s
γ₀ : Path (p' 0) (p' n)
hγ₀ : (∀ i ≤ n, p' i ∈ range ⇑γ₀) ∧ range ⇑γ₀ ⊆ s
γ₁ : Path (p' n) (p' (n + 1))
hγ₁ : ∀ (t : ↑I), γ₁ t ∈ s
γ : Path (p' 0) (p' (n + 1)) := γ₀.trans γ₁
range_eq : range ⇑γ = range ⇑γ₀ ∪ range ⇑γ₁
⊢ ∀ (y : ↑I), γ₁ y ∈ s

Proof state:
case h.mk
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 ⟨k, h⟩ else p ⟨0, ⋯⟩
γ : Path (p' 0) (p' n)
hγ : (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s
hpp' : ∀ k < n + 1, p ↑k = p' k
i : ℕ
hi : i < n + 1
⊢ p ⟨i, hi⟩ = p' i

Tactic:
rw [← hpp' i hi]

Result:
case h.mk
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 ⟨k, h⟩ else p ⟨0, ⋯⟩
γ : Path (p' 0) (p' n)
hγ : (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s
hpp' : ∀ k < n + 1, p ↑k = p' k
i : ℕ
hi : i < n + 1
⊢ p ⟨i, hi⟩ = p ↑i