. 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
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 }
hd : M.δ (q, head✝) = some q'
⊢ Option.bind (some q') (DFA.del_star_curried M xs) =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))
no goals