rw [eq]
r : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = 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 r.star = result
placeholder✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled✝ : { nfa' // (↑placeholder✝).nodes.size < nfa'.nodes.size }
patched✝ : Array Node
nfa' : NFA
isLt✝ : nfa.nodes.size < patched✝.size
inBounds✝ : ∀ (i : Fin patched✝.size), patched✝[↑i].inBounds patched✝.size
property✝ : nfa.nodes.size < nfa'.nodes.size
a✝² : placeholder✝ = nfa.pushNode Node.fail ⋯
a✝¹ : compiled✝ = (↑placeholder✝).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
a✝ : patched✝ = (↑compiled✝).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled✝).start ↑next)
eq₄ : nfa' = { nodes := patched✝, start := ⟨nfa.nodes.size, isLt✝⟩, inBounds := inBounds✝ }
eq : result = ⟨nfa', property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑result).start
r : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = 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 r.star = result
placeholder✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled✝ : { nfa' // (↑placeholder✝).nodes.size < nfa'.nodes.size }
patched✝ : Array Node
nfa' : NFA
isLt✝ : nfa.nodes.size < patched✝.size
inBounds✝ : ∀ (i : Fin patched✝.size), patched✝[↑i].inBounds patched✝.size
property✝ : nfa.nodes.size < nfa'.nodes.size
a✝² : placeholder✝ = nfa.pushNode Node.fail ⋯
a✝¹ : compiled✝ = (↑placeholder✝).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
a✝ : patched✝ = (↑compiled✝).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled✝).start ↑next)
eq₄ : nfa' = { nodes := patched✝, start := ⟨nfa.nodes.size, isLt✝⟩, inBounds := inBounds✝ }
eq : result = ⟨nfa', property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑⟨nfa', property✝⟩).start