doc-next-gen

Mathlib.Data.Finset.Basic

Module docstring

{"# Basic lemmas on finite sets

This file contains lemmas on the interaction of various definitions on the Finset type.

For an explanation of Finset design decisions, please see Mathlib/Data/Finset/Defs.lean.

Main declarations

Main definitions

  • Finset.choose: Given a proof h of existence and uniqueness of a certain element satisfying a predicate, choose s h returns the element of s satisfying that predicate.

Equivalences between finsets

  • The Mathlib/Logic/Equiv/Defs.lean file describes a general type of equivalence, so look in there for any lemmas. There is some API for rewriting sums and products from s to t given that s ≃ t. TODO: examples

Tags

finite sets, finset

","### Lattice structure ","#### union ","#### inter ","### erase ","### sdiff ","### attach ","### filter ","### range ","### dedup on list and multiset ","### choose "}

Finset.sizeOf_lt_sizeOf_of_mem theorem
[SizeOf α] {x : α} {s : Finset α} (hx : x ∈ s) : SizeOf.sizeOf x < SizeOf.sizeOf s
Full source 
@[deprecated "Deprecated without replacement." (since := "2025-02-07")]
theorem sizeOf_lt_sizeOf_of_mem [SizeOf α] {x : α} {s : Finset α} (hx : x ∈ s) :
    SizeOf.sizeOf x < SizeOf.sizeOf s := by
  cases s
  dsimp [SizeOf.sizeOf, SizeOf.sizeOf, Multiset.sizeOf]
  rw [Nat.add_comm]
  refine lt_trans ?_ (Nat.lt_succ_self _)
  exact Multiset.sizeOf_lt_sizeOf_of_mem hx
Size Comparison for Elements in a Finite Set: $\text{sizeOf}(x) < \text{sizeOf}(s)$ if $x \in s$
Informal description
For any type $\alpha$ with a size function, if an element $x \in \alpha$ belongs to a finite set $s$ (i.e., $x \in s$), then the size of $x$ is strictly less than the size of $s$.
Finset.disjUnion_eq_union theorem
(s t h) : @disjUnion α s t h = s ∪ t
Full source 
@[simp]
theorem disjUnion_eq_union (s t h) : @disjUnion α s t h = s ∪ t :=
  ext fun a => by simp
Disjoint Union Equals Standard Union for Finite Sets
Informal description
For any two finite sets $s$ and $t$ of type $\alpha$ and a proof $h$ that they are disjoint, the disjoint union $\text{disjUnion}\ s\ t\ h$ is equal to the standard union $s \cup t$.
Finset.disjoint_union_left theorem
: Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u
Full source 
@[simp]
theorem disjoint_union_left : DisjointDisjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u := by
  simp only [disjoint_left, mem_union, or_imp, forall_and]
Disjointness of Union with Respect to Another Set: $s \cup t \perp u \leftrightarrow s \perp u \wedge t \perp u$
Informal description
For any finite sets $s$, $t$, and $u$ of a type $\alpha$, the union $s \cup t$ is disjoint from $u$ if and only if both $s$ is disjoint from $u$ and $t$ is disjoint from $u$.
Finset.disjoint_of_subset_iff_left_eq_empty theorem
(h : s ⊆ t) : Disjoint s t ↔ s = ∅
Full source 
theorem disjoint_of_subset_iff_left_eq_empty (h : s ⊆ t) :
    DisjointDisjoint s t ↔ s = ∅ :=
  disjoint_of_le_iff_left_eq_bot h
Disjointness Criterion for Subsets: $s \subseteq t \Rightarrow (s \cap t = \emptyset \leftrightarrow s = \emptyset)$
Informal description
For any finite subsets $s$ and $t$ of a type $\alpha$, if $s$ is a subset of $t$, then $s$ and $t$ are disjoint if and only if $s$ is the empty set. In other words, $s \cap t = \emptyset \leftrightarrow s = \emptyset$ under the assumption that $s \subseteq t$.
Finset.pairwiseDisjoint_iff theorem
{ι : Type*} {s : Set ι} {f : ι → Finset α} : s.PairwiseDisjoint f ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j
Full source 
lemma pairwiseDisjoint_iff {ι : Type*} {s : Set ι} {f : ι → Finset α} :
    s.PairwiseDisjoint f ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j := by
  simp [Set.PairwiseDisjoint, Set.Pairwise, Function.onFun, not_imp_comm (a := _ = _),
    not_disjoint_iff_nonempty_inter]
Characterization of Pairwise Disjoint Finite Sets: $f(i) \cap f(j) \neq \emptyset \Rightarrow i = j$
Informal description
For any type $\alpha$ and any set $s$ of indices of type $\iota$ with a function $f \colon \iota \to \text{Finset } \alpha$, the following are equivalent: 1. The images $f(i)$ and $f(j)$ are disjoint for all distinct $i, j \in s$. 2. For any $i, j \in s$, if the intersection $f(i) \cap f(j)$ is nonempty, then $i = j$.
Finset.isDirected_le instance
: IsDirected (Finset α) (· ≤ ·)
Full source 
instance isDirected_le : IsDirected (Finset α) (· ≤ ·) := by classical infer_instance
Finite Subsets are Directed under Inclusion
Informal description
The collection of finite subsets of a type $\alpha$ is directed with respect to the partial order $\leq$ (subset inclusion). That is, for any two finite subsets $s$ and $t$ of $\alpha$, there exists a finite subset $u$ such that $s \subseteq u$ and $t \subseteq u$.
Finset.isDirected_subset instance
: IsDirected (Finset α) (· ⊆ ·)
Full source 
instance isDirected_subset : IsDirected (Finset α) (· ⊆ ·) := isDirected_le
Finite Subsets are Directed under Subset Inclusion
Informal description
The collection of finite subsets of a type $\alpha$ is directed with respect to the subset relation $\subseteq$. That is, for any two finite subsets $s$ and $t$ of $\alpha$, there exists a finite subset $u$ such that $s \subseteq u$ and $t \subseteq u$.
Finset.erase_empty theorem
(a : α) : erase ∅ a = ∅
Full source 
@[simp]
theorem erase_empty (a : α) : erase ∅ a = ∅ :=
  rfl
Erasure from Empty Set Yields Empty Set
Informal description
For any element $a$ of type $\alpha$, erasing $a$ from the empty finite set $\emptyset$ yields the empty set, i.e., $\text{erase}(\emptyset, a) = \emptyset$.
Finset.Nontrivial.erase_nonempty theorem
(hs : s.Nontrivial) : (s.erase a).Nonempty
Full source 
protected lemma Nontrivial.erase_nonempty (hs : s.Nontrivial) : (s.erase a).Nonempty :=
  (hs.exists_ne a).imp <| by aesop
Nonemptiness of Finite Set After Erasure of Nontrivial Set
Informal description
For any finite set $s$ of type $\alpha$, if $s$ is nontrivial (i.e., contains at least two distinct elements), then the set obtained by removing any element $a$ from $s$ is nonempty.
Finset.erase_nonempty theorem
(ha : a ∈ s) : (s.erase a).Nonempty ↔ s.Nontrivial
Full source 
@[simp] lemma erase_nonempty (ha : a ∈ s) : (s.erase a).Nonempty ↔ s.Nontrivial := by
  simp only [Finset.Nonempty, mem_erase, and_comm (b := _ ∈ _)]
  refine ⟨?_, fun hs ↦ hs.exists_ne a⟩
  rintro ⟨b, hb, hba⟩
  exact ⟨_, hb, _, ha, hba⟩
Nonemptiness of Finite Set After Erasure if and only if Set is Nontrivial
Informal description
For a finite set $s$ and an element $a \in s$, the set $s \setminus \{a\}$ is nonempty if and only if $s$ contains at least two distinct elements.
Finset.erase_singleton theorem
(a : α) : ({ a } : Finset α).erase a = ∅
Full source 
@[simp]
theorem erase_singleton (a : α) : ({a} : Finset α).erase a = ∅ := by
  ext x
  simp
Erasing a Singleton Yields the Empty Set
Informal description
For any element $a$ of type $\alpha$, the finite set $\{a\}$ with $a$ removed equals the empty set, i.e., $\{a\} \setminus \{a\} = \emptyset$.
Finset.erase_insert_eq_erase theorem
(s : Finset α) (a : α) : (insert a s).erase a = s.erase a
Full source 
@[simp]
theorem erase_insert_eq_erase (s : Finset α) (a : α) : (insert a s).erase a = s.erase a :=
  ext fun x => by
    simp +contextual only [mem_erase, mem_insert, and_congr_right_iff,
      false_or, iff_self, imp_true_iff]
Insert-Erase Commutation: $(s \cup \{a\}) \setminus \{a\} = s \setminus \{a\}$
Informal description
For any finite set $s$ of type $\alpha$ and any element $a \in \alpha$, the operation of first inserting $a$ into $s$ and then erasing $a$ from the result yields the same set as erasing $a$ from $s$ directly. In other words, $(s \cup \{a\}) \setminus \{a\} = s \setminus \{a\}$.
Finset.erase_insert theorem
{a : α} {s : Finset α} (h : a ∉ s) : erase (insert a s) a = s
Full source 
theorem erase_insert {a : α} {s : Finset α} (h : a ∉ s) : erase (insert a s) a = s := by
  rw [erase_insert_eq_erase, erase_eq_of_not_mem h]
Erase-Insert Identity for Non-member Elements in Finite Sets
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of elements of $\alpha$, if $a$ does not belong to $s$, then erasing $a$ from the set obtained by inserting $a$ into $s$ yields $s$ itself. In symbols: $$\text{erase}(\text{insert}(a, s), a) = s$$
Finset.erase_insert_of_ne theorem
{a b : α} {s : Finset α} (h : a ≠ b) : erase (insert a s) b = insert a (erase s b)
Full source 
theorem erase_insert_of_ne {a b : α} {s : Finset α} (h : a ≠ b) :
    erase (insert a s) b = insert a (erase s b) :=
  ext fun x => by
    have : x ≠ bx ≠ b ∧ x = ax ≠ b ∧ x = a ↔ x = a := and_iff_right_of_imp fun hx => hx.symm ▸ h
    simp only [mem_erase, mem_insert, and_or_left, this]
Commutation of Erase and Insert for Distinct Elements in Finite Sets
Informal description
For any two distinct elements $a$ and $b$ of a type $\alpha$, and any finite set $s$ of elements of $\alpha$, the operation of erasing $b$ from the set obtained by inserting $a$ into $s$ is equal to inserting $a$ into the set obtained by erasing $b$ from $s$. In symbols: $$\text{erase}(\text{insert}(a, s), b) = \text{insert}(a, \text{erase}(s, b))$$
Finset.erase_cons_of_ne theorem
{a b : α} {s : Finset α} (ha : a ∉ s) (hb : a ≠ b) : erase (cons a s ha) b = cons a (erase s b) fun h => ha <| erase_subset _ _ h
Full source 
theorem erase_cons_of_ne {a b : α} {s : Finset α} (ha : a ∉ s) (hb : a ≠ b) :
    erase (cons a s ha) b = cons a (erase s b) fun h => ha <| erase_subset _ _ h := by
  simp only [cons_eq_insert, erase_insert_of_ne hb]
Commutation of Erase and Cons for Distinct Elements in Finite Sets
Informal description
For any two distinct elements $a$ and $b$ of a type $\alpha$, and any finite set $s$ of elements of $\alpha$ such that $a \notin s$, the operation of erasing $b$ from the set obtained by adding $a$ to $s$ (via `cons`) is equal to adding $a$ to the set obtained by erasing $b$ from $s$. More precisely, if $a \notin s$ and $a \neq b$, then: $$\text{erase}(\text{cons}(a, s, \text{ha}), b) = \text{cons}(a, \text{erase}(s, b), \lambda h, \text{ha} (\text{erase\_subset} b s h))$$ where $\text{ha}$ is the proof that $a \notin s$, and $\text{erase\_subset}$ ensures that erasing $b$ from $s$ preserves the property that $a \notin \text{erase}(s, b)$.
Finset.insert_erase theorem
(h : a ∈ s) : insert a (erase s a) = s
Full source 
@[simp] theorem insert_erase (h : a ∈ s) : insert a (erase s a) = s :=
  ext fun x => by
    simp only [mem_insert, mem_erase, or_and_left, dec_em, true_and]
    apply or_iff_right_of_imp
    rintro rfl
    exact h
Insertion and Erasure Inverse Property for Finite Sets
Informal description
For any finite set $s$ and any element $a \in s$, the insertion of $a$ into the set obtained by removing $a$ from $s$ results in the original set $s$. In other words, $\{a\} \cup (s \setminus \{a\}) = s$.
Finset.erase_eq_iff_eq_insert theorem
(hs : a ∈ s) (ht : a ∉ t) : erase s a = t ↔ s = insert a t
Full source 
lemma erase_eq_iff_eq_insert (hs : a ∈ s) (ht : a ∉ t) : eraseerase s a = t ↔ s = insert a t := by
  aesop
Erasure-Insertion Equivalence for Finite Sets: $s \setminus \{a\} = t \leftrightarrow s = \{a\} \cup t$
Informal description
For any finite set $s$ and element $a \in s$, and any finite set $t$ with $a \notin t$, the equality $s \setminus \{a\} = t$ holds if and only if $s = \{a\} \cup t$.
Finset.insert_erase_invOn theorem
: Set.InvOn (insert a) (fun s ↦ erase s a) {s : Finset α | a ∈ s} {s : Finset α | a ∉ s}
Full source 
lemma insert_erase_invOn :
    Set.InvOn (insert a) (fun s ↦ erase s a) {s : Finset α | a ∈ s} {s : Finset α | a ∉ s} :=
  ⟨fun _s ↦ insert_erase, fun _s ↦ erase_insert⟩
Inverse Relationship Between Insertion and Erasure in Finite Sets
Informal description
For any element $a$ of type $\alpha$, the functions $\text{insert}(a, \cdot)$ and $\text{erase}(\cdot, a)$ are mutual inverses when restricted to appropriate sets. Specifically: 1. $\text{insert}(a, \cdot)$ is a left inverse of $\text{erase}(\cdot, a)$ on the set $\{s \mid a \in s\}$ of finite sets containing $a$. 2. $\text{erase}(\cdot, a)$ is a right inverse of $\text{insert}(a, \cdot)$ on the set $\{s \mid a \notin s\}$ of finite sets not containing $a$. In other words, the pair $(\text{insert}(a, \cdot), \text{erase}(\cdot, a))$ forms a bijection between: - The collection of finite sets containing $a$ - The collection of finite sets not containing $a$
Finset.ssubset_iff_exists_subset_erase theorem
{s t : Finset α} : s ⊂ t ↔ ∃ a ∈ t, s ⊆ t.erase a
Full source 
theorem ssubset_iff_exists_subset_erase {s t : Finset α} : s ⊂ ts ⊂ t ↔ ∃ a ∈ t, s ⊆ t.erase a := by
  refine ⟨fun h => ?_, fun ⟨a, ha, h⟩ => ssubset_of_subset_of_ssubset h <| erase_ssubset ha⟩
  obtain ⟨a, ht, hs⟩ := not_subset.1 h.2
  exact ⟨a, ht, subset_erase.2 ⟨h.1, hs⟩⟩
Characterization of Strict Subset via Element Erasure: $s \subset t \leftrightarrow \exists a \in t, s \subseteq t \setminus \{a\}$
Informal description
For any two finite sets $s$ and $t$ of elements of type $\alpha$, the set $s$ is a strict subset of $t$ if and only if there exists an element $a \in t$ such that $s$ is a subset of $t \setminus \{a\}$. In other words: $$ s \subset t \leftrightarrow \exists a \in t, s \subseteq t \setminus \{a\}. $$
Finset.erase_ssubset_insert theorem
(s : Finset α) (a : α) : s.erase a ⊂ insert a s
Full source 
theorem erase_ssubset_insert (s : Finset α) (a : α) : s.erase a ⊂ insert a s :=
  ssubset_iff_exists_subset_erase.2
    ⟨a, mem_insert_self _ _, erase_subset_erase _ <| subset_insert _ _⟩
Strict subset relation between erasure and insertion: $s \setminus \{a\} \subset s \cup \{a\}$
Informal description
For any finite set $s$ of elements of type $\alpha$ and any element $a \in \alpha$, the set obtained by removing $a$ from $s$ is a strict subset of the set obtained by inserting $a$ into $s$, i.e., $s \setminus \{a\} \subset s \cup \{a\}$.
Finset.erase_cons theorem
{s : Finset α} {a : α} (h : a ∉ s) : (s.cons a h).erase a = s
Full source 
theorem erase_cons {s : Finset α} {a : α} (h : a ∉ s) : (s.cons a h).erase a = s := by
  rw [cons_eq_insert, erase_insert_eq_erase, erase_eq_of_not_mem h]
Erasing Cons Element from Finite Set Yields Original Set
Informal description
For any finite set $s$ of type $\alpha$ and any element $a \in \alpha$ such that $a \notin s$, erasing $a$ from the set obtained by cons-ing $a$ to $s$ (with proof $h$ that $a \notin s$) yields the original set $s$. In other words, $(s \cup \{a\}) \setminus \{a\} = s$ when $a \notin s$.
Finset.subset_insert_iff theorem
{a : α} {s t : Finset α} : s ⊆ insert a t ↔ erase s a ⊆ t
Full source 
theorem subset_insert_iff {a : α} {s t : Finset α} : s ⊆ insert a ts ⊆ insert a t ↔ erase s a ⊆ t := by
  simp only [subset_iff, or_iff_not_imp_left, mem_erase, mem_insert, and_imp]
  exact forall_congr' fun x => forall_swap
Subset Relation with Insertion and Erasure in Finite Sets
Informal description
For any element $a$ of type $\alpha$ and any finite subsets $s$ and $t$ of $\alpha$, the subset relation $s \subseteq t \cup \{a\}$ holds if and only if $s \setminus \{a\} \subseteq t$.
Finset.erase_insert_subset theorem
(a : α) (s : Finset α) : erase (insert a s) a ⊆ s
Full source 
theorem erase_insert_subset (a : α) (s : Finset α) : eraseerase (insert a s) a ⊆ s :=
  subset_insert_iff.1 <| Subset.rfl
Subset property of insertion followed by erasure in finite sets
Informal description
For any element $a$ of type $\alpha$ and any finite subset $s$ of $\alpha$, the set obtained by first inserting $a$ into $s$ and then removing $a$ is a subset of $s$. In other words, $\text{erase}(\text{insert}(a, s), a) \subseteq s$.
Finset.insert_erase_subset theorem
(a : α) (s : Finset α) : s ⊆ insert a (erase s a)
Full source 
theorem insert_erase_subset (a : α) (s : Finset α) : s ⊆ insert a (erase s a) :=
  subset_insert_iff.2 <| Subset.rfl
Subset Property of Insertion and Erasure in Finite Sets
Informal description
For any element $a$ of type $\alpha$ and any finite subset $s$ of $\alpha$, the set $s$ is a subset of the set obtained by inserting $a$ into $s$ after removing $a$ (if present), i.e., $s \subseteq \{a\} \cup (s \setminus \{a\})$.
Finset.subset_insert_iff_of_not_mem theorem
(h : a ∉ s) : s ⊆ insert a t ↔ s ⊆ t
Full source 
theorem subset_insert_iff_of_not_mem (h : a ∉ s) : s ⊆ insert a ts ⊆ insert a t ↔ s ⊆ t := by
  rw [subset_insert_iff, erase_eq_of_not_mem h]
Subset Relation with Insertion for Non-member Elements in Finite Sets
Informal description
For any element $a$ of type $\alpha$ and any finite subsets $s$ and $t$ of $\alpha$, if $a$ does not belong to $s$, then $s$ is a subset of $t \cup \{a\}$ if and only if $s$ is a subset of $t$.
Finset.erase_injOn' theorem
(a : α) : {s : Finset α | a ∈ s}.InjOn fun s => erase s a
Full source 
theorem erase_injOn' (a : α) : { s : Finset α | a ∈ s }.InjOn fun s => erase s a :=
  fun s hs t ht (h : s.erase a = _) => by rw [← insert_erase hs, ← insert_erase ht, h]
Injectivity of Erasure on Finite Sets Containing a Given Element
Informal description
For any element $a$ of type $\alpha$, the function that erases $a$ from a finite set is injective on the collection of finite sets containing $a$. In other words, if $s_1$ and $s_2$ are finite sets containing $a$, then $s_1 \setminus \{a\} = s_2 \setminus \{a\}$ implies $s_1 = s_2$.
Finset.Nontrivial.exists_cons_eq theorem
{s : Finset α} (hs : s.Nontrivial) : ∃ t a ha b hb hab, (cons b t hb).cons a (mem_cons.not.2 <| not_or_intro hab ha) = s
Full source 
lemma Nontrivial.exists_cons_eq {s : Finset α} (hs : s.Nontrivial) :
    ∃ t a ha b hb hab, (cons b t hb).cons a (mem_cons.not.2 <| not_or_intro hab ha) = s := by
  classical
  obtain ⟨a, ha, b, hb, hab⟩ := hs
  have : b ∈ s.erase a := mem_erase.2 ⟨hab.symm, hb⟩
  refine ⟨(s.erase a).erase b, a, ?_, b, ?_, ?_, ?_⟩ <;>
    simp [insert_erase this, insert_erase ha, *]
Decomposition of Nontrivial Finite Set into Double Insertion
Informal description
For any nontrivial finite set $s$ (i.e., $s$ has at least two distinct elements), there exists a finite set $t$ and elements $a, b \in \alpha$ with proofs $ha : a \notin t$, $hb : b \notin t$, and $hab : a \neq b$, such that $s$ can be reconstructed by consecutively inserting $b$ and then $a$ into $t$ (with the insertion of $a$ preserving the non-membership condition).
Finset.erase_sdiff_erase theorem
(hab : a ≠ b) (hb : b ∈ s) : s.erase a \ s.erase b = { b }
Full source 
lemma erase_sdiff_erase (hab : a ≠ b) (hb : b ∈ s) : s.erase a \ s.erase b = {b} := by
  ext; aesop
Set Difference of Erasures Yields Singleton: $(s \setminus \{a\}) \setminus (s \setminus \{b\}) = \{b\}$ for $a \neq b$ and $b \in s$
Informal description
For any two distinct elements $a$ and $b$ in a finite set $s$ (with $b \in s$), the set difference between $s \setminus \{a\}$ and $s \setminus \{b\}$ is the singleton set $\{b\}$. In other words, $(s \setminus \{a\}) \setminus (s \setminus \{b\}) = \{b\}$.
Finset.sdiff_singleton_eq_erase theorem
(a : α) (s : Finset α) : s \ { a } = erase s a
Full source 
theorem sdiff_singleton_eq_erase (a : α) (s : Finset α) : s \ {a} = erase s a := by
  ext
  rw [mem_erase, mem_sdiff, mem_singleton, and_comm]
Set Difference with Singleton Equals Erasure
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of elements of $\alpha$, the set difference $s \setminus \{a\}$ is equal to the finite set obtained by erasing $a$ from $s$.
Finset.erase_eq theorem
(s : Finset α) (a : α) : s.erase a = s \ { a }
Full source 
theorem erase_eq (s : Finset α) (a : α) : s.erase a = s \ {a} :=
  (sdiff_singleton_eq_erase _ _).symm
Equality of Erasure and Set Difference for Finite Sets
Informal description
For any finite set $s$ of elements of type $\alpha$ and any element $a \in \alpha$, the set obtained by erasing $a$ from $s$ is equal to the set difference $s \setminus \{a\}$.
Finset.disjoint_erase_comm theorem
: Disjoint (s.erase a) t ↔ Disjoint s (t.erase a)
Full source 
theorem disjoint_erase_comm : DisjointDisjoint (s.erase a) t ↔ Disjoint s (t.erase a) := by
  simp_rw [erase_eq, disjoint_sdiff_comm]
Commutativity of Disjointness with Element Erasure: $\text{Disjoint}(s \setminus \{a\}, t) \leftrightarrow \text{Disjoint}(s, t \setminus \{a\})$
Informal description
For any finite sets $s$ and $t$ of elements of type $\alpha$ and any element $a \in \alpha$, the sets $s \setminus \{a\}$ and $t$ are disjoint if and only if $s$ and $t \setminus \{a\}$ are disjoint.
Finset.disjoint_insert_erase theorem
(ha : a ∉ t) : Disjoint (s.erase a) (insert a t) ↔ Disjoint s t
Full source 
lemma disjoint_insert_erase (ha : a ∉ t) : DisjointDisjoint (s.erase a) (insert a t) ↔ Disjoint s t := by
  rw [disjoint_erase_comm, erase_insert ha]
Disjointness Condition for Insert-Erase Operations: $\text{Disjoint}(s \setminus \{a\}, t \cup \{a\}) \leftrightarrow \text{Disjoint}(s, t)$
Informal description
For any finite sets $s$ and $t$ of elements of type $\alpha$ and any element $a \in \alpha$ such that $a \notin t$, the sets $s \setminus \{a\}$ and $t \cup \{a\}$ are disjoint if and only if $s$ and $t$ are disjoint.
Finset.disjoint_erase_insert theorem
(ha : a ∉ s) : Disjoint (insert a s) (t.erase a) ↔ Disjoint s t
Full source 
lemma disjoint_erase_insert (ha : a ∉ s) : DisjointDisjoint (insert a s) (t.erase a) ↔ Disjoint s t := by
  rw [← disjoint_erase_comm, erase_insert ha]
Disjointness Preservation under Insertion and Erasure: $\text{Disjoint}(\{a\} \cup s, t \setminus \{a\}) \leftrightarrow \text{Disjoint}(s, t)$
Informal description
For any finite sets $s$ and $t$ of elements of type $\alpha$ and any element $a \in \alpha$ such that $a \notin s$, the sets $\{a\} \cup s$ and $t \setminus \{a\}$ are disjoint if and only if $s$ and $t$ are disjoint. In symbols: $$\text{Disjoint}(\{a\} \cup s, t \setminus \{a\}) \leftrightarrow \text{Disjoint}(s, t)$$
Finset.disjoint_of_erase_left theorem
(ha : a ∉ t) (hst : Disjoint (s.erase a) t) : Disjoint s t
Full source 
theorem disjoint_of_erase_left (ha : a ∉ t) (hst : Disjoint (s.erase a) t) : Disjoint s t := by
  rw [← erase_insert ha, ← disjoint_erase_comm, disjoint_insert_right]
  exact ⟨not_mem_erase _ _, hst⟩
Disjointness Preservation Under Left Erasure: $a \notin t \land (s \setminus \{a\}) \cap t = \emptyset \implies s \cap t = \emptyset$
Informal description
For any finite sets $s$ and $t$ of elements of type $\alpha$ and any element $a \in \alpha$ such that $a \notin t$, if the set $s \setminus \{a\}$ is disjoint from $t$, then $s$ is disjoint from $t$.
Finset.disjoint_of_erase_right theorem
(ha : a ∉ s) (hst : Disjoint s (t.erase a)) : Disjoint s t
Full source 
theorem disjoint_of_erase_right (ha : a ∉ s) (hst : Disjoint s (t.erase a)) : Disjoint s t := by
  rw [← erase_insert ha, disjoint_erase_comm, disjoint_insert_left]
  exact ⟨not_mem_erase _ _, hst⟩
Disjointness Preservation Under Right Erasure: $a \notin s \land s \cap (t \setminus \{a\}) = \emptyset \implies s \cap t = \emptyset$
Informal description
For any finite sets $s$ and $t$ of elements of type $\alpha$ and any element $a \in \alpha$, if $a$ is not in $s$ and $s$ is disjoint from $t \setminus \{a\}$, then $s$ is disjoint from $t$.
Finset.inter_erase theorem
(a : α) (s t : Finset α) : s ∩ t.erase a = (s ∩ t).erase a
Full source 
theorem inter_erase (a : α) (s t : Finset α) : s ∩ t.erase a = (s ∩ t).erase a := by
  simp only [erase_eq, inter_sdiff_assoc]
Intersection with Erasure Equals Erasure of Intersection
Informal description
For any element $a$ of type $\alpha$ and any finite sets $s$ and $t$ of elements of type $\alpha$, the intersection of $s$ with the set obtained by erasing $a$ from $t$ is equal to the set obtained by erasing $a$ from the intersection of $s$ and $t$. In symbols: $$ s \cap (t \setminus \{a\}) = (s \cap t) \setminus \{a\}. $$
Finset.erase_inter theorem
(a : α) (s t : Finset α) : s.erase a ∩ t = (s ∩ t).erase a
Full source 
@[simp]
theorem erase_inter (a : α) (s t : Finset α) : s.erase a ∩ t = (s ∩ t).erase a := by
  simpa only [inter_comm t] using inter_erase a t s
Erasure-Intersection Commutativity for Finite Sets
Informal description
For any element $a$ of type $\alpha$ and any finite sets $s$ and $t$ of elements of type $\alpha$, the intersection of the set obtained by erasing $a$ from $s$ with $t$ is equal to the set obtained by erasing $a$ from the intersection of $s$ and $t$. In symbols: $$ (s \setminus \{a\}) \cap t = (s \cap t) \setminus \{a\}. $$
Finset.erase_sdiff_comm theorem
(s t : Finset α) (a : α) : s.erase a \ t = (s \ t).erase a
Full source 
theorem erase_sdiff_comm (s t : Finset α) (a : α) : s.erase a \ t = (s \ t).erase a := by
  simp_rw [erase_eq, sdiff_right_comm]
Commutativity of Erasure and Set Difference for Finite Sets
Informal description
For any finite sets $s$ and $t$ of elements of type $\alpha$ and any element $a \in \alpha$, the set difference of $s \setminus \{a\}$ and $t$ is equal to the set obtained by erasing $a$ from the set difference $s \setminus t$. In symbols: $$(s \setminus \{a\}) \setminus t = (s \setminus t) \setminus \{a\}.$$
Finset.erase_inter_comm theorem
(s t : Finset α) (a : α) : s.erase a ∩ t = s ∩ t.erase a
Full source 
theorem erase_inter_comm (s t : Finset α) (a : α) : s.erase a ∩ t = s ∩ t.erase a := by
  rw [erase_inter, inter_erase]
Commutativity of Erasure and Intersection for Finite Sets
Informal description
For any finite sets $s$ and $t$ of elements of type $\alpha$ and any element $a \in \alpha$, the intersection of the set obtained by erasing $a$ from $s$ with $t$ is equal to the intersection of $s$ with the set obtained by erasing $a$ from $t$. In symbols: $$ (s \setminus \{a\}) \cap t = s \cap (t \setminus \{a\}). $$
Finset.erase_union_distrib theorem
(s t : Finset α) (a : α) : (s ∪ t).erase a = s.erase a ∪ t.erase a
Full source 
theorem erase_union_distrib (s t : Finset α) (a : α) : (s ∪ t).erase a = s.erase a ∪ t.erase a := by
  simp_rw [erase_eq, union_sdiff_distrib]
Distributivity of Erasure over Union in Finite Sets
Informal description
For any finite sets $s$ and $t$ of elements of type $\alpha$ and any element $a \in \alpha$, the erasure of $a$ from the union $s \cup t$ is equal to the union of the erasures of $a$ from $s$ and $t$: $$(s \cup t) \setminus \{a\} = (s \setminus \{a\}) \cup (t \setminus \{a\}).$$
Finset.insert_inter_distrib theorem
(s t : Finset α) (a : α) : insert a (s ∩ t) = insert a s ∩ insert a t
Full source 
theorem insert_inter_distrib (s t : Finset α) (a : α) :
    insert a (s ∩ t) = insertinsert a s ∩ insert a t := by simp_rw [insert_eq, union_inter_distrib_left]
Insertion Distributes over Intersection in Finite Sets: $\{a\} \cup (s \cap t) = (\{a\} \cup s) \cap (\{a\} \cup t)$
Informal description
For any finite sets $s$ and $t$ of elements of type $\alpha$ and any element $a \in \alpha$, the insertion of $a$ into the intersection $s \cap t$ is equal to the intersection of the insertions of $a$ into $s$ and $t$: $$ \{a\} \cup (s \cap t) = (\{a\} \cup s) \cap (\{a\} \cup t). $$
Finset.erase_sdiff_distrib theorem
(s t : Finset α) (a : α) : (s \ t).erase a = s.erase a \ t.erase a
Full source 
theorem erase_sdiff_distrib (s t : Finset α) (a : α) : (s \ t).erase a = s.erase a \ t.erase a := by
  simp_rw [erase_eq, sdiff_sdiff, sup_sdiff_eq_sup le_rfl, sup_comm]
Erasure Distributes over Set Difference in Finite Sets
Informal description
For any finite sets $s$ and $t$ of elements of type $\alpha$ and any element $a \in \alpha$, the erasure of $a$ from the set difference $s \setminus t$ is equal to the set difference of the erasures, i.e., $(s \setminus t) \setminus \{a\} = (s \setminus \{a\}) \setminus (t \setminus \{a\})$.
Finset.erase_union_of_mem theorem
(ha : a ∈ t) (s : Finset α) : s.erase a ∪ t = s ∪ t
Full source 
theorem erase_union_of_mem (ha : a ∈ t) (s : Finset α) : s.erase a ∪ t = s ∪ t := by
  rw [← insert_erase (mem_union_right s ha), erase_union_distrib, ← union_insert, insert_erase ha]
Union with Erasure Cancellation: $(s \setminus \{a\}) \cup t = s \cup t$ for $a \in t$
Informal description
For any finite set $s$ of elements of type $\alpha$ and any element $a$ that belongs to another finite set $t$ of elements of $\alpha$, the union of the set $s$ with $a$ removed and the set $t$ is equal to the union of $s$ and $t$. In other words, $(s \setminus \{a\}) \cup t = s \cup t$.
Finset.union_erase_of_mem theorem
(ha : a ∈ s) (t : Finset α) : s ∪ t.erase a = s ∪ t
Full source 
theorem union_erase_of_mem (ha : a ∈ s) (t : Finset α) : s ∪ t.erase a = s ∪ t := by
  rw [← insert_erase (mem_union_left t ha), erase_union_distrib, ← insert_union, insert_erase ha]
Union with Erasure Preserves Union for Contained Elements
Informal description
For any finite sets $s$ and $t$ of elements of type $\alpha$ and any element $a \in s$, the union of $s$ with the set obtained by removing $a$ from $t$ is equal to the union of $s$ with $t$. In other words, $s \cup (t \setminus \{a\}) = s \cup t$.
Finset.sdiff_union_erase_cancel theorem
(hts : t ⊆ s) (ha : a ∈ t) : s \ t ∪ t.erase a = s.erase a
Full source 
theorem sdiff_union_erase_cancel (hts : t ⊆ s) (ha : a ∈ t) : s \ ts \ t ∪ t.erase a = s.erase a := by
  simp_rw [erase_eq, sdiff_union_sdiff_cancel hts (singleton_subset_iff.2 ha)]
Set Difference and Erasure Cancellation: $(s \setminus t) \cup (t \setminus \{a\}) = s \setminus \{a\}$ for $a \in t \subseteq s$
Informal description
For any finite sets $s$ and $t$ of elements of type $\alpha$ such that $t \subseteq s$, and any element $a \in t$, the union of the set difference $s \setminus t$ and the set $t$ with $a$ removed equals the set $s$ with $a$ removed. In other words, $(s \setminus t) \cup (t \setminus \{a\}) = s \setminus \{a\}$.
Finset.sdiff_insert theorem
(s t : Finset α) (x : α) : s \ insert x t = (s \ t).erase x
Full source 
theorem sdiff_insert (s t : Finset α) (x : α) : s \ insert x t = (s \ t).erase x := by
  simp_rw [← sdiff_singleton_eq_erase, insert_eq, sdiff_sdiff_left', sdiff_union_distrib,
    inter_comm]
Set Difference with Inserted Element Equals Erasure of Set Difference
Informal description
For any finite sets $s$ and $t$ of elements of type $\alpha$ and any element $x \in \alpha$, the set difference $s \setminus (t \cup \{x\})$ is equal to $(s \setminus t) \setminus \{x\}$.
Finset.sdiff_insert_insert_of_mem_of_not_mem theorem
{s t : Finset α} {x : α} (hxs : x ∈ s) (hxt : x ∉ t) : insert x (s \ insert x t) = s \ t
Full source 
theorem sdiff_insert_insert_of_mem_of_not_mem {s t : Finset α} {x : α} (hxs : x ∈ s) (hxt : x ∉ t) :
    insert x (s \ insert x t) = s \ t := by
  rw [sdiff_insert, insert_erase (mem_sdiff.mpr ⟨hxs, hxt⟩)]
Insertion and Set Difference Property for Finite Sets
Informal description
For any finite sets $s$ and $t$ of elements of type $\alpha$, and any element $x \in \alpha$ such that $x \in s$ and $x \notin t$, the set obtained by inserting $x$ into the difference $s \setminus (t \cup \{x\})$ equals the difference $s \setminus t$. In other words, $\{x\} \cup (s \setminus (t \cup \{x\})) = s \setminus t$.
Finset.sdiff_erase theorem
(h : a ∈ s) : s \ t.erase a = insert a (s \ t)
Full source 
theorem sdiff_erase (h : a ∈ s) : s \ t.erase a = insert a (s \ t) := by
  rw [← sdiff_singleton_eq_erase, sdiff_sdiff_eq_sdiff_union (singleton_subset_iff.2 h), insert_eq,
    union_comm]
Set Difference with Erased Element Equals Insertion of Set Difference
Informal description
For any finite sets $s$ and $t$ of elements of type $\alpha$ and any element $a \in s$, the set difference $s \setminus (t \setminus \{a\})$ is equal to the insertion of $a$ into $s \setminus t$, i.e., $s \setminus t.\text{erase}(a) = \{a\} \cup (s \setminus t)$.
Finset.sdiff_erase_self theorem
(ha : a ∈ s) : s \ s.erase a = { a }
Full source 
theorem sdiff_erase_self (ha : a ∈ s) : s \ s.erase a = {a} := by
  rw [sdiff_erase ha, Finset.sdiff_self, insert_empty_eq]
Set Difference with Self-Erasure Yields Singleton: $s \setminus (s \setminus \{a\}) = \{a\}$
Informal description
For any finite set $s$ and any element $a \in s$, the set difference $s \setminus (s \setminus \{a\})$ is equal to the singleton set $\{a\}$.
Finset.erase_eq_empty_iff theorem
(s : Finset α) (a : α) : s.erase a = ∅ ↔ s = ∅ ∨ s = { a }
Full source 
theorem erase_eq_empty_iff (s : Finset α) (a : α) : s.erase a = ∅ ↔ s = ∅ ∨ s = {a} := by
  rw [← sdiff_singleton_eq_erase, sdiff_eq_empty_iff_subset, subset_singleton_iff]
Empty Erasure Condition for Finite Sets: $s \setminus \{a\} = \emptyset \leftrightarrow s = \emptyset \lor s = \{a\}$
Informal description
For any finite set $s$ of elements of type $\alpha$ and any element $a \in \alpha$, the set obtained by erasing $a$ from $s$ is empty if and only if $s$ is either empty or equal to the singleton set $\{a\}$.
Finset.sdiff_disjoint theorem
: Disjoint (t \ s) s
Full source 
theorem sdiff_disjoint : Disjoint (t \ s) s :=
  disjoint_left.2 fun _a ha => (mem_sdiff.1 ha).2
Disjointness of Set Difference: $(t \setminus s) \cap s = \emptyset$
Informal description
For any finite sets $s$ and $t$ of elements of type $\alpha$, the set difference $t \setminus s$ is disjoint from $s$, i.e., $(t \setminus s) \cap s = \emptyset$.
Finset.disjoint_sdiff theorem
: Disjoint s (t \ s)
Full source 
theorem disjoint_sdiff : Disjoint s (t \ s) :=
  sdiff_disjoint.symm
Disjointness of Set and Set Difference: $s \cap (t \setminus s) = \emptyset$
Informal description
For any finite sets $s$ and $t$ of elements of type $\alpha$, the set $s$ is disjoint from the set difference $t \setminus s$, i.e., $s \cap (t \setminus s) = \emptyset$.
Finset.attach_empty theorem
: attach (∅ : Finset α) = ∅
Full source 
@[simp]
theorem attach_empty : attach (∅ : Finset α) = ∅ :=
  rfl
Empty Set Attachment Yields Empty Set
Informal description
The attached finite set of the empty set is empty, i.e., $\operatorname{attach}(\emptyset) = \emptyset$.
Finset.attach_nonempty_iff theorem
{s : Finset α} : s.attach.Nonempty ↔ s.Nonempty
Full source 
@[simp]
theorem attach_nonempty_iff {s : Finset α} : s.attach.Nonempty ↔ s.Nonempty := by
  simp [Finset.Nonempty]
Nonempty Attached Finite Set iff Original Finite Set is Nonempty
Informal description
For any finite set $s$ of elements of type $\alpha$, the attached finite set (where each element is paired with a proof of its membership in $s$) is nonempty if and only if $s$ itself is nonempty.
Finset.attach_eq_empty_iff theorem
{s : Finset α} : s.attach = ∅ ↔ s = ∅
Full source 
@[simp]
theorem attach_eq_empty_iff {s : Finset α} : s.attach = ∅ ↔ s = ∅ := by
  simp [eq_empty_iff_forall_not_mem]
Empty Attached Finite Set iff Original Finite Set is Empty
Informal description
For any finite set $s$ of elements of type $\alpha$, the attached finite set (where each element is paired with a proof of its membership in $s$) is empty if and only if $s$ itself is empty.
Finset.filter_singleton theorem
(a : α) : filter p { a } = if p a then { a } else ∅
Full source 
theorem filter_singleton (a : α) : filter p {a} = if p a then {a} else ∅ := by
  classical
    ext x
    simp only [mem_singleton, forall_eq, mem_filter]
    split_ifs with h <;> by_cases h' : x = a <;> simp [h, h']
Filtering a Singleton Set
Informal description
For any element $a$ of type $\alpha$ and a decidable predicate $p$, the filtered set obtained by applying $p$ to the singleton set $\{a\}$ is equal to $\{a\}$ if $p(a)$ holds, and is the empty set otherwise. In symbols: \[ \text{filter } p \{a\} = \begin{cases} \{a\} & \text{if } p(a), \\ \emptyset & \text{otherwise.} \end{cases} \]
Finset.filter_cons_of_pos theorem
(a : α) (s : Finset α) (ha : a ∉ s) (hp : p a) : filter p (cons a s ha) = cons a (filter p s) ((mem_of_mem_filter _).mt ha)
Full source 
theorem filter_cons_of_pos (a : α) (s : Finset α) (ha : a ∉ s) (hp : p a) :
    filter p (cons a s ha) = cons a (filter p s) ((mem_of_mem_filter _).mt ha) :=
  eq_of_veq <| Multiset.filter_cons_of_pos s.val hp
Filtering a Finite Set with Positive Predicate on Added Element
Informal description
For any element $a$ of type $\alpha$, any finite set $s$ of elements of type $\alpha$ not containing $a$, and a decidable predicate $p$ such that $p(a)$ holds, the filtered set obtained by applying $p$ to the set formed by adding $a$ to $s$ is equal to the set formed by adding $a$ to the filtered version of $s$. In symbols: \[ \text{filter } p (\{a\} \cup s) = \{a\} \cup (\text{filter } p s) \quad \text{when} \quad a \notin s \text{ and } p(a). \]
Finset.filter_cons_of_neg theorem
(a : α) (s : Finset α) (ha : a ∉ s) (hp : ¬p a) : filter p (cons a s ha) = filter p s
Full source 
theorem filter_cons_of_neg (a : α) (s : Finset α) (ha : a ∉ s) (hp : ¬p a) :
    filter p (cons a s ha) = filter p s :=
  eq_of_veq <| Multiset.filter_cons_of_neg s.val hp
Filtering a Finite Set with Negated Predicate on Added Element
Informal description
For any element $a$ of type $\alpha$, any finite set $s$ of elements of type $\alpha$ not containing $a$, and a decidable predicate $p$ such that $\neg p(a)$, the filtered set obtained by applying $p$ to the set formed by adding $a$ to $s$ is equal to the filtered set obtained by applying $p$ to $s$ itself. In symbols: \[ \text{filter } p (\{a\} \cup s) = \text{filter } p s \quad \text{when} \quad a \notin s \text{ and } \neg p(a). \]
Finset.disjoint_filter theorem
{s : Finset α} {p q : α → Prop} [DecidablePred p] [DecidablePred q] : Disjoint (s.filter p) (s.filter q) ↔ ∀ x ∈ s, p x → ¬q x
Full source 
theorem disjoint_filter {s : Finset α} {p q : α → Prop} [DecidablePred p] [DecidablePred q] :
    DisjointDisjoint (s.filter p) (s.filter q) ↔ ∀ x ∈ s, p x → ¬q x := by
  constructor <;> simp +contextual [disjoint_left]
Disjointness of Filtered Finite Sets via Predicate Negation
Informal description
For any finite set $s$ of type $\alpha$ and any decidable predicates $p$ and $q$ on $\alpha$, the filtered sets $s \text{.filter } p$ and $s \text{.filter } q$ are disjoint if and only if for every element $x \in s$, if $p(x)$ holds then $q(x)$ does not hold. In symbols: \[ \text{Disjoint } (s \text{.filter } p) \ (s \text{.filter } q) \leftrightarrow \forall x \in s, \ p(x) \to \neg q(x). \]
Finset.disjoint_filter_filter' theorem
(s t : Finset α) {p q : α → Prop} [DecidablePred p] [DecidablePred q] (h : Disjoint p q) : Disjoint (s.filter p) (t.filter q)
Full source 
theorem disjoint_filter_filter' (s t : Finset α)
    {p q : α → Prop} [DecidablePred p] [DecidablePred q] (h : Disjoint p q) :
    Disjoint (s.filter p) (t.filter q) := by
  simp_rw [disjoint_left, mem_filter]
  rintro a ⟨_, hp⟩ ⟨_, hq⟩
  rw [Pi.disjoint_iff] at h
  simpa [hp, hq] using h a
Disjointness of Filtered Sets under Disjoint Predicates
Informal description
For any two finite sets $s$ and $t$ of type $\alpha$, and any two decidable predicates $p$ and $q$ on $\alpha$, if the predicates $p$ and $q$ are disjoint (i.e., there is no element $x$ for which both $p(x)$ and $q(x)$ hold), then the filtered sets $s \text{.filter } p$ and $t \text{.filter } q$ are disjoint as well. In other words, if $p$ and $q$ are mutually exclusive, then the subsets of $s$ and $t$ satisfying $p$ and $q$ respectively have no common elements.
Finset.disjoint_filter_filter_neg theorem
(s t : Finset α) (p : α → Prop) [DecidablePred p] [∀ x, Decidable (¬p x)] : Disjoint (s.filter p) (t.filter fun a => ¬p a)
Full source 
theorem disjoint_filter_filter_neg (s t : Finset α) (p : α → Prop)
    [DecidablePred p] [∀ x, Decidable (¬p x)] :
    Disjoint (s.filter p) (t.filter fun a => ¬p a) :=
  disjoint_filter_filter' s t disjoint_compl_right
Disjointness of Positively and Negatively Filtered Finite Sets
Informal description
For any two finite sets $s$ and $t$ of type $\alpha$, and any decidable predicate $p$ on $\alpha$ (with decidable negation), the filtered set $s \text{.filter } p$ is disjoint from the filtered set $t \text{.filter } (\neg p)$. In other words, the subset of $s$ satisfying $p$ and the subset of $t$ satisfying the negation of $p$ have no common elements.
Finset.filter_disj_union theorem
(s : Finset α) (t : Finset α) (h : Disjoint s t) : filter p (disjUnion s t h) = (filter p s).disjUnion (filter p t) (disjoint_filter_filter h)
Full source 
theorem filter_disj_union (s : Finset α) (t : Finset α) (h : Disjoint s t) :
    filter p (disjUnion s t h) = (filter p s).disjUnion (filter p t) (disjoint_filter_filter h) :=
  eq_of_veq <| Multiset.filter_add _ _ _
Filtering Preserves Disjoint Union of Finite Sets
Informal description
For any two disjoint finite sets $s$ and $t$ of type $\alpha$ and a decidable predicate $p : \alpha \to \text{Prop}$, the filter of the disjoint union $s \sqcup t$ under $p$ is equal to the disjoint union of the filtered sets $s.\mathrm{filter}\,p$ and $t.\mathrm{filter}\,p$. In symbols: $$ \mathrm{filter}\,p (s \sqcup t) = (\mathrm{filter}\,p s) \sqcup (\mathrm{filter}\,p t). $$
Finset.filter_cons theorem
{a : α} (s : Finset α) (ha : a ∉ s) : filter p (cons a s ha) = if p a then cons a (filter p s) ((mem_of_mem_filter _).mt ha) else filter p s
Full source 
theorem filter_cons {a : α} (s : Finset α) (ha : a ∉ s) :
    filter p (cons a s ha) =
      if p a then cons a (filter p s) ((mem_of_mem_filter _).mt ha) else filter p s := by
  split_ifs with h
  · rw [filter_cons_of_pos _ _ _ ha h]
  · rw [filter_cons_of_neg _ _ _ ha h]
Filtering a Finite Set After Adding an Element
Informal description
For any element $a$ of type $\alpha$, any finite set $s$ of elements of type $\alpha$ not containing $a$, and a decidable predicate $p$, the filtered set obtained by applying $p$ to the set formed by adding $a$ to $s$ is equal to: - $\{a\} \cup (\text{filter } p s)$ if $p(a)$ holds - $\text{filter } p s$ otherwise In symbols: \[ \text{filter } p (\{a\} \cup s) = \begin{cases} \{a\} \cup (\text{filter } p s) & \text{if } p(a) \\ \text{filter } p s & \text{otherwise} \end{cases} \] where $a \notin s$.
Finset.filter_union theorem
(s₁ s₂ : Finset α) : (s₁ ∪ s₂).filter p = s₁.filter p ∪ s₂.filter p
Full source 
theorem filter_union (s₁ s₂ : Finset α) : (s₁ ∪ s₂).filter p = s₁.filter p ∪ s₂.filter p :=
  ext fun _ => by simp only [mem_filter, mem_union, or_and_right]
Filtering Preserves Union of Finite Sets
Informal description
For any two finite sets $s_1$ and $s_2$ of type $\alpha$ and a decidable predicate $p : \alpha \to \text{Prop}$, the filter of the union $s_1 \cup s_2$ under $p$ is equal to the union of the filters of $s_1$ and $s_2$ under $p$. In other words, $$ \{x \in s_1 \cup s_2 \mid p(x)\} = \{x \in s_1 \mid p(x)\} \cup \{x \in s_2 \mid p(x)\}. $$
Finset.filter_union_right theorem
(s : Finset α) : s.filter p ∪ s.filter q = s.filter fun x => p x ∨ q x
Full source 
theorem filter_union_right (s : Finset α) : s.filter p ∪ s.filter q = s.filter fun x => p x ∨ q x :=
  ext fun x => by simp [mem_filter, mem_union, ← and_or_left]
Union of Filtered Sets Equals Filter of Union Predicates
Informal description
For any finite set $s$ of type $\alpha$ and predicates $p, q : \alpha \to \text{Prop}$, the union of the filtered sets $s \text{.filter } p$ and $s \text{.filter } q$ is equal to the finite set obtained by filtering $s$ with the disjunction of $p$ and $q$, i.e., $$ \{x \in s \mid p(x)\} \cup \{x \in s \mid q(x)\} = \{x \in s \mid p(x) \lor q(x)\}. $$
Finset.filter_mem_eq_inter theorem
{s t : Finset α} [∀ i, Decidable (i ∈ t)] : (s.filter fun i => i ∈ t) = s ∩ t
Full source 
theorem filter_mem_eq_inter {s t : Finset α} [∀ i, Decidable (i ∈ t)] :
    (s.filter fun i => i ∈ t) = s ∩ t :=
  ext fun i => by simp [mem_filter, mem_inter]
Filtered Membership Equals Intersection
Informal description
For any two finite sets $s$ and $t$ of type $\alpha$ with a decidable membership predicate for $t$, the filtered set $\{x \in s \mid x \in t\}$ is equal to the intersection $s \cap t$.
Finset.filter_inter_distrib theorem
(s t : Finset α) : (s ∩ t).filter p = s.filter p ∩ t.filter p
Full source 
theorem filter_inter_distrib (s t : Finset α) : (s ∩ t).filter p = s.filter p ∩ t.filter p := by
  ext
  simp [mem_filter, mem_inter, and_assoc]
Distributivity of Filter over Intersection for Finite Sets
Informal description
For any finite sets $s$ and $t$ of type $\alpha$ and any decidable predicate $p : \alpha \to \text{Prop}$, the filter of the intersection $s \cap t$ by $p$ is equal to the intersection of the filters of $s$ and $t$ by $p$, i.e., $$ \{x \in s \cap t \mid p(x)\} = \{x \in s \mid p(x)\} \cap \{x \in t \mid p(x)\}. $$
Finset.filter_inter theorem
(s t : Finset α) : filter p s ∩ t = filter p (s ∩ t)
Full source 
theorem filter_inter (s t : Finset α) : filterfilter p s ∩ t = filter p (s ∩ t) := by
  ext
  simp only [mem_inter, mem_filter, and_right_comm]
Filter-Intersection Commutativity for Finite Sets
Informal description
For any finite sets $s$ and $t$ of type $\alpha$ and a decidable predicate $p$, the intersection of the filtered set $\text{filter } p \ s$ with $t$ is equal to the filtered set obtained by applying $p$ to the intersection of $s$ and $t$. In symbols: \[ \text{filter } p \ s \cap t = \text{filter } p \ (s \cap t). \]
Finset.inter_filter theorem
(s t : Finset α) : s ∩ filter p t = filter p (s ∩ t)
Full source 
theorem inter_filter (s t : Finset α) : s ∩ filter p t = filter p (s ∩ t) := by
  rw [inter_comm, filter_inter, inter_comm]
Intersection-Filter Commutativity for Finite Sets
Informal description
For any finite sets $s$ and $t$ of a type $\alpha$ and any decidable predicate $p$ on $\alpha$, the intersection of $s$ with the filtered set $\{x \in t \mid p(x)\}$ is equal to the filtered set $\{x \in s \cap t \mid p(x)\}$. In symbols: $$ s \cap \{x \in t \mid p(x)\} = \{x \in s \cap t \mid p(x)\}. $$
Finset.filter_insert theorem
(a : α) (s : Finset α) : filter p (insert a s) = if p a then insert a (filter p s) else filter p s
Full source 
theorem filter_insert (a : α) (s : Finset α) :
    filter p (insert a s) = if p a then insert a (filter p s) else filter p s := by
  ext x
  split_ifs with h <;> by_cases h' : x = a <;> simp [h, h']
Filtering an Inserted Element in a Finite Set
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the filtered set obtained by applying predicate $p$ to the insertion of $a$ into $s$ is equal to: if $p(a)$ holds, then insert $a$ into the filtered set $p(s)$; otherwise, just take the filtered set $p(s)$. In symbols: $$ \text{filter } p \ (\text{insert } a \ s) = \begin{cases} \text{insert } a \ (\text{filter } p \ s) & \text{if } p(a) \\ \text{filter } p \ s & \text{otherwise} \end{cases} $$
Finset.filter_erase theorem
(a : α) (s : Finset α) : filter p (erase s a) = erase (filter p s) a
Full source 
theorem filter_erase (a : α) (s : Finset α) : filter p (erase s a) = erase (filter p s) a := by
  ext x
  simp only [and_assoc, mem_filter, iff_self, mem_erase]
Commutation of Filter and Erase Operations on Finite Sets
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the operation of first removing $a$ from $s$ and then filtering by a predicate $p$ is equal to first filtering $s$ by $p$ and then removing $a$ from the result. In symbols: \[ \text{filter } p (\text{erase } s a) = \text{erase } (\text{filter } p s) a. \]
Finset.filter_or theorem
(s : Finset α) : (s.filter fun a => p a ∨ q a) = s.filter p ∪ s.filter q
Full source 
theorem filter_or (s : Finset α) : (s.filter fun a => p a ∨ q a) = s.filter p ∪ s.filter q :=
  ext fun _ => by simp [mem_filter, mem_union, and_or_left]
Filter of Disjunction Equals Union of Filters
Informal description
For any finite set $s$ of type $\alpha$ and predicates $p, q : \alpha \to \text{Prop}$, the filter of $s$ by the disjunction $p \lor q$ is equal to the union of the filters of $s$ by $p$ and by $q$. That is, \[ \{a \in s \mid p(a) \lor q(a)\} = \{a \in s \mid p(a)\} \cup \{a \in s \mid q(a)\}. \]
Finset.filter_and theorem
(s : Finset α) : (s.filter fun a => p a ∧ q a) = s.filter p ∩ s.filter q
Full source 
theorem filter_and (s : Finset α) : (s.filter fun a => p a ∧ q a) = s.filter p ∩ s.filter q :=
  ext fun _ => by simp [mem_filter, mem_inter, and_comm, and_left_comm, and_self_iff, and_assoc]
Filter of Conjunction Equals Intersection of Filters
Informal description
For any finite set $s$ of type $\alpha$ and predicates $p, q : \alpha \to \text{Prop}$, the filter of $s$ by the conjunction $p \land q$ is equal to the intersection of the filters of $s$ by $p$ and by $q$. That is, \[ \{a \in s \mid p(a) \land q(a)\} = \{a \in s \mid p(a)\} \cap \{a \in s \mid q(a)\}. \]
Finset.filter_not theorem
(s : Finset α) : (s.filter fun a => ¬p a) = s \ s.filter p
Full source 
theorem filter_not (s : Finset α) : (s.filter fun a => ¬p a) = s \ s.filter p :=
  ext fun a => by
    simp only [Bool.decide_coe, Bool.not_eq_true', mem_filter, and_comm, mem_sdiff, not_and_or,
      Bool.not_eq_true, and_or_left, and_not_self, or_false]
Complementary Filter Equals Set Difference
Informal description
For any finite set $s$ of type $\alpha$ and a decidable predicate $p : \alpha \to \text{Prop}$, the filter of $s$ by the negation $\neg p$ is equal to the set difference $s \setminus \{a \in s \mid p(a)\}$. That is, \[ \{a \in s \mid \neg p(a)\} = s \setminus \{a \in s \mid p(a)\}. \]
Finset.filter_and_not theorem
(s : Finset α) (p q : α → Prop) [DecidablePred p] [DecidablePred q] : s.filter (fun a ↦ p a ∧ ¬q a) = s.filter p \ s.filter q
Full source 
lemma filter_and_not (s : Finset α) (p q : α → Prop) [DecidablePred p] [DecidablePred q] :
    s.filter (fun a ↦ p a ∧ ¬ q a) = s.filter p \ s.filter q := by
  rw [filter_and, filter_not, ← inter_sdiff_assoc, inter_eq_left.2 (filter_subset _ _)]
Filter of Conjunction with Negation Equals Set Difference of Filters
Informal description
For any finite set $s$ of type $\alpha$ and decidable predicates $p, q : \alpha \to \text{Prop}$, the filter of $s$ by the conjunction $p \land \neg q$ is equal to the set difference of the filters of $s$ by $p$ and by $q$. That is, \[ \{a \in s \mid p(a) \land \neg q(a)\} = \{a \in s \mid p(a)\} \setminus \{a \in s \mid q(a)\}. \]
Finset.sdiff_eq_filter theorem
(s₁ s₂ : Finset α) : s₁ \ s₂ = filter (· ∉ s₂) s₁
Full source 
theorem sdiff_eq_filter (s₁ s₂ : Finset α) : s₁ \ s₂ = filter (· ∉ s₂) s₁ :=
  ext fun _ => by simp [mem_sdiff, mem_filter]
Set Difference as Filter: $s_1 \setminus s_2 = \{x \in s_1 \mid x \notin s_2\}$
Informal description
For any two finite sets $s_1$ and $s_2$ of a type $\alpha$ with decidable equality, the set difference $s_1 \setminus s_2$ is equal to the subset of $s_1$ obtained by filtering out all elements that belong to $s_2$. In other words, $s_1 \setminus s_2 = \{x \in s_1 \mid x \notin s_2\}$.
Finset.subset_union_elim theorem
{s : Finset α} {t₁ t₂ : Set α} (h : ↑s ⊆ t₁ ∪ t₂) : ∃ s₁ s₂ : Finset α, s₁ ∪ s₂ = s ∧ ↑s₁ ⊆ t₁ ∧ ↑s₂ ⊆ t₂ \ t₁
Full source 
theorem subset_union_elim {s : Finset α} {t₁ t₂ : Set α} (h : ↑s ⊆ t₁ ∪ t₂) :
    ∃ s₁ s₂ : Finset α, s₁ ∪ s₂ = s ∧ ↑s₁ ⊆ t₁ ∧ ↑s₂ ⊆ t₂ \ t₁ := by
  classical
    refine ⟨s.filter (· ∈ t₁), s.filter (· ∉ t₁), ?_, ?_, ?_⟩
    · simp [filter_union_right, em]
    · intro x
      simp
    · intro x
      simp only [not_not, coe_filter, Set.mem_setOf_eq, Set.mem_diff, and_imp]
      intro hx hx₂
      exact ⟨Or.resolve_left (h hx) hx₂, hx₂⟩
Decomposition of Finite Set Contained in Union: $s \subseteq t_1 \cup t_2$ Implies Existence of Partition $s_1 \cup s_2 = s$ with $s_1 \subseteq t_1$ and $s_2 \subseteq t_2 \setminus t_1$
Informal description
For any finite set $s$ of type $\alpha$ and any two sets $t_1, t_2 \subseteq \alpha$, if the set corresponding to $s$ is contained in the union $t_1 \cup t_2$, then there exist finite subsets $s_1, s_2 \subseteq s$ such that: 1. $s_1 \cup s_2 = s$, 2. The set corresponding to $s_1$ is contained in $t_1$, and 3. The set corresponding to $s_2$ is contained in the set difference $t_2 \setminus t_1$.
Finset.filter_eq theorem
[DecidableEq β] (s : Finset β) (b : β) : s.filter (Eq b) = ite (b ∈ s) { b } ∅
Full source 
/-- After filtering out everything that does not equal a given value, at most that value remains.

  This is equivalent to `filter_eq'` with the equality the other way.
-/
theorem filter_eq [DecidableEq β] (s : Finset β) (b : β) :
    s.filter (Eq b) = ite (b ∈ s) {b} ∅ := by
  split_ifs with h
  · ext
    simp only [mem_filter, mem_singleton, decide_eq_true_eq]
    refine ⟨fun h => h.2.symm, ?_⟩
    rintro rfl
    exact ⟨h, rfl⟩
  · ext
    simp only [mem_filter, not_and, iff_false, not_mem_empty, decide_eq_true_eq]
    rintro m rfl
    exact h m
Filtering a Finite Set for Equality with a Given Element
Informal description
For a finite set $s$ of type $\beta$ with decidable equality and an element $b \in \beta$, the filter of $s$ containing only elements equal to $b$ is equal to $\{b\}$ if $b \in s$, and the empty set otherwise. In other words: \[ \text{filter } (a \mapsto a = b) \ s = \begin{cases} \{b\} & \text{if } b \in s \\ \emptyset & \text{otherwise} \end{cases} \]
Finset.filter_eq' theorem
[DecidableEq β] (s : Finset β) (b : β) : (s.filter fun a => a = b) = ite (b ∈ s) { b } ∅
Full source 
/-- After filtering out everything that does not equal a given value, at most that value remains.

  This is equivalent to `filter_eq` with the equality the other way.
-/
theorem filter_eq' [DecidableEq β] (s : Finset β) (b : β) :
    (s.filter fun a => a = b) = ite (b ∈ s) {b} ∅ :=
  _root_.trans (filter_congr fun _ _ => by simp_rw [@eq_comm _ b]) (filter_eq s b)
Filtered Set for Equality with a Given Element
Informal description
For a finite set $s$ of type $\beta$ with decidable equality and an element $b \in \beta$, the subset of $s$ consisting of elements equal to $b$ is equal to $\{b\}$ if $b \in s$, and the empty set otherwise. In other words: \[ \{a \in s \mid a = b\} = \begin{cases} \{b\} & \text{if } b \in s \\ \emptyset & \text{otherwise} \end{cases} \]
Finset.filter_ne theorem
[DecidableEq β] (s : Finset β) (b : β) : (s.filter fun a => b ≠ a) = s.erase b
Full source 
theorem filter_ne [DecidableEq β] (s : Finset β) (b : β) :
    (s.filter fun a => b ≠ a) = s.erase b := by
  ext
  simp only [mem_filter, mem_erase, Ne, decide_not, Bool.not_eq_true', decide_eq_false_iff_not]
  tauto
Filtering Inequality Equals Erasure in Finite Sets
Informal description
For any finite set $s$ of type $\beta$ with decidable equality and any element $b \in \beta$, the subset of $s$ consisting of elements not equal to $b$ is equal to the set obtained by erasing $b$ from $s$. In other words: \[ \{a \in s \mid b \neq a\} = s \setminus \{b\} \]
Finset.filter_ne' theorem
[DecidableEq β] (s : Finset β) (b : β) : (s.filter fun a => a ≠ b) = s.erase b
Full source 
theorem filter_ne' [DecidableEq β] (s : Finset β) (b : β) : (s.filter fun a => a ≠ b) = s.erase b :=
  _root_.trans (filter_congr fun _ _ => by simp_rw [@ne_comm _ b]) (filter_ne s b)
Equality of Filtered Inequality and Erasure in Finite Sets
Informal description
For any finite set $s$ of type $\beta$ with decidable equality and any element $b \in \beta$, the subset of $s$ consisting of elements not equal to $b$ is equal to the set obtained by erasing $b$ from $s$. In other words: \[ \{a \in s \mid a \neq b\} = s \setminus \{b\} \]
Finset.filter_union_filter_of_codisjoint theorem
(s : Finset α) (h : Codisjoint p q) : s.filter p ∪ s.filter q = s
Full source 
theorem filter_union_filter_of_codisjoint (s : Finset α) (h : Codisjoint p q) :
    s.filter p ∪ s.filter q = s :=
  (filter_or _ _ _).symm.trans <| filter_true_of_mem fun x _ => h.top_le x trivial
Union of Codisjoint Filters Equals Original Set
Informal description
For any finite set $s$ of type $\alpha$ and codisjoint predicates $p, q : \alpha \to \text{Prop}$, the union of the subsets of $s$ filtered by $p$ and by $q$ equals $s$ itself. That is, \[ \{a \in s \mid p(a)\} \cup \{a \in s \mid q(a)\} = s. \]
Finset.filter_union_filter_neg_eq theorem
[∀ x, Decidable (¬p x)] (s : Finset α) : (s.filter p ∪ s.filter fun a => ¬p a) = s
Full source 
theorem filter_union_filter_neg_eq [∀ x, Decidable (¬p x)] (s : Finset α) :
    (s.filter p ∪ s.filter fun a => ¬p a) = s :=
  filter_union_filter_of_codisjoint _ _ _ <| @codisjoint_hnot_right _ _ p
Union of Filtered Set and its Complement Equals Original Set
Informal description
For any finite set $s$ of type $\alpha$ and any decidable predicate $p : \alpha \to \text{Prop}$, the union of the subsets of $s$ filtered by $p$ and by $\neg p$ equals $s$ itself. That is, \[ \{a \in s \mid p(a)\} \cup \{a \in s \mid \neg p(a)\} = s. \]
Finset.range_filter_eq theorem
{n m : ℕ} : (range n).filter (· = m) = if m < n then { m } else ∅
Full source 
@[simp]
theorem range_filter_eq {n m : ℕ} : (range n).filter (· = m) = if m < n then {m} else ∅ := by
  convert filter_eq (range n) m using 2
  · ext
    rw [eq_comm]
  · simp
Filtering Range for Equality Yields Singleton or Empty Set
Informal description
For any natural numbers $n$ and $m$, the finite set obtained by filtering the range $\{0, \ldots, n-1\}$ for elements equal to $m$ is $\{m\}$ if $m < n$, and the empty set otherwise. In other words: \[ \text{filter } (x \mapsto x = m) \ (\text{range } n) = \begin{cases} \{m\} & \text{if } m < n \\ \emptyset & \text{otherwise} \end{cases} \]
Multiset.toFinset_add theorem
(s t : Multiset α) : toFinset (s + t) = toFinset s ∪ toFinset t
Full source 
@[simp]
theorem toFinset_add (s t : Multiset α) : toFinset (s + t) = toFinsettoFinset s ∪ toFinset t :=
  Finset.ext <| by simp
Finite Set of Multiset Sum Equals Union of Finite Sets
Informal description
For any two multisets $s$ and $t$ over a type $\alpha$, the finite set corresponding to their sum $s + t$ is equal to the union of the finite sets corresponding to $s$ and $t$, i.e., $\text{toFinset}(s + t) = \text{toFinset}(s) \cup \text{toFinset}(t)$.
Multiset.toFinset_inter theorem
(s t : Multiset α) : toFinset (s ∩ t) = toFinset s ∩ toFinset t
Full source 
@[simp]
theorem toFinset_inter (s t : Multiset α) : toFinset (s ∩ t) = toFinsettoFinset s ∩ toFinset t :=
  Finset.ext <| by simp
Finite Set of Multiset Intersection Equals Intersection of Finite Sets
Informal description
For any two multisets $s$ and $t$ over a type $\alpha$, the finite set corresponding to their intersection $s \cap t$ is equal to the intersection of the finite sets corresponding to $s$ and $t$, i.e., $\text{toFinset}(s \cap t) = \text{toFinset}(s) \cap \text{toFinset}(t)$.
Multiset.toFinset_union theorem
(s t : Multiset α) : (s ∪ t).toFinset = s.toFinset ∪ t.toFinset
Full source 
@[simp]
theorem toFinset_union (s t : Multiset α) : (s ∪ t).toFinset = s.toFinset ∪ t.toFinset := by
  ext; simp
Finite Set of Multiset Union Equals Union of Finite Sets
Informal description
For any two multisets $s$ and $t$ over a type $\alpha$, the finite set corresponding to their union $s \cup t$ is equal to the union of the finite sets corresponding to $s$ and $t$, i.e., $(s \cup t).\text{toFinset} = s.\text{toFinset} \cup t.\text{toFinset}$.
Multiset.toFinset_eq_empty theorem
{m : Multiset α} : m.toFinset = ∅ ↔ m = 0
Full source 
@[simp]
theorem toFinset_eq_empty {m : Multiset α} : m.toFinset = ∅ ↔ m = 0 :=
  Finset.val_inj.symm.trans Multiset.dedup_eq_zero
Empty Multiset to Empty Finset Conversion
Informal description
For any multiset $m$ of type $\alpha$, the finite set obtained by converting $m$ is empty if and only if $m$ is the empty multiset, i.e., $\mathrm{toFinset}(m) = \emptyset \leftrightarrow m = 0$.
Multiset.toFinset_nonempty theorem
: s.toFinset.Nonempty ↔ s ≠ 0
Full source 
@[simp]
theorem toFinset_nonempty : s.toFinset.Nonempty ↔ s ≠ 0 := by
  simp only [toFinset_eq_empty, Ne, Finset.nonempty_iff_ne_empty]
Nonempty Finset from Multiset iff Multiset is Nonzero
Informal description
For any multiset $s$ of type $\alpha$, the finite set obtained from $s$ is nonempty if and only if $s$ is not the empty multiset. In other words, $s.\text{toFinset}$ is nonempty $\leftrightarrow s \neq 0$.
Multiset.toFinset_filter theorem
(s : Multiset α) (p : α → Prop) [DecidablePred p] : Multiset.toFinset (s.filter p) = s.toFinset.filter p
Full source 
@[simp]
theorem toFinset_filter (s : Multiset α) (p : α → Prop) [DecidablePred p] :
    Multiset.toFinset (s.filter p) = s.toFinset.filter p := by
  ext; simp
Commutativity of Filtering and Finite Set Conversion for Multisets
Informal description
For any multiset $s$ of elements of type $\alpha$ and any decidable predicate $p$ on $\alpha$, the finite set obtained by first filtering $s$ with $p$ and then converting to a finite set is equal to the finite set obtained by first converting $s$ to a finite set and then filtering with $p$. In other words: \[ \text{toFinset}(s \text{.filter } p) = \text{toFinset}(s) \text{.filter } p \]
List.toFinset_union theorem
(l l' : List α) : (l ∪ l').toFinset = l.toFinset ∪ l'.toFinset
Full source 
@[simp]
theorem toFinset_union (l l' : List α) : (l ∪ l').toFinset = l.toFinset ∪ l'.toFinset := by
  ext
  simp
Finite Set Conversion Preserves List Union
Informal description
For any two lists $l$ and $l'$ of elements of type $\alpha$, the finite set obtained from the union of $l$ and $l'$ is equal to the union of the finite sets obtained from $l$ and $l'$ individually. That is, $(l \cup l').\text{toFinset} = l.\text{toFinset} \cup l'.\text{toFinset}$.
List.toFinset_inter theorem
(l l' : List α) : (l ∩ l').toFinset = l.toFinset ∩ l'.toFinset
Full source 
@[simp]
theorem toFinset_inter (l l' : List α) : (l ∩ l').toFinset = l.toFinset ∩ l'.toFinset := by
  ext
  simp
Intersection of Lists Preserved Under Conversion to Finite Sets
Informal description
For any two lists $l$ and $l'$ of elements of type $\alpha$, the finite set obtained from their intersection $l \cap l'$ is equal to the intersection of the finite sets obtained from $l$ and $l'$ individually. That is, $(l \cap l').\text{toFinset} = l.\text{toFinset} \cap l'.\text{toFinset}$.
List.toFinset_filter theorem
(s : List α) (p : α → Bool) : (s.filter p).toFinset = s.toFinset.filter (p ·)
Full source 
@[simp]
theorem toFinset_filter (s : List α) (p : α → Bool) :
    (s.filter p).toFinset = s.toFinset.filter (p ·) := by
  ext; simp [List.mem_filter]
Commutativity of List Filtering and Finite Set Conversion: $(s \text{.filter } p)\text{.toFinset} = s\text{.toFinset}\text{.filter } p$
Informal description
For any list $s$ of elements of type $\alpha$ and any boolean predicate $p$ on $\alpha$, the finite set obtained by first filtering $s$ with $p$ and then converting to a finite set is equal to the finite set obtained by first converting $s$ to a finite set and then filtering with $p$. In symbols: $$(s \text{.filter } p)\text{.toFinset} = s\text{.toFinset}\text{.filter } p$$
Finset.toList_eq_nil theorem
{s : Finset α} : s.toList = [] ↔ s = ∅
Full source 
@[simp]
theorem toList_eq_nil {s : Finset α} : s.toList = [] ↔ s = ∅ :=
  Multiset.toList_eq_nil.trans val_eq_zero
Empty List Characterization of Finite Sets
Informal description
For any finite set $s$ of type $\alpha$, the list representation of $s$ is empty if and only if $s$ is the empty set, i.e., $\text{toList}(s) = [] \leftrightarrow s = \emptyset$.
Finset.empty_toList theorem
{s : Finset α} : s.toList.isEmpty ↔ s = ∅
Full source 
theorem empty_toList {s : Finset α} : s.toList.isEmpty ↔ s = ∅ := by simp
Empty List Representation of Finite Set Equals Empty Set
Informal description
For any finite set $s$ of type $\alpha$, the list representation of $s$ is empty if and only if $s$ is the empty set, i.e., $\text{toList}(s) = [] \leftrightarrow s = \emptyset$.
Finset.toList_empty theorem
: (∅ : Finset α).toList = []
Full source 
@[simp]
theorem toList_empty : (∅ : Finset α).toList = [] :=
  toList_eq_nil.mpr rfl
Empty Finite Set Yields Empty List
Informal description
The list representation of the empty finite set is the empty list, i.e., $\text{toList}(\emptyset) = []$.
Finset.Nonempty.toList_ne_nil theorem
{s : Finset α} (hs : s.Nonempty) : s.toList ≠ []
Full source 
theorem Nonempty.toList_ne_nil {s : Finset α} (hs : s.Nonempty) : s.toList ≠ [] :=
  mt toList_eq_nil.mp hs.ne_empty
Nonempty Finite Sets Have Nonempty List Representation
Informal description
For any nonempty finite set $s$ of type $\alpha$, the list representation of $s$ is not the empty list, i.e., $\text{toList}(s) \neq []$.
Finset.Nonempty.not_empty_toList theorem
{s : Finset α} (hs : s.Nonempty) : ¬s.toList.isEmpty
Full source 
theorem Nonempty.not_empty_toList {s : Finset α} (hs : s.Nonempty) : ¬s.toList.isEmpty :=
  mt empty_toList.mp hs.ne_empty
Nonempty Finite Sets Have Nonempty List Representation
Informal description
For any nonempty finite set $s$ of type $\alpha$, the list representation of $s$ is not empty, i.e., $\text{toList}(s) \neq []$.
Finset.chooseX definition
(hp : ∃! a, a ∈ l ∧ p a) : { a // a ∈ l ∧ p a }
Full source 
/-- Given a finset `l` and a predicate `p`, associate to a proof that there is a unique element of
`l` satisfying `p` this unique element, as an element of the corresponding subtype. -/
def chooseX (hp : ∃! a, a ∈ l ∧ p a) : { a // a ∈ l ∧ p a } :=
  Multiset.chooseX p l.val hp
Unique element selection in a finite set with proof
Informal description
Given a finite set $l$ and a predicate $p$, if there exists a unique element $a \in l$ satisfying $p(a)$, then `Finset.chooseX p l hp` returns this element $a$ together with proofs that $a \in l$ and $p(a)$. Here, $hp$ is a proof of the existence and uniqueness of such an element $a$.
Finset.choose definition
(hp : ∃! a, a ∈ l ∧ p a) : α
Full source 
/-- Given a finset `l` and a predicate `p`, associate to a proof that there is a unique element of
`l` satisfying `p` this unique element, as an element of the ambient type. -/
def choose (hp : ∃! a, a ∈ l ∧ p a) : α :=
  chooseX p l hp
Unique element selection in a finite set
Informal description
Given a finite set $l$ and a predicate $p$, if there exists a unique element $a \in l$ satisfying $p(a)$, then $\text{Finset.choose} \, p \, l \, hp$ returns this unique element $a$ (as an element of the ambient type). Here, $hp$ is a proof of the existence and uniqueness of such an element $a$.
Finset.choose_spec theorem
(hp : ∃! a, a ∈ l ∧ p a) : choose p l hp ∈ l ∧ p (choose p l hp)
Full source 
theorem choose_spec (hp : ∃! a, a ∈ l ∧ p a) : choosechoose p l hp ∈ lchoose p l hp ∈ l ∧ p (choose p l hp) :=
  (chooseX p l hp).property
Specification of the Unique Element Chosen from a Finite Set
Informal description
Given a finite set $l$ and a predicate $p$, if there exists a unique element $a \in l$ satisfying $p(a)$, then the element $\text{choose}(p, l, hp)$ belongs to $l$ and satisfies $p(\text{choose}(p, l, hp))$.
Finset.choose_mem theorem
(hp : ∃! a, a ∈ l ∧ p a) : choose p l hp ∈ l
Full source 
theorem choose_mem (hp : ∃! a, a ∈ l ∧ p a) : choosechoose p l hp ∈ l :=
  (choose_spec _ _ _).1
Membership of the chosen element in a finite set
Informal description
Given a finite set $l$ and a predicate $p$, if there exists a unique element $a \in l$ satisfying $p(a)$, then the element $\text{choose}(p, l, hp)$ belongs to $l$.
Finset.choose_property theorem
(hp : ∃! a, a ∈ l ∧ p a) : p (choose p l hp)
Full source 
theorem choose_property (hp : ∃! a, a ∈ l ∧ p a) : p (choose p l hp) :=
  (choose_spec _ _ _).2
Property of the Unique Element Chosen from a Finite Set
Informal description
Given a finite set $l$ and a predicate $p$, if there exists a unique element $a \in l$ satisfying $p(a)$, then the element $\text{choose}(p, l, hp)$ satisfies $p(\text{choose}(p, l, hp))$.
Equiv.Finset.union definition
(s t : Finset α) (h : Disjoint s t) : s ⊕ t ≃ (s ∪ t : Finset α)
Full source 
/-- The disjoint union of finsets is a sum -/
def Finset.union (s t : Finset α) (h : Disjoint s t) :
    s ⊕ ts ⊕ t ≃ (s ∪ t : Finset α) :=
  Equiv.setCongr (coe_union _ _) |>.trans (Equiv.Set.union (disjoint_coe.mpr h)) |>.symm
Equivalence between disjoint union and union of finite sets
Informal description
Given two disjoint finite sets $s$ and $t$ of type $\alpha$, there is an equivalence (bijection) between their disjoint union $s \oplus t$ and their union $s \cup t$ as finite sets. This equivalence is constructed by first converting the finite sets to ordinary sets, using the equivalence between the union of disjoint sets and their sum, and then taking the inverse of this equivalence.
Equiv.Finset.union_symm_inl theorem
(h : Disjoint s t) (x : s) : Equiv.Finset.union s t h (Sum.inl x) = ⟨x, Finset.mem_union.mpr <| Or.inl x.2⟩
Full source 
@[simp]
theorem Finset.union_symm_inl (h : Disjoint s t) (x : s) :
    Equiv.Finset.union s t h (Sum.inl x) = ⟨x, Finset.mem_union.mpr <| Or.inl x.2⟩ :=
  rfl
Behavior of Union Equivalence on Left Injection for Disjoint Finite Sets
Informal description
Let $s$ and $t$ be two disjoint finite sets of type $\alpha$, and let $h$ be a proof of their disjointness. For any element $x \in s$, the equivalence $\text{Equiv.Finset.union}\ s\ t\ h$ maps the left injection of $x$ (denoted $\text{Sum.inl}\ x$) to the pair $\langle x, \text{Or.inl}\ x.2\rangle$, where $x.2$ is a proof that $x \in s$ and $\text{Or.inl}\ x.2$ is a proof that $x \in s \cup t$ via the left disjunct.
Equiv.Finset.union_symm_inr theorem
(h : Disjoint s t) (y : t) : Equiv.Finset.union s t h (Sum.inr y) = ⟨y, Finset.mem_union.mpr <| Or.inr y.2⟩
Full source 
@[simp]
theorem Finset.union_symm_inr (h : Disjoint s t) (y : t) :
    Equiv.Finset.union s t h (Sum.inr y) = ⟨y, Finset.mem_union.mpr <| Or.inr y.2⟩ :=
  rfl
Right Inclusion in Disjoint Union Equivalence for Finite Sets
Informal description
For any two disjoint finite sets $s$ and $t$ of type $\alpha$, and any element $y \in t$, the equivalence `Equiv.Finset.union` maps the right inclusion $\text{Sum.inr}(y)$ to the pair $\langle y, \text{Or.inr}(y.2) \rangle$, where $y.2$ is the proof that $y \in t$ and $\text{Or.inr}(y.2)$ is the proof that $y \in s \cup t$ via right membership.
Equiv.piFinsetUnion definition
{ι} [DecidableEq ι] (α : ι → Type*) {s t : Finset ι} (h : Disjoint s t) : ((∀ i : s, α i) × ∀ i : t, α i) ≃ ∀ i : (s ∪ t : Finset ι), α i
Full source 
/-- The type of dependent functions on the disjoint union of finsets `s ∪ t` is equivalent to the
  type of pairs of functions on `s` and on `t`. This is similar to `Equiv.sumPiEquivProdPi`. -/
def piFinsetUnion {ι} [DecidableEq ι] (α : ι → Type*) {s t : Finset ι} (h : Disjoint s t) :
    ((∀ i : s, α i) × ∀ i : t, α i) ≃ ∀ i : (s ∪ t : Finset ι), α i :=
  let e := Equiv.Finset.union s t h
  sumPiEquivProdPi (fun b ↦ α (e b)) |>.symm.trans (.piCongrLeft (fun i : ↥(s ∪ t) ↦ α i) e)
Equivalence between product of dependent functions on disjoint finite sets and dependent functions on their union
Informal description
Given a type $\iota$ with decidable equality and a family of types $\alpha : \iota \to \text{Type*}$, for any two disjoint finite sets $s, t \subseteq \iota$, there is an equivalence between the product of dependent function spaces $(\prod_{i \in s} \alpha i) \times (\prod_{i \in t} \alpha i)$ and the dependent function space over their union $\prod_{i \in s \cup t} \alpha i$. This equivalence is constructed by: 1. First establishing a bijection between the disjoint union $s \oplus t$ and $s \cup t$ (via `Equiv.Finset.union`) 2. Then using `sumPiEquivProdPi` to transform dependent functions on the sum type to a product of dependent functions 3. Finally applying `piCongrLeft` to transport these functions back to the original index set
Finset.equivToSet definition
(s : Finset α) : s ≃ s.toSet
Full source 
/-- A finset is equivalent to its coercion as a set. -/
def _root_.Finset.equivToSet (s : Finset α) : s ≃ s.toSet where
  toFun a := ⟨a.1, mem_coe.2 a.2⟩
  invFun a := ⟨a.1, mem_coe.1 a.2⟩
  left_inv := fun _ ↦ rfl
  right_inv := fun _ ↦ rfl
Bijection between a finite set and its corresponding set
Informal description
For any finite set $s$ of type $\alpha$, there is a bijection between the elements of $s$ (as a `Finset`) and the elements of the corresponding set $\{a \mid a \in s\}$. The bijection is given by: - The forward map sends an element $a \in s$ to the same element viewed in the set $\{a \mid a \in s\}$. - The inverse map sends an element $a$ from the set $\{a \mid a \in s\}$ back to the same element viewed in the original finite set $s$. Both maps are identity-preserving, meaning they satisfy $f(g(x)) = x$ and $g(f(x)) = x$ for all $x$ in their respective domains.
Multiset.toFinset_replicate theorem
(n : ℕ) (a : α) : (replicate n a).toFinset = if n = 0 then ∅ else { a }
Full source 
@[simp]
lemma toFinset_replicate (n : ℕ) (a : α) :
    (replicate n a).toFinset = if n = 0 then ∅ else {a} := by
  ext x
  simp only [mem_toFinset, Finset.mem_singleton, mem_replicate]
  split_ifs with hn <;> simp [hn]
Finite Set of Replicated Elements: $\text{replicate } n a \to \text{Finset}$
Informal description
For any natural number $n$ and any element $a$ of type $\alpha$, the finite set obtained from the multiset consisting of $n$ copies of $a$ is equal to the empty set if $n = 0$, and to the singleton set $\{a\}$ otherwise. In other words, $$(\text{replicate } n a).\text{toFinset} = \begin{cases} \emptyset & \text{if } n = 0, \\ \{a\} & \text{if } n \neq 0. \end{cases}$$