[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
⊢ Fintype (Sym.Sym' α n)
[PROOFSTEP]
refine
  @Quotient.fintype _ _ _
    ?_
      -- Porting note: had to build the instance manually
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
⊢ DecidableRel fun x x_1 => x ≈ x_1
[PROOFSTEP]
intros x y
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
x y : Vector α n
⊢ Decidable ((fun x x_1 => x ≈ x_1) x y)
[PROOFSTEP]
apply List.decidablePerm
