cases hd: M.δ _ <;> simp [DFA.toTotalDFA, hd]
α 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)) ⋯)
no goals