. intro ⟨qf, hdel, hf⟩
  let r := constrRun w M.q₀
  have : r.isSome :=
    del_star_isSome_iff_constrRun_isSome.mp
      (Option.isSome_iff_exists.mpr ⟨qf, hdel⟩)
  exists r.get this
  simp [last_state_eq_del_star (r.get this)] at hdel
  rw [hdel]; assumption
case mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ (∃ qf ∈ del_star M (M.q₀, w), qf ∈ M.F) → w ∈ AcceptedLanguage M
no goals