Theorem: TotalDFA.in_language_iff_del_star_final (FormalSystems/Chomsky/Regular/TotalDFA.lean)

State before:
α qs : Type
M : TotalDFA α qs
w : Word { x // x ∈ M.Z }
⊢ w ∈ DFA.AcceptedLanguage M.toDFA ↔ del_star' M (M.q₀, w) ∈ M.F
Tactic:
rw [DFA.in_language_iff_del_star_final, total_del_star_eq]
State after:
α 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

State before:
α 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
Tactic:
simp
State after:
no goals