induction path with
| base _ => exact absurd assm₁ (Nat.not_lt_of_le assm₂)
| @step i j k cs cs' step rest ih =>
  have := eq_or_ge_of_step_pushRegex eq assm₂ step.h₂ step.step
  cases this with
  | inl eq =>
    simp [eq] at step rest
    have pathToNext : pathToNext result next nfa.nodes.size i cs :=
      ⟨i, [], cs, rfl, .base assm₂, step.castStart' assm₂⟩
    exact ⟨cs, cs', rfl, pathToNext, rest⟩
  | inr ge =>
    obtain ⟨cs₁, cs₂, eqs, pathToNext, pathIn⟩ := ih assm₁ ge
    exact ⟨cs ++ cs₁, cs₂, by simp [eqs], pathToNext.cons (step.castStart' assm₂), pathIn⟩
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i : ℕ
cs : List Char
start : ℕ
eq : nfa.pushRegex next r = result
assm₁ : i' < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
path : (↑result).pathIn start i i' cs
⊢ ∃ cs₁ cs₂, cs = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) i' cs₂
no goals