exact pathToNext_of_matches.group eq ih
case group
r : Data.Expr
cs s✝ : List Char
r✝ : Data.Expr
i✝ : ℕ
m✝ : Data.Expr.matches s✝ r✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r✝ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) s✝
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.group i✝ r✝) = nfa'
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) s✝
no goals