cases step with
| charStep _ _ step => simp [node, NFA.Node.charStep] at step
| εStep h₁ h₂ step =>
  apply Or.inr
  have : j = rStart_of eq := by
    simp [node, NFA.Node.εStep] at step
    cases step with
    | inl eq => exact eq
    | inr eq =>
      have : nfa.nodes.size ≤ j := le_of_pathIn_left path
      exact absurd next.isLt (Nat.not_lt_of_le (eq ▸ this))
  subst this
  simp [NFA.Node.εStep]
  have : rStart_of eq ≠ nfa.nodes.size := Nat.ne_of_gt ge
  simp [this] at ih
  exact ih
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
j k : ℕ
cs cs' : List Char
path : (↑result).pathIn nfa.nodes.size j k cs'
ih✝ :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = nfa.nodes.size then
        cs' = [] ∨
          ∃ cs₁ cs₂,
            cs' = cs₁ ++ cs₂ ∧
              (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
      else
        ∃ cs₁ cs₂, cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁ ∧ starLoop eq cs₂
assm₂ : k = nfa.nodes.size
ih :
  if j = nfa.nodes.size then
    cs' = [] ∨
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
  else ∃ cs₁ cs₂, cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁ ∧ starLoop eq cs₂
step : (↑result).stepIn nfa.nodes.size nfa.nodes.size j cs
assm₁ : nfa.nodes.size < (↑result).nodes.size
ge : nfa.nodes.size + 1 ≤ rStart_of eq
node : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq) ↑next
⊢ cs = [] ∧ cs' = [] ∨
    ∃ cs₁ cs₂,
      cs ++ cs' = cs₁ ++ cs₂ ∧
        (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
no goals