cases rest with
| base _ =>
  subst assm₂
  exact ⟨i, [], cs, by simp, .base assm₁, step.castStart' assm₁⟩
| step step' rest =>
  have : 0 < j := by
    cases Nat.eq_or_lt_of_le (Nat.zero_le j) with
    | inl eqj =>
      have : 0 < nfa.nodes.size :=
        calc
          0 < 1 := by decide
          _ < _ := (NFA.done.pushRegex ⟨0, by decide⟩ r).property
          _ = _ := by simp [←eq, compile]
      have hn : nfa[0] = .done := by
        simp [←eq]
        unfold compile
        rw [pushRegex_get_lt rfl 0 (by decide)]
        rfl
      simp [eqj] at hn
      cases step'.step <;> simp [hn, NFA.Node.charStep, NFA.Node.εStep] at *
    | inr gt => exact gt
  have ih := ih this assm₂
  apply ih.cons (step.castStart' assm₁)
case step
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn 0 i j cs
rest : nfa.pathIn 0 j k cs'
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j cs'
assm₁ : 0 < i
assm₂ : k = 0
⊢ nfa.pathToNext 0 1 i (cs ++ cs')
no goals