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

State before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
⊢ Option.isSome (del_star M (q, w)) = true ↔ Option.isSome (constrRun w q) = true
Tactic:
simp [del_star]
State after:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
⊢ Option.isSome (del_star_curried M w q) = true ↔ Option.isSome (constrRun w q) = true

State before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
⊢ Option.isSome (del_star_curried M w q) = true ↔ Option.isSome (constrRun w q) = true
Tactic:
apply del_star_curried_isSome_iff_constrRun_isSome
State after:
no goals