Choice is indispensable for much of modern classical mathematics. Therefore, most proof assistants offer it as part of their standard library. The most powerful version is sometimes called global choice or Hilbert's choice operator. This I believe is the version used by Lean, HOL-Light, and Is...