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

Tactic:
rcases hn fun i hi => hp' i <| Nat.le_succ_of_le hi with ⟨γ₀, hγ₀⟩

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

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 ≤ 0, p' i ∈ range ⇑(Path.refl (p' 0))

Tactic:
rintro i hi

Result:
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' i ∈ range ⇑(Path.refl (p' 0))

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 : i = i % n.succ
⊢ p ⟨i, hi⟩ = p ↑i

Tactic:
congr

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

Tactic:
let p' : ℕ → X := fun k => if h : k < n + 1 then p ⟨k, h⟩ else p ⟨0, n.zero_lt_succ⟩

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

Proof state:
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⟩

Tactic:
rw [Fin.val_cast_of_lt hk]

Result:
no goals

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

Tactic:
have range_eq : range γ = range γ₀ ∪ range γ₁ := γ₀.trans_range γ₁

Result:
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 ≤ n + 1, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ 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:
suffices i = i % n.succ by congr

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
⊢ i = i % n.succ

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
⊢ i = i % n.succ

Tactic:
rw [Nat.mod_eq_of_lt hi]

Result:
no goals

Proof state:
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

Tactic:
constructor

Result:
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 ≤ 0, p' i ∈ range ⇑(Path.refl (p' 0))

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

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
γ : Path (p' 0) (p' (n + 1)) := γ₀.trans γ₁
⊢ ∃ γ, (∀ i ≤ n + 1, p' i ∈ range ⇑γ) ∧ range ⇑γ ⊆ s

Tactic:
use γ

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

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

Tactic:
rcases h.joinedIn (p' n) (hp' n n.le_succ) (p' <| n + 1) (hp' (n + 1) <| le_rfl) with
  ⟨γ₁, hγ₁⟩

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

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' i ∈ range ⇑(Path.refl (p' 0))

Tactic:
rw [Nat.le_zero.mp hi]

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