feat: add Classical.ofNonempty

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
 

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)