rw [DFA.in_language_iff_del_star_final, total_del_star_eq]
α qs : Type
M : TotalDFA α qs
w : Word { x // x ∈ M.Z }
⊢ w ∈ DFA.AcceptedLanguage M.toDFA ↔ del_star' M (M.q₀, w) ∈ M.F
α qs : Type
M : TotalDFA α qs
w : Word { x // x ∈ M.Z }
⊢ (∃ qf ∈ some (del_star' M (M.q₀, w)), qf ∈ M.F) ↔ del_star' M (M.q₀, w) ∈ M.F