doc-next-gen

Mathlib.Data.Fintype.Basic

Module docstring

{"# Instances for finite types

This file is a collection of basic Fintype instances for types such as Fin, Prod and pi types. "}

Fin.univ_def theorem
(n : ℕ) : (univ : Finset (Fin n)) = ⟨List.finRange n, List.nodup_finRange n⟩
Full source 
theorem Fin.univ_def (n : ℕ) : (univ : Finset (Fin n)) = ⟨List.finRange n, List.nodup_finRange n⟩ :=
  rfl
Universal Finite Set of Finite Ordinals as Range List with No Duplicates
Informal description
For any natural number $n$, the universal finite set of $\mathrm{Fin}(n)$ is equal to the pair consisting of the list $[0, 1, \dots, n-1]$ and a proof that this list has no duplicates.
Finset.val_univ_fin theorem
(n : ℕ) : (Finset.univ : Finset (Fin n)).val = List.finRange n
Full source 
theorem Finset.val_univ_fin (n : ℕ) : (Finset.univ : Finset (Fin n)).val = List.finRange n := rfl
Universal Finite Set of Finite Ordinals as Range List
Informal description
For any natural number $n$, the underlying list of the universal finite set of $\mathrm{Fin}(n)$ is equal to the list $[0, 1, \dots, n-1]$.
nonempty_fintype theorem
(α : Type*) [Finite α] : Nonempty (Fintype α)
Full source 
/-- See also `nonempty_encodable`, `nonempty_denumerable`. -/
theorem nonempty_fintype (α : Type*) [Finite α] : Nonempty (Fintype α) := by
  rcases Finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩
  exact ⟨.ofEquiv _ e.symm⟩
Existence of Finite Type Structure for Finite Types
Informal description
For any finite type $\alpha$, there exists a finite type structure (a `Fintype` instance) on $\alpha$.
List.toFinset_finRange theorem
(n : ℕ) : (List.finRange n).toFinset = Finset.univ
Full source 
@[simp] theorem List.toFinset_finRange (n : ℕ) : (List.finRange n).toFinset = Finset.univ := by
  ext; simp
Finite Range List to Universal Finite Set Equality
Informal description
For any natural number $n$, the finite set constructed from the list $[0, 1, \dots, n-1]$ is equal to the universal finite set of $\mathrm{Fin}(n)$.
Fin.univ_val_map theorem
{n : ℕ} (f : Fin n → α) : Finset.univ.val.map f = List.ofFn f
Full source 
@[simp] theorem Fin.univ_val_map {n : ℕ} (f : Fin n → α) :
    Finset.univ.val.map f = List.ofFn f := by
  simp [List.ofFn_eq_map, univ_def]
Universal Finite Set Map Equals List of Function Values on $\mathrm{Fin}(n)$
Informal description
For any natural number $n$ and any function $f \colon \mathrm{Fin}(n) \to \alpha$, the underlying multiset of the universal finite set of $\mathrm{Fin}(n)$ mapped by $f$ is equal to the list obtained by applying $f$ to all elements of $\mathrm{Fin}(n)$.
Fin.univ_image_def theorem
{n : ℕ} [DecidableEq α] (f : Fin n → α) : Finset.univ.image f = (List.ofFn f).toFinset
Full source 
theorem Fin.univ_image_def {n : ℕ} [DecidableEq α] (f : Fin n → α) :
    Finset.univ.image f = (List.ofFn f).toFinset := by
  simp [Finset.image]
Image of Universal Finite Set Equals List-to-Finset of Function Values on $\mathrm{Fin}(n)$
Informal description
For any natural number $n$ and any function $f \colon \mathrm{Fin}(n) \to \alpha$ (where $\alpha$ has decidable equality), the image of the universal finite set of $\mathrm{Fin}(n)$ under $f$ is equal to the finite set obtained from the list of function values $(f(0), f(1), \dots, f(n-1))$.
Fin.univ_map_def theorem
{n : ℕ} (f : Fin n ↪ α) : Finset.univ.map f = ⟨List.ofFn f, List.nodup_ofFn.mpr f.injective⟩
Full source 
theorem Fin.univ_map_def {n : ℕ} (f : FinFin n ↪ α) :
    Finset.univ.map f = ⟨List.ofFn f, List.nodup_ofFn.mpr f.injective⟩ := by
  simp [Finset.map]
Mapping of Universal Finite Set via Injective Embedding Equals List-Based Finite Set
Informal description
For any natural number $n$ and any injective function embedding $f \colon \mathrm{Fin}(n) \hookrightarrow \alpha$, the finite set obtained by mapping the universal finite set of $\mathrm{Fin}(n)$ under $f$ is equal to the finite set constructed from the list $(f(0), f(1), \dots, f(n-1))$, which has no duplicates due to the injectivity of $f$.
Fin.image_succAbove_univ theorem
{n : ℕ} (i : Fin (n + 1)) : univ.image i.succAbove = { i }ᶜ
Full source 
@[simp]
theorem Fin.image_succAbove_univ {n : ℕ} (i : Fin (n + 1)) : univ.image i.succAbove = {i}{i}ᶜ := by
  ext m
  simp
Image of Universal Set under `succAbove` Embedding is Complement of Singleton
Informal description
For any natural number $n$ and any element $i \in \mathrm{Fin}(n+1)$, the image of the universal finite set under the embedding $\mathrm{succAbove}_i$ is equal to the complement of the singleton set $\{i\}$ in $\mathrm{Fin}(n+1)$. In other words, $\mathrm{image}(\mathrm{succAbove}_i, \mathrm{univ}) = \mathrm{Fin}(n+1) \setminus \{i\}$.
Fin.image_succ_univ theorem
(n : ℕ) : (univ : Finset (Fin n)).image Fin.succ = {0}ᶜ
Full source 
@[simp]
theorem Fin.image_succ_univ (n : ℕ) : (univ : Finset (Fin n)).image Fin.succ = {0}{0}ᶜ := by
  rw [← Fin.succAbove_zero, Fin.image_succAbove_univ]
Image of Universal Set under Successor Function is Complement of Zero in Finite Ordinals
Informal description
For any natural number $n$, the image of the universal finite set $\mathrm{univ} : \mathrm{Finset}(\mathrm{Fin}(n))$ under the successor function $\mathrm{succ}$ is equal to the complement of the singleton set $\{0\}$ in $\mathrm{Fin}(n)$. In other words, $\mathrm{image}(\mathrm{succ}, \mathrm{univ}) = \mathrm{Fin}(n) \setminus \{0\}$.
Fin.image_castSucc theorem
(n : ℕ) : (univ : Finset (Fin n)).image Fin.castSucc = {Fin.last n}ᶜ
Full source 
@[simp]
theorem Fin.image_castSucc (n : ℕ) :
    (univ : Finset (Fin n)).image Fin.castSucc = {Fin.last n}{Fin.last n}ᶜ := by
  rw [← Fin.succAbove_last, Fin.image_succAbove_univ]
Image of Universal Set under `castSucc` is Complement of Last Element
Informal description
For any natural number $n$, the image of the universal finite set $\mathrm{univ} : \mathrm{Finset}(\mathrm{Fin}(n))$ under the embedding $\mathrm{castSucc}$ is equal to the complement of the singleton set containing the last element $\mathrm{last}\,n$ in $\mathrm{Fin}(n)$. In other words, $\mathrm{image}(\mathrm{castSucc}, \mathrm{univ}) = \mathrm{Fin}(n) \setminus \{\mathrm{last}\,n\}$.
Fin.univ_succ theorem
(n : ℕ) : (univ : Finset (Fin (n + 1))) = Finset.cons 0 (univ.map ⟨Fin.succ, Fin.succ_injective _⟩) (by simp [map_eq_image])
Full source 
/-- Embed `Fin n` into `Fin (n + 1)` by prepending zero to the `univ` -/
theorem Fin.univ_succ (n : ℕ) :
    (univ : Finset (Fin (n + 1))) =
      Finset.cons 0 (univ.map ⟨Fin.succ, Fin.succ_injective _⟩) (by simp [map_eq_image]) := by
  simp [map_eq_image]
Universal Set Decomposition for $\mathrm{Fin}(n+1)$ via Successor Function
Informal description
For any natural number $n$, the universal finite set of $\mathrm{Fin}(n+1)$ (the type of finite ordinals less than $n+1$) can be constructed by prepending $0$ to the image of the universal finite set of $\mathrm{Fin}(n)$ under the injective successor function $\mathrm{succ} : \mathrm{Fin}(n) \to \mathrm{Fin}(n+1)$. In other words, $\mathrm{univ} = \{0\} \cup \mathrm{succ}(\mathrm{univ})$, where $\mathrm{univ}$ on the left is for $\mathrm{Fin}(n+1)$ and on the right is for $\mathrm{Fin}(n)$.
Fin.univ_castSuccEmb theorem
(n : ℕ) : (univ : Finset (Fin (n + 1))) = Finset.cons (Fin.last n) (univ.map Fin.castSuccEmb) (by simp [map_eq_image])
Full source 
/-- Embed `Fin n` into `Fin (n + 1)` by appending a new `Fin.last n` to the `univ` -/
theorem Fin.univ_castSuccEmb (n : ℕ) :
    (univ : Finset (Fin (n + 1))) =
      Finset.cons (Fin.last n) (univ.map Fin.castSuccEmb) (by simp [map_eq_image]) := by
  simp [map_eq_image]
Universal Set Decomposition for $\mathrm{Fin}(n+1)$ via $\mathrm{castSuccEmb}$
Informal description
For any natural number $n$, the universal finite set of $\mathrm{Fin}(n+1)$ is equal to the set obtained by cons-ing the last element $\mathrm{last}\,n$ to the image of the universal finite set of $\mathrm{Fin}(n)$ under the embedding $\mathrm{castSuccEmb}$. In other words, the universal set of $\mathrm{Fin}(n+1)$ consists of the last element and all elements obtained by embedding the elements of $\mathrm{Fin}(n)$ via $\mathrm{castSuccEmb}$.
Fin.univ_succAbove theorem
(n : ℕ) (p : Fin (n + 1)) : (univ : Finset (Fin (n + 1))) = Finset.cons p (univ.map <| Fin.succAboveEmb p) (by simp)
Full source 
/-- Embed `Fin n` into `Fin (n + 1)` by inserting
around a specified pivot `p : Fin (n + 1)` into the `univ` -/
theorem Fin.univ_succAbove (n : ℕ) (p : Fin (n + 1)) :
    (univ : Finset (Fin (n + 1))) = Finset.cons p (univ.map <| Fin.succAboveEmb p) (by simp) := by
  simp [map_eq_image]
Decomposition of Universal Set in $\mathrm{Fin}(n+1)$ via $\mathrm{succAboveEmb}$ Embedding
Informal description
For any natural number $n$ and any element $p \in \mathrm{Fin}(n+1)$, the universal finite set of $\mathrm{Fin}(n+1)$ is equal to the set obtained by inserting $p$ into the image of the universal finite set of $\mathrm{Fin}(n)$ under the embedding $\mathrm{succAboveEmb}(p)$. That is, $$\mathrm{univ} = \{p\} \cup \mathrm{succAboveEmb}(p)(\mathrm{univ})$$ where $\mathrm{univ}$ denotes the universal finite set of $\mathrm{Fin}(n+1)$.
Fin.univ_image_get theorem
[DecidableEq α] (l : List α) : Finset.univ.image l.get = l.toFinset
Full source 
@[simp] theorem Fin.univ_image_get [DecidableEq α] (l : List α) :
    Finset.univ.image l.get = l.toFinset := by
  simp [univ_image_def]
Image of Universal Set under List Indexing Equals List's Finite Set
Informal description
For any list $l$ of elements of type $\alpha$ with decidable equality, the image of the universal finite set of $\mathrm{Fin}(l.\mathrm{length})$ under the function that retrieves elements of $l$ by their indices is equal to the finite set obtained from $l$ itself. In other words, $\mathrm{image}(\mathrm{get}(l), \mathrm{univ}) = l.\mathrm{toFinset}$.
Fin.univ_image_getElem' theorem
[DecidableEq β] (l : List α) (f : α → β) : Finset.univ.image (fun i : Fin l.length => f <| l[(i : Nat)]) = (l.map f).toFinset
Full source 
@[simp] theorem Fin.univ_image_getElem' [DecidableEq β] (l : List α) (f : α → β) :
    Finset.univ.image (fun i : Fin l.length => f <| l[(i : Nat)]) = (l.map f).toFinset := by
  simp only [univ_image_def, List.ofFn_getElem_eq_map]
Image of Universal Finite Set via List Indexing Equals Mapped List's Finite Set
Informal description
For any list $l$ of elements of type $\alpha$ and any function $f \colon \alpha \to \beta$ (where $\beta$ has decidable equality), the image of the universal finite set of $\mathrm{Fin}(l.\mathrm{length})$ under the function $\lambda i \colon \mathrm{Fin}(l.\mathrm{length}), f(l[i])$ is equal to the finite set obtained from the list $l.\mathrm{map}\, f$.
Fin.univ_image_get' theorem
[DecidableEq β] (l : List α) (f : α → β) : Finset.univ.image (f <| l.get ·) = (l.map f).toFinset
Full source 
theorem Fin.univ_image_get' [DecidableEq β] (l : List α) (f : α → β) :
    Finset.univ.image (f <| l.get ·) = (l.map f).toFinset := by
  simp
Image of Universal Set under Composed List Indexing Equals Mapped List's Finite Set
Informal description
For any list $l$ of elements of type $\alpha$ and any function $f \colon \alpha \to \beta$ (where $\beta$ has decidable equality), the image of the universal finite set of $\mathrm{Fin}(l.\mathrm{length})$ under the composition of $f$ with the list indexing function $l.\mathrm{get}$ is equal to the finite set obtained from the list $l.\mathrm{map}\, f$. In other words, the following equality holds: $$\mathrm{image}(f \circ l.\mathrm{get}, \mathrm{univ}) = (l.\mathrm{map}\, f).\mathrm{toFinset}$$
Unique.fintype definition
{α : Type*} [Unique α] : Fintype α
Full source 
@[instance]
def Unique.fintype {α : Type*} [Unique α] : Fintype α :=
  Fintype.ofSubsingleton default
Finite type structure on a unique type
Informal description
For any type $\alpha$ with a unique element, $\alpha$ is a finite type. Specifically, the finite type structure is constructed using the unique element as a subsingleton.
Fintype.subtypeEq instance
(y : α) : Fintype { x // x = y }
Full source 
/-- Short-circuit instance to decrease search for `Unique.fintype`,
since that relies on a subsingleton elimination for `Unique`. -/
instance Fintype.subtypeEq (y : α) : Fintype { x // x = y } :=
  Fintype.subtype {y} (by simp)
Finite Subtype of Elements Equal to a Given Element
Informal description
For any element $y$ of type $\alpha$, the subtype $\{x \mid x = y\}$ is a finite type.
Fintype.subtypeEq' instance
(y : α) : Fintype { x // y = x }
Full source 
/-- Short-circuit instance to decrease search for `Unique.fintype`,
since that relies on a subsingleton elimination for `Unique`. -/
instance Fintype.subtypeEq' (y : α) : Fintype { x // y = x } :=
  Fintype.subtype {y} (by simp [eq_comm])
Finite Subtype of Elements Equal to a Given Element (Symmetric Version)
Informal description
For any element $y$ of type $\alpha$, the subtype $\{x \mid y = x\}$ is a finite type.
Fintype.univ_empty theorem
: @univ Empty _ = ∅
Full source 
theorem Fintype.univ_empty : @univ Empty _ = ∅ :=
  rfl
Universal Finite Set of Empty Type is Empty
Informal description
The universal finite set of the empty type is equal to the empty set, i.e., $\text{univ} = \emptyset$.
Fintype.univ_pempty theorem
: @univ PEmpty _ = ∅
Full source 
theorem Fintype.univ_pempty : @univ PEmpty _ = ∅ :=
  rfl
Universal Finite Set of Empty Type is Empty
Informal description
The universal finite set of the empty type `PEmpty` is equal to the empty set, i.e., $\text{univ} = \emptyset$.
Fintype.univ_unit theorem
: @univ Unit _ = {()}
Full source 
theorem Fintype.univ_unit : @univ Unit _ = {()} :=
  rfl
Universal Finite Set of Unit Type is Singleton
Informal description
The universal finite set of the unit type `Unit` is the singleton set containing the unique element `()`.
Fintype.univ_punit theorem
: @univ PUnit _ = { PUnit.unit }
Full source 
theorem Fintype.univ_punit : @univ PUnit _ = {PUnit.unit} :=
  rfl
Universal Finite Set of Pointed Unit Type is Singleton
Informal description
The universal finite set of the pointed unit type `PUnit` is the singleton set containing the unique element `PUnit.unit`.
Fintype.univ_bool theorem
: @univ Bool _ = { true, false }
Full source 
@[simp]
theorem Fintype.univ_bool : @univ Bool _ = {true, false} :=
  rfl
Universal Finite Set of Boolean Type is $\{\text{true}, \text{false}\}$
Informal description
The universal finite set of the Boolean type is $\{\text{true}, \text{false}\}$.
Fintype.prodLeft definition
{α β} [DecidableEq α] [Fintype (α × β)] [Nonempty β] : Fintype α
Full source 
/-- Given that `α × β` is a fintype, `α` is also a fintype. -/
def Fintype.prodLeft {α β} [DecidableEq α] [Fintype (α × β)] [Nonempty β] : Fintype α :=
  ⟨(@univ (α × β) _).image Prod.fst, fun a => by simp⟩
Finiteness of the first component in a finite product type
Informal description
Given types $\alpha$ and $\beta$ with $\beta$ nonempty and $\alpha \times \beta$ finite, the type $\alpha$ is also finite. Specifically, the finite set of elements of $\alpha$ is obtained by projecting the first components of the elements in the universal finite set of $\alpha \times \beta$.
Fintype.prodRight definition
{α β} [DecidableEq β] [Fintype (α × β)] [Nonempty α] : Fintype β
Full source 
/-- Given that `α × β` is a fintype, `β` is also a fintype. -/
def Fintype.prodRight {α β} [DecidableEq β] [Fintype (α × β)] [Nonempty α] : Fintype β :=
  ⟨(@univ (α × β) _).image Prod.snd, fun b => by simp⟩
Finiteness of the second component in a finite product type
Informal description
Given types $\alpha$ and $\beta$ with $\alpha$ nonempty and $\alpha \times \beta$ finite, the type $\beta$ is also finite. Specifically, the finite set of elements of $\beta$ is obtained by projecting the second components of the elements in the universal finite set of $\alpha \times \beta$.
ULift.fintype instance
(α : Type*) [Fintype α] : Fintype (ULift α)
Full source 
instance ULift.fintype (α : Type*) [Fintype α] : Fintype (ULift α) :=
  Fintype.ofEquiv _ Equiv.ulift.symm
Finiteness of Lifted Types
Informal description
For any finite type $\alpha$, the lifted type $\text{ULift}\,\alpha$ is also finite.
PLift.fintype instance
(α : Type*) [Fintype α] : Fintype (PLift α)
Full source 
instance PLift.fintype (α : Type*) [Fintype α] : Fintype (PLift α) :=
  Fintype.ofEquiv _ Equiv.plift.symm
Finiteness of PLifted Types
Informal description
For any finite type $\alpha$, the lifted type $\mathrm{PLift}\,\alpha$ is also finite.
Quotient.fintype instance
[Fintype α] (s : Setoid α) [DecidableRel ((· ≈ ·) : α → α → Prop)] : Fintype (Quotient s)
Full source 
instance Quotient.fintype [Fintype α] (s : Setoid α) [DecidableRel ((· ≈ ·) : α → α → Prop)] :
    Fintype (Quotient s) :=
  Fintype.ofSurjective Quotient.mk'' Quotient.mk''_surjective
Finiteness of Quotient Types
Informal description
For any finite type $\alpha$ with a setoid $s$ and a decidable equivalence relation $\approx$ on $\alpha$, the quotient type $\text{Quotient } s$ is also finite.
PSigma.fintypePropLeft instance
{α : Prop} {β : α → Type*} [Decidable α] [∀ a, Fintype (β a)] : Fintype (Σ' a, β a)
Full source 
instance PSigma.fintypePropLeft {α : Prop} {β : α → Type*} [Decidable α] [∀ a, Fintype (β a)] :
    Fintype (Σ'a, β a) :=
  if h : α then Fintype.ofEquiv (β h) ⟨fun x => ⟨h, x⟩, PSigma.snd, fun _ => rfl, fun ⟨_, _⟩ => rfl⟩
  else ⟨∅, fun x => (h x.1).elim⟩
Finiteness of Dependent Sum over Decidable Proposition with Finite Fibers
Informal description
For any decidable proposition $\alpha$ and any family of types $\beta$ indexed by $\alpha$ where each $\beta(a)$ is finite, the dependent sum type $\Sigma' a, \beta(a)$ is finite.
PSigma.fintypePropRight instance
{α : Type*} {β : α → Prop} [∀ a, Decidable (β a)] [Fintype α] : Fintype (Σ' a, β a)
Full source 
instance PSigma.fintypePropRight {α : Type*} {β : α → Prop} [∀ a, Decidable (β a)] [Fintype α] :
    Fintype (Σ'a, β a) :=
  Fintype.ofEquiv { a // β a }
    ⟨fun ⟨x, y⟩ => ⟨x, y⟩, fun ⟨x, y⟩ => ⟨x, y⟩, fun ⟨_, _⟩ => rfl, fun ⟨_, _⟩ => rfl⟩
Finiteness of Dependent Sum over Finite Type with Decidable Propositions
Informal description
For any type $\alpha$ with a finite number of elements and any family of propositions $\beta$ indexed by $\alpha$, if each proposition $\beta(a)$ is decidable for $a \in \alpha$, then the dependent sum type $\Sigma' a, \beta(a)$ is finite.
PSigma.fintypePropProp instance
{α : Prop} {β : α → Prop} [Decidable α] [∀ a, Decidable (β a)] : Fintype (Σ' a, β a)
Full source 
instance PSigma.fintypePropProp {α : Prop} {β : α → Prop} [Decidable α] [∀ a, Decidable (β a)] :
    Fintype (Σ'a, β a) :=
  if h : ∃ a, β a then ⟨{⟨h.fst, h.snd⟩}, fun ⟨_, _⟩ => by simp⟩ else ⟨∅, fun ⟨x, y⟩ =>
    (h ⟨x, y⟩).elim⟩
Finiteness of Dependent Sum of Decidable Propositions
Informal description
For any proposition $\alpha$ and any family of propositions $\beta$ indexed by $\alpha$, if $\alpha$ is decidable and each $\beta(a)$ is decidable for $a \in \alpha$, then the dependent sum type $\Sigma' a, \beta(a)$ is finite.
pfunFintype instance
(p : Prop) [Decidable p] (α : p → Type*) [∀ hp, Fintype (α hp)] : Fintype (∀ hp : p, α hp)
Full source 
instance pfunFintype (p : Prop) [Decidable p] (α : p → Type*) [∀ hp, Fintype (α hp)] :
    Fintype (∀ hp : p, α hp) :=
  if hp : p then Fintype.ofEquiv (α hp) ⟨fun a _ => a, fun f => f hp, fun _ => rfl, fun _ => rfl⟩
  else ⟨singleton fun h => (hp h).elim, fun h => mem_singleton.2
    (funext fun x => by contradiction)⟩
Finiteness of Dependent Function Types on Decidable Propositions
Informal description
For any decidable proposition $p$ and any family of types $\alpha$ indexed by $p$, if each $\alpha(hp)$ is finite for $hp : p$, then the type of dependent functions $\forall hp : p, \alpha(hp)$ is finite.
truncOfMultisetExistsMem definition
{α} (s : Multiset α) : (∃ x, x ∈ s) → Trunc α
Full source 
/-- For `s : Multiset α`, we can lift the existential statement that `∃ x, x ∈ s` to a `Trunc α`.
-/
def truncOfMultisetExistsMem {α} (s : Multiset α) : (∃ x, x ∈ s) → Trunc α :=
  Quotient.recOnSubsingleton s fun l h =>
    match l, h with
    | [], _ => False.elim (by tauto)
    | a :: _, _ => Trunc.mk a
Truncation of an element in a nonempty multiset
Informal description
Given a multiset $s$ over a type $\alpha$ and a proof that there exists an element $x$ in $s$, the function constructs a term of type `Trunc α` representing the truncation of some element in $s$.
truncOfNonemptyFintype definition
(α) [Nonempty α] [Fintype α] : Trunc α
Full source 
/-- A `Nonempty` `Fintype` constructively contains an element.
-/
def truncOfNonemptyFintype (α) [Nonempty α] [Fintype α] : Trunc α :=
  truncOfMultisetExistsMem Finset.univ.val (by simp)
Truncation of an element in a nonempty finite type
Informal description
Given a nonempty finite type $\alpha$, the function constructs a term of type `Trunc α` representing the truncation of some element in $\alpha$. This is achieved by using the universal finite set of $\alpha$ and the fact that it is nonempty.
truncSigmaOfExists definition
{α} [Fintype α] {P : α → Prop} [DecidablePred P] (h : ∃ a, P a) : Trunc (Σ' a, P a)
Full source 
/-- By iterating over the elements of a fintype, we can lift an existential statement `∃ a, P a`
to `Trunc (Σ' a, P a)`, containing data.
-/
def truncSigmaOfExists {α} [Fintype α] {P : α → Prop} [DecidablePred P] (h : ∃ a, P a) :
    Trunc (Σ'a, P a) :=
  @truncOfNonemptyFintype (Σ'a, P a) ((Exists.elim h) fun a ha => ⟨⟨a, ha⟩⟩) _
Truncation of a dependent pair from an existential statement over a finite type
Informal description
Given a finite type $\alpha$ and a decidable predicate $P$ on $\alpha$, if there exists an element $a \in \alpha$ such that $P(a)$ holds, then the function constructs a term of type `Trunc (Σ' a, P a)`, representing the truncation of a dependent pair consisting of an element $a$ and a proof that $P(a)$ holds.
Multiset.count_univ theorem
[DecidableEq α] (a : α) : count a Finset.univ.val = 1
Full source 
@[simp]
theorem count_univ [DecidableEq α] (a : α) : count a Finset.univ.val = 1 :=
  count_eq_one_of_mem Finset.univ.nodup (Finset.mem_univ _)
Multiplicity of Elements in Universal Multiset is One
Informal description
For any element $a$ of a finite type $\alpha$ with decidable equality, the multiplicity of $a$ in the universal multiset (constructed from the universal finite set of $\alpha$) is equal to 1, i.e., $\text{count}(a, \text{univ.val}) = 1$.
Multiset.map_univ_val_equiv theorem
(e : α ≃ β) : map e univ.val = univ.val
Full source 
@[simp]
theorem map_univ_val_equiv (e : α ≃ β) :
    map e univ.val = univ.val := by
  rw [← congr_arg Finset.val (Finset.map_univ_equiv e), Finset.map_val, Equiv.coe_toEmbedding]
Bijection Preserves Universal Multiset for Finite Types
Informal description
For any equivalence (bijection) $e$ between finite types $\alpha$ and $\beta$, the image of the universal multiset of $\alpha$ under $e$ is equal to the universal multiset of $\beta$. In other words, if we apply the bijection $e$ to every element in the complete collection of elements of $\alpha$, we obtain the complete collection of elements of $\beta$.
Multiset.bijective_iff_map_univ_eq_univ theorem
(f : α → β) : f.Bijective ↔ map f (Finset.univ : Finset α).val = univ.val
Full source 
/-- For functions on finite sets, they are bijections iff they map universes into universes. -/
@[simp]
theorem bijective_iff_map_univ_eq_univ (f : α → β) :
    f.Bijective ↔ map f (Finset.univ : Finset α).val = univ.val :=
  ⟨fun bij ↦ congr_arg (·.val) (map_univ_equiv <| Equiv.ofBijective f bij),
    fun eq ↦ ⟨
      fun a₁ a₂ ↦ inj_on_of_nodup_map (eq.symm ▸ univ.nodup) _ (mem_univ a₁) _ (mem_univ a₂),
      fun b ↦ have ⟨a, _, h⟩ := mem_map.mp (eq.symm ▸ mem_univ_val b); ⟨a, h⟩⟩⟩
Bijectivity Criterion via Universal Multiset Mapping
Informal description
For a function $f : \alpha \to \beta$ between finite types $\alpha$ and $\beta$, $f$ is bijective if and only if the image of the universal multiset of $\alpha$ under $f$ is equal to the universal multiset of $\beta$. In other words, $f$ is bijective if and only if $f$ maps every element of $\alpha$ to every element of $\beta$ exactly once.
seqOfForallFinsetExistsAux definition
{α : Type*} [DecidableEq α] (P : α → Prop) (r : α → α → Prop) (h : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y) : ℕ → α
Full source 
/-- Auxiliary definition to show `exists_seq_of_forall_finset_exists`. -/
noncomputable def seqOfForallFinsetExistsAux {α : Type*} [DecidableEq α] (P : α → Prop)
    (r : α → α → Prop) (h : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y) : ℕ → α
  | n =>
    Classical.choose
      (h
        (Finset.image (fun i : Fin n => seqOfForallFinsetExistsAux P r h i)
          (Finset.univ : Finset (Fin n))))
Auxiliary sequence construction from finite subset existence
Informal description
Given a decidable type $\alpha$, a predicate $P$ on $\alpha$, and a binary relation $r$ on $\alpha$, if for every finite subset $s$ of $\alpha$ there exists an element $y$ such that whenever all elements of $s$ satisfy $P$, then $y$ satisfies $P$ and is related to every element of $s$ via $r$, then the function `seqOfForallFinsetExistsAux` constructs a sequence in $\alpha$ indexed by natural numbers. For each $n$, the $n$-th element of the sequence is chosen (using the axiom of choice) to satisfy $P$ and be related via $r$ to all previous elements in the sequence (i.e., those indexed by $i < n$).
exists_seq_of_forall_finset_exists theorem
{α : Type*} (P : α → Prop) (r : α → α → Prop) (h : ∀ s : Finset α, (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y) : ∃ f : ℕ → α, (∀ n, P (f n)) ∧ ∀ m n, m < n → r (f m) (f n)
Full source 
/-- Induction principle to build a sequence, by adding one point at a time satisfying a given
relation with respect to all the previously chosen points.

More precisely, Assume that, for any finite set `s`, one can find another point satisfying
some relation `r` with respect to all the points in `s`. Then one may construct a
function `f : ℕ → α` such that `r (f m) (f n)` holds whenever `m < n`.
We also ensure that all constructed points satisfy a given predicate `P`. -/
theorem exists_seq_of_forall_finset_exists {α : Type*} (P : α → Prop) (r : α → α → Prop)
    (h : ∀ s : Finset α, (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y) :
    ∃ f : ℕ → α, (∀ n, P (f n)) ∧ ∀ m n, m < n → r (f m) (f n) := by
  classical
    have : Nonempty α := by
      rcases h ∅ (by simp) with ⟨y, _⟩
      exact ⟨y⟩
    choose! F hF using h
    have h' : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y := fun s => ⟨F s, hF s⟩
    set f := seqOfForallFinsetExistsAux P r h' with hf
    have A : ∀ n : ℕ, P (f n) := by
      intro n
      induction' n using Nat.strong_induction_on with n IH
      have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
      rw [hf, seqOfForallFinsetExistsAux]
      exact
        (Classical.choose_spec
            (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n))))
            (by simp [IH'])).1
    refine ⟨f, A, fun m n hmn => ?_⟩
    conv_rhs => rw [hf]
    rw [seqOfForallFinsetExistsAux]
    apply
      (Classical.choose_spec
          (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [A])).2
    exact Finset.mem_image.2 ⟨⟨m, hmn⟩, Finset.mem_univ _, rfl⟩
Existence of Sequence Satisfying Predicate and Pairwise Relation from Finite Subset Condition
Informal description
Given a type $\alpha$, a predicate $P$ on $\alpha$, and a binary relation $r$ on $\alpha$, if for every finite subset $s$ of $\alpha$ where all elements satisfy $P$, there exists an element $y$ satisfying $P$ and related via $r$ to all elements of $s$, then there exists a sequence $f : \mathbb{N} \to \alpha$ such that: 1. For every $n \in \mathbb{N}$, $P(f(n))$ holds. 2. For any $m, n \in \mathbb{N}$ with $m < n$, the relation $r(f(m), f(n))$ holds.
exists_seq_of_forall_finset_exists' theorem
{α : Type*} (P : α → Prop) (r : α → α → Prop) [IsSymm α r] (h : ∀ s : Finset α, (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y) : ∃ f : ℕ → α, (∀ n, P (f n)) ∧ Pairwise (r on f)
Full source 
/-- Induction principle to build a sequence, by adding one point at a time satisfying a given
symmetric relation with respect to all the previously chosen points.

More precisely, Assume that, for any finite set `s`, one can find another point satisfying
some relation `r` with respect to all the points in `s`. Then one may construct a
function `f : ℕ → α` such that `r (f m) (f n)` holds whenever `m ≠ n`.
We also ensure that all constructed points satisfy a given predicate `P`. -/
theorem exists_seq_of_forall_finset_exists' {α : Type*} (P : α → Prop) (r : α → α → Prop)
    [IsSymm α r] (h : ∀ s : Finset α, (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y) :
    ∃ f : ℕ → α, (∀ n, P (f n)) ∧ Pairwise (r on f) := by
  rcases exists_seq_of_forall_finset_exists P r h with ⟨f, hf, hf'⟩
  refine ⟨f, hf, fun m n hmn => ?_⟩
  rcases lt_trichotomy m n with (h | rfl | h)
  · exact hf' m n h
  · exact (hmn rfl).elim
  · unfold Function.onFun
    apply symm
    exact hf' n m h
Existence of Pairwise-Related Sequence Satisfying Predicate from Finite Extension Property
Informal description
Let $\alpha$ be a type, $P$ a predicate on $\alpha$, and $r$ a symmetric binary relation on $\alpha$. Suppose that for every finite subset $s \subseteq \alpha$ where all elements satisfy $P$, there exists an element $y \in \alpha$ such that $P(y)$ holds and $r(x,y)$ holds for all $x \in s$. Then there exists a sequence $f \colon \mathbb{N} \to \alpha$ such that: 1. For every $n \in \mathbb{N}$, $P(f(n))$ holds. 2. The relation $r$ holds pairwise on the sequence, i.e., $r(f(m), f(n))$ for all $m \neq n$.