simp [eqi]
case inl.intro.εStep
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
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
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : 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' : result = ⟨nfa', property⟩
lt : i < nfa.nodes.size + 1
eqi : i = nfa.nodes.size
left✝ : nfa.nodes.size + 1 ≤ rStart_of eq
node : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq) ↑next
h₁✝ : nfa.nodes.size ≤ i
h₂✝ : i < (↑result).nodes.size
step : ↑next ∈ (↑result)[i].εStep
⊢ i = nfa.nodes.size ∧ [] = []
no goals