match step with
| stepIn.charStep (c := c) _ _ step =>
  simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
  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
| stepIn.εStep _ _ step =>
    simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
case intro.intro.intro.intro.intro
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
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
this✝ : i < nfa.nodes.size + 1
this : i = nfa.nodes.size
⊢ Expr.matches cs (Expr.classes cls)
no goals