From f1adedb2debe16ce8b3370a666d50456bf010c75 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 14 Jan 2022 13:44:59 -0800
Subject: [PATCH] feat: add `Classical.ofNonempty`

---
 src/Init/Prelude.lean         | 3 +++
 src/Lean/Meta/AppBuilder.lean | 4 ++++
 2 files changed, 7 insertions(+)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 2d39afbec4..d8af52ec8c 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -207,6 +207,9 @@ protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂
 instance {α : Sort u} [Inhabited α] : Nonempty α :=
   ⟨Inhabited.default⟩
 
+noncomputable def Classical.ofNonempty {α : Sort u} [Nonempty α] : α :=
+  Classical.choice inferInstance
+
 constant arbitrary [Inhabited α] : α :=
   Inhabited.default
 
diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index 09f1bc978a..b66d9df051 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -437,6 +437,10 @@ def mkLe (a b : Expr) : MetaM Expr :=
 def mkArbitrary (α : Expr) : MetaM Expr :=
   mkAppOptM ``arbitrary #[α, none]
 
+/-- Return `@Classical.ofNonempty α _` -/
+def mkOfNonempty (α : Expr) : MetaM Expr := do
+  mkAppOptM ``Classical.ofNonempty #[α, none]
+
 /-- Return `sorryAx type` -/
 def mkSyntheticSorry (type : Expr) : MetaM Expr :=
   return mkApp2 (mkConst ``sorryAx [← getLevel type]) type (mkConst ``Bool.true)