cases path with
| base _ =>
  simp [eqs]
  exact .sparse cls c step
| step step rest =>
  cases step with
  | charStep _ _ step =>
    simp [NFA.Node.charStep] at step
    have := le_of_pathIn_left rest
    exact absurd next.isLt (Nat.not_lt_of_ge (step.right ▸ this))
  | εStep _ _ step => simp [NFA.Node.εStep] at step
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
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
c : Char
h₂✝ : i < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
eqs : cs = pcs ++ [c]
path : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size pcs
step✝ : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size nfa.nodes.size (↑next) scs
this✝ this h₁✝ : True
step : c ∈ cls
⊢ Expr.matches cs (Expr.classes cls)
no goals