diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean
index 71a4feb8d4..ca8c089516 100644
--- a/src/Init/Classical.lean
+++ b/src/Init/Classical.lean
@@ -13,8 +13,6 @@ universe u v
 
 namespace Classical
 
-axiom choice {α : Sort u} : Nonempty α → α
-
 noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop) (h : ∃ x, p x) : {x // p x} :=
   choice <| let ⟨x, px⟩ := h; ⟨⟨x, px⟩⟩
 
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 5c5cc17a6c..11fd8c366d 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -460,15 +460,6 @@ instance : Inhabited Prop where
 
 deriving instance Inhabited for NonScalar, PNonScalar, True, ForInStep
 
-class inductive Nonempty (α : Sort u) : Prop where
-  | intro (val : α) : Nonempty α
-
-protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p :=
-  h₂ h₁.1
-
-instance {α : Sort u} [Inhabited α] : Nonempty α :=
-  ⟨arbitrary⟩
-
 theorem nonempty_of_exists {α : Sort u} {p : α → Prop} : Exists (fun x => p x) → Nonempty α
   | ⟨w, h⟩ => ⟨w⟩
 
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index a5922a82aa..2d39afbec4 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -196,6 +196,17 @@ theorem ne_true_of_eq_false : {b : Bool} → Eq b false → Not (Eq b true)
 class Inhabited (α : Sort u) where
   mk {} :: (default : α)
 
+class inductive Nonempty (α : Sort u) : Prop where
+  | intro (val : α) : Nonempty α
+
+axiom Classical.choice {α : Sort u} : Nonempty α → α
+
+protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p :=
+  h₂ h₁.1
+
+instance {α : Sort u} [Inhabited α] : Nonempty α :=
+  ⟨Inhabited.default⟩
+
 constant arbitrary [Inhabited α] : α :=
   Inhabited.default