case eps h_v h_w =>
  simp [toGrammar, transitionToRule] at h_v
  simp [fromDerivation, NFA.Run.last]
  assumption
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
h_v : RegularProduction.eps s ∈ (toGrammar M).productions
h_w : w = ε
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.eps s h_v h_w)) ∈ M.F
no goals