match r with
| .final _ _ =>
  dsimp [NFA.Run.last, fromNFA] at h
  have ⟨_, qf, _, _⟩ := Finset.mem_filter.mp h
  exists qf; constructor; assumption
  apply Exists.intro; swap
  apply NFA.Run.final _
  assumption
  dsimp [NFA.Run.last]
  assumption
| .step _ h_step _ _ =>
  dsimp [NFA.Run.last] at h
  dsimp [fromNFA, toNFA] at h_step; simp at h_step
  have ⟨_, h_q₂, r', hr'⟩ := fromNFA_run_imp_run h
  rw [h_step, Finset.mem_fold_union_iff] at h_q₂
  have ⟨x, _, _⟩ := h_q₂
  exists x; constructor; assumption
  apply Exists.intro; swap
  apply NFA.Run.step
  repeat { assumption }
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h : NFA.Run.last r ∈ (fromNFA M).F
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F
no goals