-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
theorem toSubgraph_adj_getVert {u v} (w : G.Walk u v) {i : ℕ} (hi : i < w.length) :
    w.toSubgraph.Adj (w.getVert i) (w.getVert (i + 1))

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
i : ℕ
hi : i < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert i) ((cons hxy i').getVert (i + 1))

Tactic:
cases i

Result:
case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
hi : 0 < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert 0) ((cons hxy i').getVert (0 + 1))

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert (n✝ + 1)) ((cons hxy i').getVert (n✝ + 1 + 1))

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
i : ℕ
hi : i < nil.length
⊢ nil.toSubgraph.Adj (nil.getVert i) (nil.getVert (i + 1))

Tactic:
cases hi

Result:
no goals

Proof state:
case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert (n✝ + 1)) ((cons hxy i').getVert (n✝ + 1 + 1))

Tactic:
simp only [Walk.toSubgraph, getVert_cons_succ, Subgraph.sup_adj, subgraphOfAdj_adj, Sym2.eq,
  Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]

Result:
case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy i').length
⊢ (u✝ = i'.getVert n✝ ∧ v✝ = i'.getVert (n✝ + 1) ∨ u✝ = i'.getVert (n✝ + 1) ∧ v✝ = i'.getVert n✝) ∨
    i'.toSubgraph.Adj (i'.getVert n✝) (i'.getVert (n✝ + 1))

Proof state:
case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy i').length
⊢ (u✝ = i'.getVert n✝ ∧ v✝ = i'.getVert (n✝ + 1) ∨ u✝ = i'.getVert (n✝ + 1) ∧ v✝ = i'.getVert n✝) ∨
    i'.toSubgraph.Adj (i'.getVert n✝) (i'.getVert (n✝ + 1))

Tactic:
right

Result:
case cons.succ.h
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy i').length
⊢ i'.toSubgraph.Adj (i'.getVert n✝) (i'.getVert (n✝ + 1))

Proof state:
case cons.succ.h
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy i').length
⊢ i'.toSubgraph.Adj (i'.getVert n✝) (i'.getVert (n✝ + 1))

Tactic:
exact ih (Nat.succ_lt_succ_iff.mp hi)

Result:
no goals

Proof state:
case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
hi : 0 < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert 0) ((cons hxy i').getVert (0 + 1))

Tactic:
simp only [Walk.toSubgraph, Walk.getVert_zero, zero_add, getVert_cons_succ, Subgraph.sup_adj,
  subgraphOfAdj_adj, true_or]

Result:
no goals