rw [this]
case cons
α qs : Type
M : DFA α qs
x : { x // x ∈ (DFA.toTotalDFA M).Z }
xs : List { x // x ∈ (DFA.toTotalDFA M).Z }
ih : ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, xs)) = none
this : TotalDFA.δ' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, x) = { val := none, property := ⋯ }
⊢ ↑(TotalDFA.del_star' (DFA.toTotalDFA M) (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, x), xs)) =
    none
case cons
α qs : Type
M : DFA α qs
x : { x // x ∈ (DFA.toTotalDFA M).Z }
xs : List { x // x ∈ (DFA.toTotalDFA M).Z }
ih : ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, xs)) = none
this : TotalDFA.δ' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, x) = { val := none, property := ⋯ }
⊢ ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := none, property := ⋯ }, xs)) = none