Theorem: Digraph.Walk.getVert_of_length_le (GraphProjects/DigraphConnectivity.lean)

State before:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ : V
i : ℕ
hi : length nil ≤ i
⊢ getVert nil i = u✝
Tactic:
rfl
State after:
no goals

State before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, length p✝ ≤ i → getVert p✝ i = w✝
i : ℕ
hi : length (cons h✝ p✝) ≤ i
⊢ getVert (cons h✝ p✝) i = w✝
Tactic:
cases i
State after:
case cons.zero
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, length p✝ ≤ i → getVert p✝ i = w✝
hi : length (cons h✝ p✝) ≤ Nat.zero
⊢ getVert (cons h✝ p✝) Nat.zero = w✝

case cons.succ
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, length p✝ ≤ i → getVert p✝ i = w✝
n✝ : ℕ
hi : length (cons h✝ p✝) ≤ Nat.succ n✝
⊢ getVert (cons h✝ p✝) (Nat.succ n✝) = w✝

State before:
case cons.zero
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, length p✝ ≤ i → getVert p✝ i = w✝
hi : length (cons h✝ p✝) ≤ Nat.zero
⊢ getVert (cons h✝ p✝) Nat.zero = w✝
Tactic:
cases hi
State after:
no goals

State before:
case cons.succ
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, length p✝ ≤ i → getVert p✝ i = w✝
n✝ : ℕ
hi : length (cons h✝ p✝) ≤ Nat.succ n✝
⊢ getVert (cons h✝ p✝) (Nat.succ n✝) = w✝
Tactic:
exact ih (Nat.succ_le_succ_iff.1 hi)
State after:
no goals