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
case step.step
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
⊢ nfa.pathToNext 0 1 i (cs ++ (cs₁✝ ++ cs₂✝))
case step.step
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
this : 0 < j
⊢ nfa.pathToNext 0 1 i (cs ++ (cs₁✝ ++ cs₂✝))