rw [eq₄]
r : Data.Expr
cs : List Char
r✝ : Data.Expr
nfa : NFA
next : Fin nfa.nodes.size
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r✝.star = nfa'✝
this : nfa.nodes.size ≤ ↑(↑nfa'✝).start
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✝
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
⊢ ↑nfa'.start = nfa.nodes.size
no goals