match d with
| .eps (v:=v) _ _ =>
  simp [last, toNFA]
  exists .eps v
| .alpha _ _ _ =>
  simp [last, fromDerivation, Fintype.wrap, toNFA]
| .step _ _ _ _ _ =>
  simp [last]
  apply fromDerivation_last_in_final
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
v✝ : { x // x ∈ G.V }
w✝ : Word { x // x ∈ (toNFA G).Z }
d : RegularDerivation G v✝ w✝
⊢ last (fromDerivation G d) ∈ (toNFA G).F
no goals