From b163aa02c078917352368e6f049cc1dc1c00880d Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@himmel-villmar.de>
Date: Wed, 20 Mar 2024 22:11:17 +0000
Subject: [PATCH] feat: remove superseded `small_of_fintype` (#11326)

---
 Mathlib.lean                      |  1 -
 Mathlib/Data/Countable/Small.lean | 12 ++++++++++--
 Mathlib/Data/Fintype/Small.lean   | 24 ------------------------
 Mathlib/Logic/Small/Basic.lean    |  3 +--
 4 files changed, 11 insertions(+), 29 deletions(-)
 delete mode 100644 Mathlib/Data/Fintype/Small.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 14ce97efaca0b..ee3e1ffd55890 100644
--- a/Mathlib.lean
+++ b/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
diff --git a/Mathlib/Data/Countable/Small.lean b/Mathlib/Data/Countable/Small.lean
index 6e1f4e13989fa..b5a37d55ddf4f 100644
--- a/Mathlib/Data/Countable/Small.lean
+++ b/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
diff --git a/Mathlib/Data/Fintype/Small.lean b/Mathlib/Data/Fintype/Small.lean
deleted file mode 100644
index 9b40e0b4b9511..0000000000000
--- a/Mathlib/Data/Fintype/Small.lean
+++ /dev/null
@@ -1,24 +0,0 @@
-/-
-Copyright (c) 2021 Scott Morrison. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
--/
-import Mathlib.Data.Fintype.Card
-import Mathlib.Logic.Small.Defs
-
-#align_import data.fintype.small from "leanprover-community/mathlib"@"1126441d6bccf98c81214a0780c73d499f6721fe"
-
-/-!
-# All finite types are small.
-
-That is, any `α` with `[Fintype α]` is equivalent to a type in any universe.
-
--/
-
-
-universe w v
-
-instance (priority := 100) small_of_fintype (α : Type v) [Fintype α] : Small.{w} α := by
-  rw [small_congr (Fintype.equivFin α)]
-  infer_instance
-#align small_of_fintype small_of_fintype
diff --git a/Mathlib/Logic/Small/Basic.lean b/Mathlib/Logic/Small/Basic.lean
index 4eebab982714a..8288d1c9fe1f0 100644
--- a/Mathlib/Logic/Small/Basic.lean
+++ b/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)] :