have := reaches_of_pathIn (i := i') this
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝ : nfa.pathToNext 0 1 (↑nfa.start) cs
this : nfa.pathIn 0 (↑nfa.start) 0 cs
i' : Fin nfa.nodes.size := ⟨0, ⋯⟩
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝¹ : nfa.pathToNext 0 1 (↑nfa.start) cs
this✝ : nfa.pathIn 0 (↑nfa.start) 0 cs
i' : Fin nfa.nodes.size := ⟨0, ⋯⟩
this : nfa.reaches i' cs
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done