feat(group_theory/*): Add finite instances (#17377)

To facilitate the transition from `fintype` to `finite` in the group theory library, here are some `finite` instances that mirror existing `fintype` instances.

src/algebra/group/conj.lean

@@ -7,7 +7,7 @@ import algebra.group.semiconj
 import algebra.group_with_zero.basic
 import algebra.hom.aut
 import algebra.hom.group
-import data.fintype.basic
+import data.finite.basic
 
 /-!
 # Conjugacy of group elements
@@ -177,6 +177,9 @@ instance [fintype α] [decidable_rel (is_conj : α → α → Prop)] :
   fintype (conj_classes α) :=
 quotient.fintype (is_conj.setoid α)
 
+instance [finite α] : finite (conj_classes α) :=
+quotient.finite _
+
 /--
 Certain instances trigger further searches when they are considered as candidate instances;
 these instances should be assigned a priority lower than the default of 1000 (for example, 900).
@@ -191,7 +194,7 @@ If those conditions hold, the instance `instT` should be assigned lower priority
 For example, suppose the search for an instance of `decidable_eq (multiset α)` tries the
 candidate instance `con.quotient.decidable_eq (c : con M) : decidable_eq c.quotient`.
 Since `multiset` and `con.quotient` are both quotient types, unification will check
-that the relations `list.perm` and `c.to_setoid.r` unify. However, `c.to_setoid` depends on 
+that the relations `list.perm` and `c.to_setoid.r` unify. However, `c.to_setoid` depends on
 a `has_mul M` instance, so this unification triggers a search for `has_mul (list α)`;
 this will traverse all subclasses of `has_mul` before failing.
 On the other hand, the search for an instance of `decidable_eq (con.quotient c)` for `c : con M`

src/group_theory/abelianization.lean

@@ -91,6 +91,9 @@ instance [fintype G] [decidable_pred (∈ commutator G)] :
   fintype (abelianization G) :=
 quotient_group.fintype (commutator G)
 
+instance [finite G] : finite (abelianization G) :=
+quotient.finite _
+
 variable {G}
 
 /-- `of` is the canonical projection from G to its abelianization. -/

src/group_theory/subgroup/basic.lean

@@ -338,6 +338,10 @@ lemma mem_to_submonoid (K : subgroup G) (x : G) : x ∈ K.to_submonoid ↔ x ∈
 instance (K : subgroup G) [d : decidable_pred (∈ K)] [fintype G] : fintype K :=
 show fintype {g : G // g ∈ K}, from infer_instance
 
+@[to_additive]
+instance (K : subgroup G) [finite G] : finite K :=
+subtype.finite
+
 @[to_additive]
 theorem to_submonoid_injective :
   function.injective (to_submonoid : subgroup G → submonoid G) :=