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)