rw [eq] at path
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
⊢ Expr.matches cs (Expr.classes cls)
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathToNext (↑next) nfa.nodes.size
    (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start) cs
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
⊢ Expr.matches cs (Expr.classes cls)