Theorem: DFA.last_state_eq_del_star (FormalSystems/Chomsky/Regular/DFA.lean)

State before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ (toNFA M).Q }
r : NFA.Run (toNFA M) q w
⊢ del_star M (q, w) = some (NFA.Run.last r)
Tactic:
simp [del_star]
State after:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ (toNFA M).Q }
r : NFA.Run (toNFA M) q w
⊢ del_star_curried M w q = some (NFA.Run.last r)

State before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ (toNFA M).Q }
r : NFA.Run (toNFA M) q w
⊢ del_star_curried M w q = some (NFA.Run.last r)
Tactic:
apply last_state_eq_del_star_curried
State after:
no goals