have : i = nfa.nodes.size := Nat.eq_of_le_of_lt_succ (le_of_pathIn_right path) this
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.empty = result
eq : result = nfa.pushNode Node.fail ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path : (↑(nfa.pushNode Node.fail ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode Node.fail ⋯)).start) i w✝¹
step : (↑(nfa.pushNode Node.fail ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this : i < nfa.nodes.size + 1
⊢ Expr.matches cs Expr.empty
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.empty = result
eq : result = nfa.pushNode Node.fail ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path : (↑(nfa.pushNode Node.fail ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode Node.fail ⋯)).start) i w✝¹
step : (↑(nfa.pushNode Node.fail ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this✝ : i < nfa.nodes.size + 1
this : i = nfa.nodes.size
⊢ Expr.matches cs Expr.empty