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

State before:
α qs : Type
M : DFA α qs
q : { x // x ∈ M.Q }
a : { x // x ∈ M.Z }
⊢ M.δ (q, a) = ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, a))
Tactic:
simp [TotalDFA.δ']
State after:
α qs : Type
M : DFA α qs
q : { x // x ∈ M.Q }
a : { x // x ∈ M.Z }
⊢ M.δ (q, a) = ↑(Option.get ((DFA.toTotalDFA M).δ ({ val := some q, property := ⋯ }, a)) ⋯)

State before:
α qs : Type
M : DFA α qs
q : { x // x ∈ M.Q }
a : { x // x ∈ M.Z }
⊢ M.δ (q, a) = ↑(Option.get ((DFA.toTotalDFA M).δ ({ val := some q, property := ⋯ }, a)) ⋯)
Tactic:
cases hd: M.δ _ <;> simp [DFA.toTotalDFA, hd]
State after:
no goals