chore(data/setoid/partition): use set.finite (#17228)

Author: urkud

src/combinatorics/simple_graph/coloring.lean

@@ -100,7 +100,7 @@ lemma coloring.mem_color_classes {v : V} : C.color_class (C v) ∈ C.color_class
 ⟨v, rfl⟩
 
 lemma coloring.color_classes_finite [finite α] : C.color_classes.finite :=
-set.finite_coe_iff.1 $ setoid.finite_classes_ker _
+setoid.finite_classes_ker _
 
 lemma coloring.card_color_classes_le [fintype α] [fintype C.color_classes] :
   fintype.card C.color_classes ≤ fintype.card α :=

src/data/setoid/partition.lean

@@ -67,8 +67,9 @@ lemma classes_ker_subset_fiber_set {β : Type*} (f : α → β) :
   (setoid.ker f).classes ⊆ set.range (λ y, {x | f x = y}) :=
 by { rintro s ⟨x, rfl⟩, rw set.mem_range, exact ⟨f x, rfl⟩ }
 
-lemma finite_classes_ker {α β : Type*} [finite β] (f : α → β) : finite (setoid.ker f).classes :=
-by { classical, exact finite.set.subset _ (classes_ker_subset_fiber_set f) }
+lemma finite_classes_ker {α β : Type*} [finite β] (f : α → β) :
+  (setoid.ker f).classes.finite :=
+(set.finite_range _).subset $ classes_ker_subset_fiber_set f
 
 lemma card_classes_ker_le {α β : Type*} [fintype β]
   (f : α → β) [fintype (setoid.ker f).classes] :