rw [eq]
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)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ 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)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ ↑(↑⟨↑nfa''', property⟩).start