chore(DomMulAct): remove decidability assumptions (#17510)

Found by the linter in #10235.

Author: grunweg

Mathlib/GroupTheory/Perm/DomMulAct.lean

@@ -88,14 +88,14 @@ lemma stabilizerMulEquiv_apply (g : (stabilizer (Perm α)ᵈᵐᵃ f)ᵐᵒᵖ)
 
 section Fintype
 
-variable [Fintype α] [DecidableEq α] [DecidableEq ι]
+variable [Fintype α]
 
 open Nat
 
 variable (f)
 
 /-- The cardinality of the type of permutations preserving a function -/
-theorem stabilizer_card [Fintype ι] :
+theorem stabilizer_card [DecidableEq α] [DecidableEq ι] [Fintype ι] :
     Fintype.card {g : Perm α // f ∘ g = f} = ∏ i, (Fintype.card {a // f a = i})! := by
   -- rewriting via Nat.card because Fintype instance is not found
   rw [← Nat.card_eq_fintype_card,
@@ -108,9 +108,12 @@ theorem stabilizer_card [Fintype ι] :
 /-- The cardinality of the set of permutations preserving a function -/
 theorem stabilizer_ncard [Fintype ι] :
     Set.ncard {g : Perm α | f ∘ g = f} = ∏ i, (Set.ncard {a | f a = i})! := by
+  classical
   simp only [← Set.Nat.card_coe_set_eq, Set.coe_setOf, card_eq_fintype_card]
   exact stabilizer_card f
 
+variable [DecidableEq α] [DecidableEq ι]
+
 /-- The cardinality of the type of permutations preserving a function
   (without the finiteness assumption on target)-/
 theorem stabilizer_card':