-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
lemma getVert_eq_support_get? {u v n} (p : G.Walk u v) (h2 : n ≤ p.length) :
    p.getVert n = p.support[n]?

Proof state:
V : Type u
G : SimpleGraph V
u v✝¹ : V
n : ℕ
p : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
h2 : n ≤ (cons h q).length
⊢ some ((cons h q).getVert n) = (u :: q.support)[n]?

Tactic:
by_cases hn : n = 0

Result:
case pos
V : Type u
G : SimpleGraph V
u v✝¹ : V
n : ℕ
p : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
h2 : n ≤ (cons h q).length
hn : n = 0
⊢ some ((cons h q).getVert n) = (u :: q.support)[n]?

case neg
V : Type u
G : SimpleGraph V
u v✝¹ : V
n : ℕ
p : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
h2 : n ≤ (cons h q).length
hn : ¬n = 0
⊢ some ((cons h q).getVert n) = (u :: q.support)[n]?

Proof state:
V : Type u
G : SimpleGraph V
u v✝¹ : V
n : ℕ
p : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
h2 : n ≤ (cons h q).length
⊢ some ((cons h q).getVert n) = (cons h q).support[n]?

Tactic:
simp only [Walk.support_cons]

Result:
V : Type u
G : SimpleGraph V
u v✝¹ : V
n : ℕ
p : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
h2 : n ≤ (cons h q).length
⊢ some ((cons h q).getVert n) = (u :: q.support)[n]?

Proof state:
case neg
V : Type u
G : SimpleGraph V
u v✝¹ : V
n : ℕ
p : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
h2 : n ≤ (cons h q).length
hn : n ≠ 0
⊢ some ((cons h q).getVert n) = (u :: q.support)[n - 1 + 1]?

Tactic:
rw [Walk.getVert_cons q h hn, List.getElem?_cons_succ]

Result:
case neg
V : Type u
G : SimpleGraph V
u v✝¹ : V
n : ℕ
p : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
h2 : n ≤ (cons h q).length
hn : n ≠ 0
⊢ some (q.getVert (n - 1)) = q.support[n - 1]?

Proof state:
case neg
V : Type u
G : SimpleGraph V
u v✝¹ : V
n : ℕ
p : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
h2 : n ≤ (cons h q).length
hn : n ≠ 0
⊢ some ((cons h q).getVert n) = (u :: q.support)[n]?

Tactic:
nth_rewrite 2 [← Nat.sub_one_add_one hn]

Result:
case neg
V : Type u
G : SimpleGraph V
u v✝¹ : V
n : ℕ
p : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
h2 : n ≤ (cons h q).length
hn : n ≠ 0
⊢ some ((cons h q).getVert n) = (u :: q.support)[n - 1 + 1]?

Proof state:
case neg
V : Type u
G : SimpleGraph V
u v✝¹ : V
n : ℕ
p : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
h2 : n ≤ (cons h q).length
hn : ¬n = 0
⊢ some ((cons h q).getVert n) = (u :: q.support)[n]?

Tactic:
push_neg at hn

Result:
case neg
V : Type u
G : SimpleGraph V
u v✝¹ : V
n : ℕ
p : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
h2 : n ≤ (cons h q).length
hn : n ≠ 0
⊢ some ((cons h q).getVert n) = (u :: q.support)[n]?

Proof state:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h2 : n ≤ nil.length
⊢ some (nil.getVert n) = nil.support[n]?

Tactic:
simp_all

Result:
no goals

Proof state:
case neg
V : Type u
G : SimpleGraph V
u v✝¹ : V
n : ℕ
p : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
h2 : n ≤ (cons h q).length
hn : n ≠ 0
⊢ some (q.getVert (n - 1)) = q.support[n - 1]?

Tactic:
exact getVert_eq_support_get? q (Nat.sub_le_of_le_add (Walk.length_cons _ _ ▸ h2))

Result:
no goals

Proof state:
case pos
V : Type u
G : SimpleGraph V
u v✝¹ : V
n : ℕ
p : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
h2 : n ≤ (cons h q).length
hn : n = 0
⊢ some ((cons h q).getVert n) = (u :: q.support)[n]?

Tactic:
simp only [hn, getVert_zero, List.length_cons, Nat.zero_lt_succ, List.getElem?_eq_getElem,
List.getElem_cons_zero]

Result:
no goals