This proof really should be

Can you add simp lemmas until something of the above works?

simpa using adj_getVert_succ p (by simpa : 0 < p.length) works except for the second simpa, but simping "not nil" to "0 < p.length" seems pretty impactful, are you sure we want to be doing that?

I managed to get it to this:

@[simp] lemma adj_getVert_one {p : G.Walk v w} (hp : ¬ p.Nil) :
    G.Adj v (p.getVert 1) := by
  have := adj_getVert_succ p (by simpa [not_nil_iff_lt_length] using hp)
  simp only [getVert_zero, zero_add] at this
  exact this

which works

but

@[simp] lemma adj_getVert_one {p : G.Walk v w} (hp : ¬ p.Nil) :
    G.Adj v (p.getVert 1) := by
  simpa [getVert_zero, zero_add] using adj_getVert_succ p (by simpa [not_nil_iff_lt_length] using hp)

errors with

type mismatch
  h✝
has type
  G.Adj (p.getVert 0) (p.getVert (0 + 1)) : Prop
but is expected to have type
  G.Adj v (p.getVert 1) : Prop

Any clue what's going on here?

Hmm... no clue, no. If you manage to minimise it, try posting it on #mathlib4 or #lean4 (depending on whether you got rid of the mathlib dependencies or not)

Type hinting the second simpa works. I don't think there's a bug with simpa, since using rwa in the second part leads to the same problem. Fixed in it that way

Probably some metavariable instantiating too late