rw [←eq]
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathToNext 0 1 (↑nfa.start) cs
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
⊢ nfa = ↑result
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathToNext 0 1 (↑nfa.start) cs
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
⊢ compile r = ↑result