induction m generalizing nfa next with
| sparse cls c hmem =>
  have : nfa.nodes.size ≤ nfa'.val.start.val := ge_pushRegex_start eq
  refine ⟨
    nfa'.val.start,
    [],
    [c],
    rfl,
    .base this,
    .charStep this nfa'.val.start.isLt ?_
  ⟩
  rw [←eq]
  simp [pushRegex, Node.charStep, hmem]
| char c =>
  have : nfa.nodes.size ≤ nfa'.val.start.val := ge_pushRegex_start eq
  refine ⟨
    nfa'.val.start,
    [],
    [c],
    rfl,
    .base this,
    .charStep this nfa'.val.start.isLt ?_
  ⟩
  rw [←eq]
  simp [pushRegex, Node.charStep]
| epsilon =>
  have : nfa.nodes.size ≤ nfa'.val.start.val := ge_pushRegex_start eq
  refine ⟨nfa'.val.start, [], [], rfl, .base this, .εStep this nfa'.val.start.isLt ?_⟩
  rw [←eq]
  simp [pushRegex, Node.εStep]
| group _ ih => exact pathToNext_of_matches.group eq ih
| alternateLeft _ ih => exact pathToNext_of_matches.alternateLeft eq ih
| alternateRight _ ih => exact pathToNext_of_matches.alternateRight eq ih
| concat cs₁ cs₂ r₁ r₂ _ _ ih₁ ih₂ => exact pathToNext_of_matches.concat eq ih₁ ih₂
| starEpsilon =>
  have : nfa.nodes.size ≤ nfa'.val.start.val := ge_pushRegex_start eq
  refine ⟨nfa'.val.start, [], [], rfl, .base this, .εStep this nfa'.val.start.isLt ?_⟩
  apply pushRegex.star eq
  intro placeholder compiled patched nfa' isLt inBounds property
    _ _ eq₃ eq₄ eq
  rw[eq]
  have : nfa'.start.val = nfa.nodes.size := by
    rw [eq₄]
  simp [this, eq₄, get_eq_nodes_get, eq₃, Node.εStep]
| starConcat cs₁ cs₂ r _ _ ih₁ ih₂ => exact pathToNext_of_matches.starConcat eq ih₁ ih₂
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next r = nfa'
m : Data.Expr.matches cs r
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
no goals