case cons _ xs ih =>
  simp [DFA.del_star_curried, Option.bind_eq_bind, TotalDFA.del_star']
  cases' hd: M.δ _ with q'
  . rw [totalDFA_del_eq_del] at hd
    let q' : M.toTotalDFA.Q := ⟨ none, Fintype.complete _ ⟩
    have : q'.val = none := rfl
    rw [<-this] at hd
    simp [Subtype.eq hd]
    rw [totalDFA_del_star_none]
  . rw [Option.some_bind]
    rw [totalDFA_del_eq_del] at hd
    let q' : M.toTotalDFA.Q := ⟨ some q', Fintype.complete _ ⟩
    have : q'.val = some _ := rfl
    rw [<-this] at hd
    rw [Subtype.eq hd]
    apply ih
α 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 : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M (head✝ :: xs) q =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝ :: xs))
no goals