cases step with
| charStep _ _ step => simp [NFA.Node.charStep] at step
| εStep _ _ step =>
  simp [NFA.Node.εStep] at step
  have := le_of_pathIn_left rest
  exact absurd next.isLt (Nat.not_lt_of_ge (step ▸ this))
case intro.intro.intro.intro.intro.εStep.step
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
h₂✝ : i < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
this✝ this h₁✝ step✝ : True
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).stepIn nfa.nodes.size nfa.nodes.size j✝ cs₁✝
rest : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
eqs : cs = cs₁✝ ++ cs₂✝
⊢ Expr.matches cs Expr.epsilon
no goals