feat(data/fintype/basic): provide a fintype instance for sym α n (#…

…8427)

This also provides `fintype (sym.sym' α n)` as an intermediate step.

Note we make `vector.perm.is_setoid` reducible as `quotient.fintype _` requires either this or `local attribute [instance] vector.perm.is_setoid` to be accepted by the elaborator.
The referenced library note suggests making it reducible is fine.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/data/fintype/basic.lean

@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 import data.array.lemmas
 import data.finset.pi
 import data.finset.powerset
+import data.sym
 import group_theory.perm.basic
 import order.well_founded
 import tactic.wlog
@@ -1124,6 +1125,12 @@ instance finset.fintype [fintype α] : fintype (finset α) :=
   [decidable_eq α] [decidable_eq β] : fintype (α ↪ β) :=
 fintype.of_equiv _ (equiv.subtype_injective_equiv_embedding α β)
 
+instance [decidable_eq α] [fintype α] {n : ℕ} : fintype (sym.sym' α n) :=
+quotient.fintype _
+
+instance [decidable_eq α] [fintype α] {n : ℕ} : fintype (sym α n) :=
+fintype.of_equiv _ sym.sym_equiv_sym'.symm
+
 @[simp] lemma fintype.card_finset [fintype α] :
   fintype.card (finset α) = 2 ^ (fintype.card α) :=
 finset.card_powerset finset.univ

src/data/sym.lean

@@ -39,7 +39,10 @@ def sym (α : Type u) (n : ℕ) := {s : multiset α // s.card = n}
 
 /--
 This is the `list.perm` setoid lifted to `vector`.
+
+See note [reducible non-instances].
 -/
+@[reducible]
 def vector.perm.is_setoid (α : Type u) (n : ℕ) : setoid (vector α n) :=
 { r := λ a b, list.perm a.1 b.1,
   iseqv := by { rcases list.perm.eqv α with ⟨hr, hs, ht⟩, tidy, } }