apply NFA.Run.fromDerivation_last_in_final
case h.right.h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ NFA.Run.last ?h.right.w ∈ (toNFA G).F

case h.right.w
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ NFA.Run (toNFA G) { val := Sum.inl G.start, property := ⋯ } w
case h.right.h.d
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ RegularDerivation G G.start w