rw [pushRegex_get_lt eq₁.symm]
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.concat r₂) = result
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₁
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₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
path : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq' : result = ⟨↑nfa₁, property⟩
i : ℕ
x✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa₂).nodes.size
⊢ (↑nfa₂)[i] = (↑nfa₁)[i]
no goals