Theorem: DFA.last_state_eq_del_star_curried (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_curried M w q = some (NFA.Run.last r)
Tactic:
cases r
State after:
case final
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ (toNFA M).Q }
h✝ : w = ε
⊢ del_star_curried M w q = some (NFA.Run.last (NFA.Run.final q h✝))

case step
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r✝ : NFA.Run (toNFA M) q₂✝ w✝
x✝ : q₂✝ ∈ (toNFA M).δ (q, a✝)
h✝ : w = a✝ :: w✝
⊢ del_star_curried M w q = some (NFA.Run.last (NFA.Run.step q x✝ r✝ h✝))

State before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ (toNFA M).Q }
h : w = ε
⊢ del_star_curried M w q = some (NFA.Run.last (NFA.Run.final q h))
Tactic:
case final h =>
  simp_rw [h, del_star_curried, NFA.Run.last]
State after:
no goals

State before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ (toNFA M).δ (q, a✝)
w_cast : w = a✝ :: w✝
⊢ del_star_curried M w q = some (NFA.Run.last (NFA.Run.step q incl r' w_cast))
Tactic:
case step r' incl w_cast =>
  unfold NFA.Run.last
  rw [w_cast]
  unfold del_star_curried
  simp_rw [toNFA, Function.comp_apply] at incl
  rw [Option.mem_toFinset, Option.mem_iff] at incl
  rw [incl, Option.bind_eq_bind, Option.some_bind]
  apply last_state_eq_del_star_curried
State after:
no goals

State before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ (toNFA M).Q }
h : w = ε
⊢ del_star_curried M w q = some (NFA.Run.last (NFA.Run.final q h))
Tactic:
simp_rw [h, del_star_curried, NFA.Run.last]
State after:
no goals

State before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ (toNFA M).δ (q, a✝)
w_cast : w = a✝ :: w✝
⊢ del_star_curried M w q = some (NFA.Run.last (NFA.Run.step q incl r' w_cast))
Tactic:
unfold NFA.Run.last
State after:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ (toNFA M).δ (q, a✝)
w_cast : w = a✝ :: 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 q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ (toNFA M).δ (q, a✝)
w_cast : w = a✝ :: w✝
⊢ del_star_curried M w q = some (NFA.Run.last r')
Tactic:
rw [w_cast]
State after:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ (toNFA M).δ (q, a✝)
w_cast : w = a✝ :: w✝
⊢ del_star_curried M (a✝ :: w✝) q = some (NFA.Run.last r')

State before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ (toNFA M).δ (q, a✝)
w_cast : w = a✝ :: w✝
⊢ del_star_curried M (a✝ :: w✝) q = some (NFA.Run.last r')
Tactic:
unfold del_star_curried
State after:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ (toNFA M).δ (q, a✝)
w_cast : w = a✝ :: w✝
⊢ M.δ (q, a✝) >>= del_star_curried M w✝ = some (NFA.Run.last r')

State before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ (toNFA M).δ (q, a✝)
w_cast : w = a✝ :: w✝
⊢ M.δ (q, a✝) >>= del_star_curried M w✝ = some (NFA.Run.last r')
Tactic:
simp_rw [toNFA, Function.comp_apply] at incl
State after:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ Option.toFinset (M.δ (q, a✝))
w_cast : w = a✝ :: w✝
⊢ M.δ (q, a✝) >>= del_star_curried M w✝ = some (NFA.Run.last r')

State before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ Option.toFinset (M.δ (q, a✝))
w_cast : w = a✝ :: w✝
⊢ M.δ (q, a✝) >>= del_star_curried M w✝ = some (NFA.Run.last r')
Tactic:
rw [Option.mem_toFinset, Option.mem_iff] at incl
State after:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : M.δ (q, a✝) = some q₂✝
w_cast : w = a✝ :: w✝
⊢ M.δ (q, a✝) >>= del_star_curried M w✝ = some (NFA.Run.last r')

State before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : M.δ (q, a✝) = some q₂✝
w_cast : w = a✝ :: w✝
⊢ M.δ (q, a✝) >>= del_star_curried M w✝ = some (NFA.Run.last r')
Tactic:
rw [incl, Option.bind_eq_bind, Option.some_bind]
State after:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : M.δ (q, a✝) = some q₂✝
w_cast : w = a✝ :: 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 q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : M.δ (q, a✝) = some q₂✝
w_cast : w = a✝ :: w✝
⊢ del_star_curried M w✝ q₂✝ = some (NFA.Run.last r')
Tactic:
apply last_state_eq_del_star_curried
State after:
no goals