theorem bijection_of_eq_card {α β : Type} [DecidableEq α] [DecidableEq β] {s : Finset α} {t : Finset β} : s.card = t.card → s = ∅ ∧ t = ∅ ∨ ∃ (f : { x : α // x ∈ s } → { x : β // x ∈ t }), Function.Bijective f

theorem bijection_of_List_perm {α : Type} {l₁ l₂ : List α} : l₁.Perm l₂ → ∃ (f : Fin l₁.length → Fin l₂.length), Function.Bijective f ∧ ∀ (i : Fin l₁.length), l₁.get i = l₂.get (f i)

theorem xor_even_le_implies_lt {m n : ℕ} : Xor' (Even m) (Even n) → m ≤ n → m < n

theorem dblcnt (M' N' : ℕ) (f : Sym2 (Fin (M' + N').succ) → Fin 2) (c : Fin 2) : 2 * {e ∈ ⊤.edgeFinset | f e = c}.card = {x : ⊤.Dart | f (Sym2.mk x.toProd) = c}.card

theorem Rat.mkRat_one_num (z : ℤ) : (mkRat z 1).num = z

theorem Rat.mkRat_one_den (z : ℤ) : (mkRat z 1).den = 1

theorem Rat.mkRat_num_one (n : ℕ) : (mkRat 1 n.succ).num = 1

theorem Rat.mkRat_den_one (n : ℕ) : (mkRat 1 n.succ).den = n.succ

structure Finset.FinpartitionWithEmpty {α : Type} [DecidableEq α] (a : Finset α) : Type

A finite partition of a : Finset α is a pairwise disjoint finite set of elements whose supremum is a.

• parts : Finset (Finset α)

  The elements of the finite partition of a

• pwDisj : (↑self.parts).PairwiseDisjoint id

  The parts are pairwise disjoint

• supParts : self.parts.sup id = a

  The supremum of the partition is a

theorem Finset.FinpartitionWithEmpty.ext_iff {α : Type} {inst✝ : DecidableEq α} {a : Finset α} {x y : a.FinpartitionWithEmpty} : x = y ↔ x.parts = y.parts

theorem Finset.FinpartitionWithEmpty.ext {α : Type} {inst✝ : DecidableEq α} {a : Finset α} {x y : a.FinpartitionWithEmpty} (parts : x.parts = y.parts) : x = y

theorem Finset.FinpartitionWithEmpty.biUnion_parts {α : Type} [DecidableEq α] {a : Finset α} {P : a.FinpartitionWithEmpty} : P.parts.biUnion id = a

theorem Finset.FinpartitionWithEmpty.sum_card_parts_with_empty {α : Type} [DecidableEq α] {a : Finset α} (P : a.FinpartitionWithEmpty) : ∑ i ∈ P.parts, i.card = a.card

theorem Finset.sum_image_vanishing {β : Type u} {α : Type v} {γ : Type w} {f : α → β} [AddCommMonoid β] [DecidableEq α] [DecidableEq γ] {s : Finset γ} {g : γ → α} : (∀ x ∈ s, ∀ y ∈ s, g x = g y → f (g x) ≠ 0 → x = y) → ∑ x ∈ image g s, f x = s.sum (f ∘ g)

theorem Fin.univ_disjUnion_zero_succ (n : ℕ) : Finset.univ = {0}.disjUnion (Finset.map (succEmb n) Finset.univ) ⋯

theorem vector_list_finset_sum {α β : Type} [AddCommMonoid β] {n : ℕ} (V : List.Vector α n) (f : α → β) : Finset.univ.sum (f ∘ V.get) = (List.map f V.toList).sum

theorem Nat.find_upward_closed_eq_succ_iff {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) (hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → p k₁ → p k₂) (k : ℕ) : Nat.find h = k + 1 ↔ p (k + 1) ∧ ¬p k