Computable FinEnum constructions for Bool, Sym, Equiv.Perm, and embeddings

FinEnum α packages a finite type with a canonical computable enumeration (an exhaustive duplicate-free list, hence DecidableEq and Fintype). Mathlib provides FinEnum for the basic shape-formers (Fin, products, sums, Finset, subtypes, pi types, …) but not for Bool nor for the combinatorial type-formers Sym, Equiv.Perm, and function embeddings — even though each has a Fintype instance and an underlying list enumerator. This file fills those gaps.

• FinEnum Bool is a small base instance.
• Sym.finEnum, Equiv.Perm.finEnum, and Function.Embedding.finEnum are provided as plain defs (not instances) on purpose: a global FinEnum instance for any of these would, through the priority 100 FinEnum → Fintype instance, synthesize a second Fintype competing with Mathlib's native one and not definitionally equal to it. Callers that want the enumeration introduce it locally with letI so no competing Fintype ever enters global resolution.

Each construction reuses an existing computable enumerator: List.sym for Sym, permsOfList for Equiv.Perm, and the equivalence with the injective-function subtype for embeddings (the latter is genuinely computable, unlike Mathlib's noncomputable Function.Embedding.fintype). List.mem_sym supplies the completeness half that Mathlib is missing for List.sym.

theorem List.mem_sym {α : Type u} {n : ℕ} {xs : List α} {z : Sym α n} : (∀ a ∈ z, a ∈ xs) → z ∈ List.sym n xs

Completeness of List.sym: every z : Sym α n whose members all lie in xs is enumerated by xs.sym n. This is the converse of List.mem_of_mem_of_mem_sym.

@[implicit_reducible]

instance instFinEnumBool_toMathlib : FinEnum Bool

Bool enumerated as [true, false].

@[reducible]

def Sym.finEnum {α : Type u} [FinEnum α] (n : ℕ) : FinEnum (Sym α n)

Computable enumeration of size-n multisets over a FinEnum type, drawn from List.sym of the canonical enumeration. Every z : Sym α n qualifies since all its members lie in FinEnum.toList.

@[reducible]

def Equiv.Perm.finEnum {α : Type u} [FinEnum α] : FinEnum (Perm α)

Computable enumeration of permutations of a FinEnum type via permsOfList applied to the canonical enumeration. Completeness holds because every element a permutation can move lies in FinEnum.toList.

@[reducible]

def Function.Embedding.finEnum {β α : Type u} [FinEnum β] [FinEnum α] : FinEnum (β ↪ α)

Computable enumeration of embeddings β ↪ α between FinEnum types, transported from the FinEnum on the subtype of injective functions {f : β → α // Function.Injective f}. Injectivity is decidable for functions out of a finite domain, so this subtype is itself FinEnum.