-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem getVert_reverse {u v : V} (p : G.Walk u v) (i : ℕ) :
    p.reverse.getVert i = p.getVert (p.length - i)

Proof state:
case inl
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert p.length = p.getVert (p.length - p.length)
hi : ¬p.length < p.length
⊢ (cons ⋯ nil).getVert (p.length - p.length) = (cons h p).getVert (p.length + 1 - p.length)

Tactic:
simp [getVert]

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ : V
⊢ nil.reverse.getVert i = nil.getVert (nil.length - i)

Tactic:
rfl

Result:
no goals

Proof state:
case inr
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : ¬i < p.length
hi' : p.length < i
⊢ (cons ⋯ nil).getVert (i - p.length - Nat.succ 0 + Nat.succ 0) = (cons h p).getVert 0

Tactic:
simp [getVert]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : i < p.length
⊢ p.getVert (p.length - i) = (cons h p).getVert (p.length - i).succ

Tactic:
simp [getVert]

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
⊢ (if i < p.length then p.getVert (p.length - i) else (cons ⋯ nil).getVert (i - p.length)) =
    (cons h p).getVert (p.length + 1 - i)

Tactic:
split_ifs

Result:
case pos
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
h✝ : i < p.length
⊢ p.getVert (p.length - i) = (cons h p).getVert (p.length + 1 - i)

case neg
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
h✝ : ¬i < p.length
⊢ (cons ⋯ nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)

Proof state:
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : ¬i < p.length
⊢ (cons ⋯ nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)

Tactic:
obtain rfl | hi' := Nat.eq_or_lt_of_not_lt hi

Result:
case inl
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert p.length = p.getVert (p.length - p.length)
hi : ¬p.length < p.length
⊢ (cons ⋯ nil).getVert (p.length - p.length) = (cons h p).getVert (p.length + 1 - p.length)

case inr
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : ¬i < p.length
hi' : p.length < i
⊢ (cons ⋯ nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)

Proof state:
case pos
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
h✝ : i < p.length
⊢ p.getVert (p.length - i) = (cons h p).getVert (p.length + 1 - i)

case neg
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
h✝ : ¬i < p.length
⊢ (cons ⋯ nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)

Tactic:
next hi =>
  rw [Nat.succ_sub hi.le]
  simp [getVert]

Result:
case neg
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
h✝ : ¬i < p.length
⊢ (cons ⋯ nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)

Proof state:
case inr
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : ¬i < p.length
hi' : p.length < i
⊢ (cons ⋯ nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)

Tactic:
rw [Nat.eq_add_of_sub_eq (Nat.sub_pos_of_lt hi') rfl, Nat.sub_eq_zero_of_le hi']

Result:
case inr
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : ¬i < p.length
hi' : p.length < i
⊢ (cons ⋯ nil).getVert (i - p.length - Nat.succ 0 + Nat.succ 0) = (cons h p).getVert 0

Proof state:
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : i < p.length
⊢ p.getVert (p.length - i) = (cons h p).getVert (p.length + 1 - i)

Tactic:
rw [Nat.succ_sub hi.le]

Result:
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : i < p.length
⊢ p.getVert (p.length - i) = (cons h p).getVert (p.length - i).succ

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
⊢ (cons h p).reverse.getVert i = (cons h p).getVert ((cons h p).length - i)

Tactic:
simp only [reverse_cons, getVert_append, length_reverse, ih, length_cons]

Result:
case cons
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
⊢ (if i < p.length then p.getVert (p.length - i) else (cons ⋯ nil).getVert (i - p.length)) =
    (cons h p).getVert (p.length + 1 - i)