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

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

State before:
α qs : Type
M : TotalDFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
⊢ DFA.del_star_curried M.toDFA w q = some (del_star' M (q, w))
Tactic:
induction w generalizing q
State after:
case nil
α qs : Type
M : TotalDFA α qs
q : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M.toDFA [] q = some (del_star' M (q, []))

case cons
α qs : Type
M : TotalDFA α qs
head✝ : { x // x ∈ M.Z }
tail✝ : List { x // x ∈ M.Z }
tail_ih✝ : ∀ {q : { x // x ∈ M.Q }}, DFA.del_star_curried M.toDFA tail✝ q = some (del_star' M (q, tail✝))
q : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M.toDFA (head✝ :: tail✝) q = some (del_star' M (q, head✝ :: tail✝))

State before:
α qs : Type
M : TotalDFA α qs
q : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M.toDFA [] q = some (del_star' M (q, []))
Tactic:
case nil => rfl
State after:
no goals

State before:
α qs : Type
M : TotalDFA α qs
head✝ : { x // x ∈ M.Z }
tail✝ : List { x // x ∈ M.Z }
ih : ∀ {q : { x // x ∈ M.Q }}, DFA.del_star_curried M.toDFA tail✝ q = some (del_star' M (q, tail✝))
q : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M.toDFA (head✝ :: tail✝) q = some (del_star' M (q, head✝ :: tail✝))
Tactic:
case cons _ _ ih =>
  unfold DFA.del_star_curried
  rw [total_del_eq] 
  apply ih
State after:
no goals

State before:
α qs : Type
M : TotalDFA α qs
q : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M.toDFA [] q = some (del_star' M (q, []))
Tactic:
rfl
State after:
no goals

State before:
α qs : Type
M : TotalDFA α qs
head✝ : { x // x ∈ M.Z }
tail✝ : List { x // x ∈ M.Z }
ih : ∀ {q : { x // x ∈ M.Q }}, DFA.del_star_curried M.toDFA tail✝ q = some (del_star' M (q, tail✝))
q : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M.toDFA (head✝ :: tail✝) q = some (del_star' M (q, head✝ :: tail✝))
Tactic:
unfold DFA.del_star_curried
State after:
α qs : Type
M : TotalDFA α qs
head✝ : { x // x ∈ M.Z }
tail✝ : List { x // x ∈ M.Z }
ih : ∀ {q : { x // x ∈ M.Q }}, DFA.del_star_curried M.toDFA tail✝ q = some (del_star' M (q, tail✝))
q : { x // x ∈ M.Q }
⊢ M.δ (q, head✝) >>= DFA.del_star_curried M.toDFA tail✝ = some (del_star' M (q, head✝ :: tail✝))

State before:
α qs : Type
M : TotalDFA α qs
head✝ : { x // x ∈ M.Z }
tail✝ : List { x // x ∈ M.Z }
ih : ∀ {q : { x // x ∈ M.Q }}, DFA.del_star_curried M.toDFA tail✝ q = some (del_star' M (q, tail✝))
q : { x // x ∈ M.Q }
⊢ M.δ (q, head✝) >>= DFA.del_star_curried M.toDFA tail✝ = some (del_star' M (q, head✝ :: tail✝))
Tactic:
rw [total_del_eq]
State after:
α qs : Type
M : TotalDFA α qs
head✝ : { x // x ∈ M.Z }
tail✝ : List { x // x ∈ M.Z }
ih : ∀ {q : { x // x ∈ M.Q }}, DFA.del_star_curried M.toDFA tail✝ q = some (del_star' M (q, tail✝))
q : { x // x ∈ M.Q }
⊢ some (δ' M (q, head✝)) >>= DFA.del_star_curried M.toDFA tail✝ = some (del_star' M (q, head✝ :: tail✝))

State before:
α qs : Type
M : TotalDFA α qs
head✝ : { x // x ∈ M.Z }
tail✝ : List { x // x ∈ M.Z }
ih : ∀ {q : { x // x ∈ M.Q }}, DFA.del_star_curried M.toDFA tail✝ q = some (del_star' M (q, tail✝))
q : { x // x ∈ M.Q }
⊢ some (δ' M (q, head✝)) >>= DFA.del_star_curried M.toDFA tail✝ = some (del_star' M (q, head✝ :: tail✝))
Tactic:
apply ih
State after:
no goals