have : 0 < nfa.start.val := by
  rw [←eq, compile]
  exact ge_pushRegex_start (rfl : NFA.done.pushRegex _ r = _)
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathIn 0 (↑nfa.start) 0 cs
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathIn 0 (↑nfa.start) 0 cs
this : 0 < ↑nfa.start
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs