case step r' incl w_cast =>
  unfold NFA.Run.last
  rw [w_cast]
  unfold del_star_curried
  simp_rw [toNFA, Function.comp_apply] at incl
  rw [Option.mem_toFinset, Option.mem_iff] at incl
  rw [incl, Option.bind_eq_bind, Option.some_bind]
  apply last_state_eq_del_star_curried
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ (toNFA M).δ (q, a✝)
w_cast : w = a✝ :: w✝
⊢ del_star_curried M w q = some (NFA.Run.last (NFA.Run.step q incl r' w_cast))
no goals