have := pathToNext_of_compile_of_pathIn eq (hi ▸ this)
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
cs : List Char
eq : compile r = nfa
h₁ : nfa.reaches i cs
h₂ : nfa[i] = Node.done
hi : ↑i = 0
this : nfa.pathIn 0 (↑nfa.start) (↑i) cs
⊢ Data.Expr.matches cs r
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
cs : List Char
eq : compile r = nfa
h₁ : nfa.reaches i cs
h₂ : nfa[i] = Node.done
hi : ↑i = 0
this✝ : nfa.pathIn 0 (↑nfa.start) (↑i) cs
this : nfa.pathToNext 0 1 (↑nfa.start) cs
⊢ Data.Expr.matches cs r