rw [Subtype.eq hd]
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q'✝ : { x // x ∈ M.Q }
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := some q'✝, property := ⋯ }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = ↑q'
this : ↑q' = some q'✝
⊢ DFA.del_star_curried M xs q'✝ =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
case some
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q q'✝ : { x // x ∈ M.Q }
q' : { x // x ∈ (DFA.toTotalDFA M).Q } := { val := some q'✝, property := ⋯ }
hd : ↑(TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝)) = ↑q'
this : ↑q' = some q'✝
⊢ DFA.del_star_curried M xs q'✝ = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) (q', xs))