case alpha h_v _ =>
  simp [toGrammar, transitionToRule] at h_v
α 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 }
h_v : RegularProduction.alpha s a✝ ∈ (toGrammar M).productions
h_w✝ : w = [a✝]
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.alpha s h_v h_w✝)) ∈ M.F
no goals