simp [DFA.fromNFA]
case w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ ↑{ val := {w✝}, property := ⋯ } ⊆ ↑(DFA.fromNFA M).q₀

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted (DFA.fromNFA.NFARunToRun run) ?w.h) ∈ (DFA.fromNFA M).F
case w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ w✝ ∈ M.Q₀

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted (DFA.fromNFA.NFARunToRun run) ⋯) ∈ (DFA.fromNFA M).F