apply pushRegex.group eq
case group
a✝¹ : ℕ
a✝ : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.group a✝¹ a✝) = result
⊢ nfa.nodes.size ≤ ↑(↑result).start
a✝¹ : ℕ
a✝ : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.group a✝¹ a✝) = result
⊢ ∀ (nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size })
    (nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }) (property : nfa.nodes.size < (↑nfa''').nodes.size)
    (inBounds' : (Node.save (2 * a✝¹ + 1) ↑next).inBounds (nfa.nodes.size + 1))
    (inBounds''' : (Node.save (2 * a✝¹) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)),
    nfa' = nfa.pushNode (Node.save (2 * a✝¹ + 1) ↑next) inBounds' →
      nfa'' = (↑nfa').pushRegex (↑nfa').start a✝ →
        nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝¹) ↑(↑nfa'').start) inBounds''' →
          result = ⟨↑nfa''', property⟩ → nfa.nodes.size ≤ ↑(↑result).start