induction path with
| base _ =>
  subst assm₂
  contradiction
| @step i j k cs cs' step rest ih =>
  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₁)
r : Data.Expr
nfa : NFA
i next : ℕ
cs : List Char
eq : compile r = nfa
assm₁ : 0 < i
assm₂ : next = 0
path : nfa.pathIn 0 i next cs
⊢ nfa.pathToNext 0 1 i cs
no goals