-- 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 pos
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 [range_eq]

Result:
case pos
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 ⇑γ₀ ∪ 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 ⇑γ₁
⊢ ∀ (y : ↑I), γ₁ y ∈ s

Tactic:
exact hγ₁

Result:
no goals

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 ≤ n, p' i ∈ s

Tactic:
intro i hi

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, ⋯⟩
i : ℕ
hi : i ≤ n
⊢ p' i ∈ 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, ⋯⟩
γ : 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
this : p ⟨i, hi⟩ = p' i
⊢ p ⟨i, hi⟩ ∈ range ⇑γ

Tactic:
convert hγ.1 i (Nat.le_of_lt_succ hi)

Result:
no goals

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, hk⟩

Tactic:
congr

Result:
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⟩

Proof state:
case h.right
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp' : ∀ i ≤ 0, p' i ∈ s
_x : ↑I
⊢ (Path.refl (p' 0)) _x ∈ s

Tactic:
exact hp' 0 le_rfl

Result:
no goals

Proof state:
case intro
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
⊢ ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ

Tactic:
have hpp' : ∀ k < n + 1, p k = p' k := by
  intro k hk
  simp only [p', hk, dif_pos]
  congr
  ext
  rw [Fin.val_cast_of_lt hk]

Result:
case intro
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
⊢ ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ

Proof state:
case pos
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 ⇑γ₀ ∪ range ⇑γ₁

Tactic:
left

Result:
case pos.h
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 ⇑γ₀

Proof state:
case pos.h
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:
exact hγ₀.1 i hi'

Result:
no goals

Proof state:
case h.right
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp' : ∀ i ≤ 0, p' i ∈ s
⊢ range ⇑(Path.refl (p' 0)) ⊆ 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
hp' : ∀ i ≤ 0, p' i ∈ s
⊢ ∀ (y : ↑I), (Path.refl (p' 0)) y ∈ s