simp [fromDerivation, NFA.Run.last]
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
a✝¹ : { x // x ∈ (toGrammar M).Z }
w'✝ : List { x // x ∈ (toGrammar M).Z }
v'✝ : { x // x ∈ (toGrammar M).V }
a✝ : RegularGrammar.RegularDerivation (toGrammar M) v'✝ w'✝
h✝ : RegularProduction.cons s (a✝¹, v'✝) ∈ (toGrammar M).productions
h_w : w = a✝¹ :: w'✝
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.step s v'✝ h✝ h_w a✝)) ∈ M.F
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
a✝¹ : { x // x ∈ (toGrammar M).Z }
w'✝ : List { x // x ∈ (toGrammar M).Z }
v'✝ : { x // x ∈ (toGrammar M).V }
a✝ : RegularGrammar.RegularDerivation (toGrammar M) v'✝ w'✝
h✝ : RegularProduction.cons s (a✝¹, v'✝) ∈ (toGrammar M).productions
h_w : w = a✝¹ :: w'✝
⊢ NFA.Run.last (fromDerivation M a✝) ∈ M.F