feat: port data.countable.small (#1128)

Port of Data.Countable.Small

based on bbeb185db4ccee8ed07dc48449414ebfa39cb821

Mathlib.lean

@@ -164,6 +164,7 @@ import Mathlib.Data.Bracket
 import Mathlib.Data.ByteArray
 import Mathlib.Data.Char
 import Mathlib.Data.Countable.Defs
+import Mathlib.Data.Countable.Small
 import Mathlib.Data.DList.Basic
 import Mathlib.Data.Equiv.Functor
 import Mathlib.Data.Erased

Mathlib/Data/Countable/Small.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2021 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+
+! This file was ported from Lean 3 source module data.countable.small
+! leanprover-community/mathlib commit bbeb185db4ccee8ed07dc48449414ebfa39cb821
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Logic.Small.Basic
+import Mathlib.Data.Countable.Defs
+
+/-!
+# All countable types are small.
+
+That is, any countable type is equivalent to a type in any universe.
+-/
+
+
+universe w v
+
+instance (priority := 100) small_of_countable (α : Type v) [Countable α] : Small.{w} α :=
+  let ⟨_, hf⟩ := exists_injective_nat α
+  small_of_injective hf
+#align small_of_countable small_of_countable