Mathlib.Data.FinEnum._auxLemma.1

theorem Mathlib.Data.FinEnum._auxLemma.1 : ∀ {α : Type u} [inst : FinEnum α] (x : α), (x ∈ FinEnum.toList α) = True

The theorem `Mathlib.Data.FinEnum._auxLemma.1` states that for any type `α` that has a `FinEnum` instance (i.e., `α` is a finite enumerable type), any value `x` of type `α` is guaranteed to be present in the exhaustive list of all possible values of type `α` generated by `FinEnum.toList α`. That is, `x` belongs to the list produced by the function `FinEnum.toList α` regardless of the specific `x` chosen. The theorem allows us to assert the completeness and correctness of the `FinEnum` enumeration for any finite enumerable type `α`.

More concisely: For any finite enumerable type `α`, every element `x` of `α` is present in the list produced by `FinEnum.toList α`.