induction r generalizing nfa next cs with
| classes cls =>
  apply pushRegex.sparse eq
  intro eq
  rw [eq] at path
  obtain ⟨i, pcs, scs, eqs, path, step⟩ := path
  have : i < nfa.nodes.size + 1 := by
    have := step.h₂
    simp at this
    exact this
  have : i = nfa.nodes.size := Nat.eq_of_le_of_lt_succ (le_of_pathIn_right path) this
  match step with
  | stepIn.charStep (c := c) _ _ step =>
    simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
    cases path with
    | base _ =>
      simp [eqs]
      exact .sparse cls c step
    | step step rest =>
      cases step with
      | charStep _ _ step =>
        simp [NFA.Node.charStep] at step
        have := le_of_pathIn_left rest
        exact absurd next.isLt (Nat.not_lt_of_ge (step.right ▸ this))
      | εStep _ _ step => simp [NFA.Node.εStep] at step
  | stepIn.εStep _ _ step =>
      simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
| empty =>
  apply pushRegex.empty eq
  intro eq
  rw [eq] at path
  obtain ⟨i, _, _, _, path, step⟩ := path
  have : i < nfa.nodes.size + 1 := by
    have := step.h₂
    simp at this
    exact this
  have : i = nfa.nodes.size := Nat.eq_of_le_of_lt_succ (le_of_pathIn_right path) this
  cases step <;> simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
| epsilon =>
  apply pushRegex.epsilon eq
  intro eq
  rw [eq] at path
  obtain ⟨i, _, _, eqs, path, step⟩ := path
  have : i < nfa.nodes.size + 1 := by
    have := step.h₂
    simp at this
    exact this
  have : i = nfa.nodes.size := Nat.eq_of_le_of_lt_succ (le_of_pathIn_right path) this
  cases step <;> simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
  cases path with
  | base _ => exact eqs ▸ .epsilon
  | step step rest =>
    cases step with
    | charStep _ _ step => simp [NFA.Node.charStep] at step
    | εStep _ _ step =>
      simp [NFA.Node.εStep] at step
      have := le_of_pathIn_left rest
      exact absurd next.isLt (Nat.not_lt_of_ge (step ▸ this))
| char c =>
  apply pushRegex.char eq
  intro eq
  rw [eq] at path
  obtain ⟨i, _, _, _, path, step⟩ := path
  have : i < nfa.nodes.size + 1 := by
    have := step.h₂
    simp at this
    exact this
  have : i = nfa.nodes.size := Nat.eq_of_le_of_lt_succ (le_of_pathIn_right path) this
  cases step <;> simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
  cases path with
  | base _ =>
    simp [*]
    exact .char c
  | step step rest =>
    cases step with
    | charStep _ _ step =>
      simp [NFA.Node.charStep] at step
      have := le_of_pathIn_left rest
      exact absurd next.isLt (Nat.not_lt_of_ge (step.right ▸ this))
    | εStep _ _ step => simp [NFA.Node.εStep] at step
| group i r ih => exact matches_of_path.group eq path ih
| alternate r₁ r₂ ih₁ ih₂ => exact matches_of_path.alternate eq path ih₁ ih₂
| concat r₁ r₂ ih₁ ih₂ => exact matches_of_path.concat eq path ih₁ ih₂
| star r ih => exact matches_of_path.star eq path ih
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next r = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ Expr.matches cs r
no goals