rw [Finset.mem_map]
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w'), qf ∈ M.F) ↔
    TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some M.q₀, property := ⋯ }, w') ∈
      Finset.map { toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } M.F
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w'), qf ∈ M.F) ↔
    ∃ a ∈ M.F,
      { toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } a =
        TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some M.q₀, property := ⋯ }, w')