-- 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 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' : n.succ ≤ i
this : i = n.succ
⊢ γ 1 = p' n.succ

Tactic:
exact γ.target

Result:
no goals

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 ⇑γ₀ ∪ range ⇑γ₁ ⊆ s

Tactic:
apply union_subset hγ₀.2

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 ⇑γ₁ ⊆ s

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

Tactic:
refine And.intro hγ.2 ?_

Result:
case 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
hpp' : ∀ k < n + 1, p ↑k = p' k
⊢ ∀ (i : Fin (n + 1)), 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' : n.succ ≤ i
this : i = n.succ
⊢ p' i ∈ range ⇑γ

Tactic:
rw [this]

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
this : i = n.succ
⊢ p' n.succ ∈ 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 < n + 1, p ↑k = p' k

Tactic:
intro k hk

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

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
hpp' : ∀ k < n + 1, p ↑k = p' k
⊢ ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ

Tactic:
use γ.cast (hpp' 0 n.zero_lt_succ) (hpp' n n.lt_succ_self)

Result:
case 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
hpp' : ∀ k < n + 1, p ↑k = p' k
⊢ range ⇑(γ.cast ⋯ ⋯) ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ⇑(γ.cast ⋯ ⋯)

Proof state:
case h.left
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp' : ∀ i ≤ 0, p' i ∈ s
i : ℕ
hi : i ≤ 0
⊢ p' 0 ∈ range ⇑(Path.refl (p' 0))

Tactic:
exact ⟨0, rfl⟩

Result:
no goals

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

Tactic:
let γ : Path (p' 0) (p' <| n + 1) := γ₀.trans γ₁

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

Proof state:
case 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
hpp' : ∀ k < n + 1, p ↑k = p' k
⊢ ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ

Tactic:
rintro ⟨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⟩ ∈ 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, ⋯⟩
⊢ ∃ γ, (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s

Tactic:
have hp' : ∀ i ≤ n, p' i ∈ s := by
  intro i hi
  simp [p', Nat.lt_succ_of_le hi, hp]

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, ⋯⟩
hp' : ∀ i ≤ n, p' i ∈ s
⊢ ∃ γ, (∀ i ≤ n, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s

Proof state:
case zero
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp' : ∀ i ≤ 0, p' i ∈ s
⊢ ∃ γ, (∀ i ≤ 0, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s

Tactic:
use Path.refl (p' 0)

Result:
case h
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPathConnected s
p' : ℕ → X
hp' : ∀ i ≤ 0, p' i ∈ s
⊢ (∀ i ≤ 0, p' i ∈ range ⇑(Path.refl (p' 0))) ∧ range ⇑(Path.refl (p' 0)) ⊆ s