no goals
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v u✝ : V
i : ℕ
hi : i < length nil
⊢ Adj G (getVert nil i) (getVert nil (i + 1))
cases hi
case cons.zero
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v u✝ v✝ w✝ : V
hxy : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, i < length p✝ → Adj G (getVert p✝ i) (getVert p✝ (i + 1))
hi : Nat.zero < length (cons hxy p✝)
⊢ Adj G (getVert (cons hxy p✝) Nat.zero) (getVert (cons hxy p✝) (Nat.zero + 1))

case cons.succ
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v u✝ v✝ w✝ : V
hxy : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, i < length p✝ → Adj G (getVert p✝ i) (getVert p✝ (i + 1))
n✝ : ℕ
hi : Nat.succ n✝ < length (cons hxy p✝)
⊢ Adj G (getVert (cons hxy p✝) (Nat.succ n✝)) (getVert (cons hxy p✝) (Nat.succ n✝ + 1))
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v u✝ v✝ w✝ : V
hxy : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, i < length p✝ → Adj G (getVert p✝ i) (getVert p✝ (i + 1))
i : ℕ
hi : i < length (cons hxy p✝)
⊢ Adj G (getVert (cons hxy p✝) i) (getVert (cons hxy p✝) (i + 1))
cases i
no goals
case cons.zero
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v u✝ v✝ w✝ : V
hxy : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, i < length p✝ → Adj G (getVert p✝ i) (getVert p✝ (i + 1))
hi : Nat.zero < length (cons hxy p✝)
⊢ Adj G (getVert (cons hxy p✝) Nat.zero) (getVert (cons hxy p✝) (Nat.zero + 1))
simp [getVert, hxy]
no goals
case cons.succ
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v u✝ v✝ w✝ : V
hxy : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, i < length p✝ → Adj G (getVert p✝ i) (getVert p✝ (i + 1))
n✝ : ℕ
hi : Nat.succ n✝ < length (cons hxy p✝)
⊢ Adj G (getVert (cons hxy p✝) (Nat.succ n✝)) (getVert (cons hxy p✝) (Nat.succ n✝ + 1))
exact ih (Nat.succ_lt_succ_iff.1 hi)