exact ⟨cs₁, cs₂, rfl, path'.cons (.εStep gti h₂ step), loop⟩
case intro.intro.intro.intro.εStep
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
nej : ¬j = nfa.nodes.size
cs₁ cs₂ : List Char
path' : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁
loop : starLoop eq cs₂
path : (↑result).pathIn nfa.nodes.size j k (cs₁ ++ cs₂)
ih :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = nfa.nodes.size then
        cs₁ ++ cs₂ = [] ∨
          ∃ cs₁_1 cs₂_1,
            cs₁ ++ cs₂ = cs₁_1 ++ cs₂_1 ∧
              (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁_1 ∧ starLoop eq cs₂_1
      else
        ∃ cs₁_1 cs₂_1,
          cs₁ ++ cs₂ = cs₁_1 ++ cs₂_1 ∧
            (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁_1 ∧ starLoop eq cs₂_1
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : j ∈ (↑result)[i].εStep
⊢ ∃ cs₁_1 cs₂_1,
    [] ++ (cs₁ ++ cs₂) = cs₁_1 ++ cs₂_1 ∧
      (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁_1 ∧ starLoop eq cs₂_1
no goals