[Merged by Bors] - chore: remove superseded small_of_fintype

Mathlib.lean

@@ -1715,7 +1715,6 @@ import Mathlib.Data.Fintype.Powerset
 import Mathlib.Data.Fintype.Prod
 import Mathlib.Data.Fintype.Quotient
 import Mathlib.Data.Fintype.Sigma
-import Mathlib.Data.Fintype.Small
 import Mathlib.Data.Fintype.Sort
 import Mathlib.Data.Fintype.Sum
 import Mathlib.Data.Fintype.Units

Mathlib/Data/Countable/Small.lean

@@ -7,6 +7,7 @@ import Mathlib.Logic.Small.Basic
 import Mathlib.Data.Countable.Defs
 
 #align_import data.countable.small from "leanprover-community/mathlib"@"bbeb185db4ccee8ed07dc48449414ebfa39cb821"
+#align_import data.fintype.small from "leanprover-community/mathlib"@"1126441d6bccf98c81214a0780c73d499f6721fe"
 
 /-!
 # All countable types are small.
@@ -17,7 +18,14 @@ 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} α :=
+instance (priority := 100) Countable.toSmall (α : Type v) [Countable α] : Small.{w} α :=
   let ⟨_, hf⟩ := exists_injective_nat α
   small_of_injective hf
-#align small_of_countable small_of_countable
+#align small_of_countable Countable.toSmall
+#align small_of_fintype Countable.toSmall
+
+@[deprecated, nolint defLemma] -- 2024-03-20
+alias small_of_countable := Countable.toSmall
+
+@[deprecated, nolint defLemma] -- 2024-03-20
+alias small_of_fintype := Countable.toSmall

Mathlib/Logic/Small/Basic.lean

@@ -57,8 +57,7 @@ theorem small_of_injective_of_exists {α : Type v} {β : Type w} {γ : Type v'}
     infer_instance
 
 /-!
-We don't define `small_of_fintype` or `small_of_countable` in this file,
-to keep imports to `Logic` to a minimum.
+We don't define `Countable.toSmall` in this file, to keep imports to `Logic` to a minimum.
 -/
 
 instance small_Pi {α} (β : α → Type*) [Small.{w} α] [∀ a, Small.{w} (β a)] :