fix: Finpartition.atomise should not have [Fintype α] (#16617)

Noticed by @b-mehta.

Mathlib/Order/Partition/Finpartition.lean

@@ -548,6 +548,8 @@ lemma card_mod_card_parts_le : s.card % P.parts.card ≤ P.parts.card := by
     rw [h, h']
   · exact (Nat.mod_lt _ h).le
 
+section Setoid
+
 variable [Fintype α]
 
 /-- A setoid over a finite type induces a finpartition of the type's elements,
@@ -587,6 +589,8 @@ theorem mem_part_ofSetoid_iff_rel {s : Setoid α} [DecidableRel s.r] {b : α} :
   simp only [← hc, mem_univ, mem_filter, true_and] at this ⊢
   exact ⟨s.trans (s.symm this), s.trans this⟩
 
+end Setoid
+
 section Atomise
 
 /-- Cuts `s` along the finsets in `F`: Two elements of `s` will be in the same part if they are