@[simp]

theorem le_trans_simp {α : Type u_1} [ha : LinearOrder α] {a b c : α} : a ≤ b → b ≤ c → a ≤ c ↔ True

@[simp]

theorem le_trans_simp' {α : Type u_1} [ha : LinearOrder α] {a b c : α} : b ≤ c → a ≤ b → a ≤ c ↔ True

@[simp]

theorem le_total_simp {α : Type u_1} [ha : LinearOrder α] {a b : α} : a ≤ b ∨ b ≤ a ↔ True

@[simp]

theorem le_antisymm_simp {α : Type u_1} [ha : LinearOrder α] {a b : α} : a ≤ b → b ≤ a → a = b ↔ True

@[simp]

theorem lt_trans_simp {α : Type u_1} [ha : LinearOrder α] {a b c : α} : a < b → b < c → a < c ↔ True

@[simp]

theorem lt_trans_simp' {α : Type u_1} [ha : LinearOrder α] {a b c : α} : b < c → a < b → a < c ↔ True

theorem Fintype.exi_iter_cycle {α : Type u_1} [ha : Fintype α] {f : α → α} {x : α} : ∃ (n : ℕ) (m : ℕ), n < m ∧ f^[n] x = f^[m] x

@[simp]

theorem Fintype.complete' {α : Type u_1} [ha : Fintype α] {x : α} : x ∈ elems

@[instance_reducible]

instance Fintype.instOfIsEmpty_projects {α : Type u_2} [h : IsEmpty α] : Fintype α

Equations

• Fintype.instOfIsEmpty_projects = { elems := ∅, complete := ⋯ }

@[instance_reducible]

noncomputable instance Fintype.instElemRange_projects {α : Type u_1} [ha : Fintype α] {β : Type u_2} {f : α → β} : Fintype ↑(Set.range f)

Equations

• Fintype.instElemRange_projects = Fintype.ofFinite ↑(Set.range f)

@[simp]

theorem Fintype.elems_eq_empty_iff {α : Type u_1} [ha : Fintype α] : elems = ∅ ↔ ∀ (x : α), False

@[instance_reducible]

noncomputable instance Fintype.instElem_projects {α : Type u_1} [ha : Fintype α] {s : Set α} : Fintype ↑s

Equations

• Fintype.instElem_projects = Fintype.ofFinite ↑s

def Finset.fold' {α : Type u_1} {β : Type u_2} (s : Finset α) (f : β → α → β) (z : β) (h : ∀ {acc : β} {x y : α}, f (f acc x) y = f (f acc y) x) : β

Equations

• s.fold' f z h = Multiset.foldl f z s.val

theorem Finset.sum_eq_sum_of_fn_congr {α : Type u_4} {S : Finset α} {f g : α → ℕ} (h : ∀ i ∈ S, f i = g i) : ∑ x ∈ S, f x = ∑ x ∈ S, g x

@[simp]

theorem Finset.sum_fn_set_eq {S : Finset ℕ} {f : ℕ → ℕ} {a b : ℕ} (ha : a ∈ S) : ∑ x ∈ S, fn_set a b f x = ∑ x ∈ S, f x + b - f a

@[simp]

theorem Finset.sum_fn_swap_eq {S : Finset ℕ} {f : ℕ → ℕ} {a b : ℕ} (ha : a ∈ S) (hb : b ∈ S) : ∑ x ∈ S, fn_swap a b f x = ∑ x ∈ S, f x

def Finset.toSortedList {α : Type u_4} [h : LinearOrder α] (s : Finset α) : List α

Equations

• s.toSortedList = Quot.liftOn s.val (fun (xs : List α) => xs.mergeSort fun (a b : α) => decide (a ≤ b)) ⋯

noncomputable def Finset.mkRaw {α : Type u_4} {β : Type u_5} (f : α → β) : Finset β

Equations

• Finset.mkRaw f = if h : Infinite α then ∅ else have h := Fintype.ofFinite α; (List.map f Fintype.elems.toList).toFinset

@[simp]

theorem Finset.toSortedList_toFinset {α : Type u_4} [h : LinearOrder α] {s : Finset α} : s.toSortedList.toFinset = s

def Finset.mkRaw_comp {α : Type u_4} {β : Type u_5} [Fintype α] [LinearOrder α] [DecidableEq β] (f : α → β) : Finset β

Equations

• Finset.mkRaw_comp f = (List.map f Fintype.elems.toSortedList).toFinset

@[simp]

theorem Finset.mem_toList_iff {α : Type u_4} {s : Finset α} {x : α} : x ∈ s.toList ↔ x ∈ s

@[simp]

theorem Finset.mem_toSortedList_iff {α : Type u_4} [LinearOrder α] {s : Finset α} {x : α} : x ∈ s.toSortedList ↔ x ∈ s

theorem Finset.mkRaw_eq {α : Type u_4} {β : Type u_5} [ha : Fintype α] [DecidableEq α] [DecidableEq β] {f : α → β} : mkRaw f = (List.map f Fintype.elems.toList).toFinset

@[simp]

theorem Finset.mem_mkRaw_iff {α : Type u_4} {β : Type u_5} [Fintype α] {f : α → β} {b : β} : b ∈ mkRaw f ↔ ∃ (a : α), f a = b

@[simp]

theorem Finset.mem_mkRaw_comp_iff {α : Type u_4} {β : Type u_5} [Fintype α] [LinearOrder α] [DecidableEq β] {f : α → β} {b : β} : b ∈ mkRaw_comp f ↔ ∃ (a : α), f a = b

@[simp]

theorem Finset.mkRaw_comp_eq_mkRaw {α : Type u_4} {β : Type u_5} [Fintype α] [LinearOrder α] [DecidableEq β] {f : α → β} : mkRaw_comp f = mkRaw f

@[simp]

theorem Finset.mkRaw_const_of_nonempty {α : Type u_4} {β : Type u_5} [Fintype α] [Nonempty α] [DecidableEq α] [DecidableEq β] {b : β} : (mkRaw fun (x : α) => b) = {b}

@[simp]

theorem Finset.mkRaw_const_of_empty {α : Type u_4} {β : Type u_5} [IsEmpty α] [DecidableEq β] {b : β} : (mkRaw fun (x : α) => b) = ∅

theorem Finset.mkRaw_fin_succ_eq_insert {α : Type u_4} [ha : DecidableEq α] {n : ℕ} {f : Fin (n + 1) → α} : mkRaw f = insert (f ⟨n, ⋯⟩) (mkRaw fun (x : Fin n) => match x with | ⟨k, hk⟩ => f ⟨k, ⋯⟩)

theorem Finset.mkRaw_card_le {α : Type u_4} {β : Type u_5} [ha₁ : Fintype α] {f : α → β} : (mkRaw f).card ≤ Fintype.card α

theorem Finset.mkRaw_toSet_eq {α : Type u_4} {β : Type u_5} [ha : Fintype α] {f : α → β} : ↑(mkRaw f) = Set.range f

theorem Finset.card_eq_cardinal_mk_to_nat {α : Type u_4} {s : Finset α} : s.card = Cardinal.toNat (Cardinal.mk ↥s)

theorem Finset.card_eq_toSet_ncard {α : Type u_4} {s : Finset α} : s.card = (↑s).ncard

theorem Finset.image_toSet_eq {α : Type u_4} {β : Type u_5} [DecidableEq β] {s : Finset α} {f : α → β} : f '' ↑s = ↑(image f s)

theorem Finset.ncard_toSet {α : Type u_4} {s : Finset α} : (↑s).ncard = s.card

theorem Finset.sum_eq_add_sum_erase_of_mem {α : Type u_4} [ha : DecidableEq α] {s : Finset α} {x : α} {f : α → ℕ} (h : x ∈ s) : ∑ i ∈ s, f i = f x + ∑ i ∈ s.erase x, f i

theorem Finset.eq_of_sum_eq_sum_and_forall_le {α : Type u_4} {s : Finset α} {f g : α → ℕ} (h₁ : ∑ i ∈ s, f i = ∑ i ∈ s, g i) (h₂ : ∀ i ∈ s, f i ≤ g i) {i : α} (h₃ : i ∈ s) : f i = g i

theorem Multiset.card_eq_sum_count_of_subset {α : Type u_1} [ha : DecidableEq α] {m₁ m₂ : Multiset α} (h₁ : m₁ ⊆ m₂) : m₁.card = ∑ i ∈ m₁.toFinset ∪ m₂.toFinset, count i m₁

@[simp]

theorem Multiset.subset_add_left' {α : Type u_1} {m₁ m₂ : Multiset α} : m₁ ⊆ m₁ + m₂

@[simp]

theorem Multiset.subset_add_right' {α : Type u_1} {m₁ m₂ : Multiset α} : m₁ ⊆ m₂ + m₁

theorem Multiset.eq_of_le_and_card_eq {α : Type u_1} {m₁ m₂ : Multiset α} (h₁ : m₁ ≤ m₂) (h₂ : m₁.card = m₂.card) : m₁ = m₂

theorem Multiset.eq_of_le_and_le {α : Type u_1} {m₁ m₂ : Multiset α} (h₁ : m₁ ≤ m₂) (h₂ : m₂ ≤ m₁) : m₁ = m₂

theorem Multiset.eq_of_nodup_and_subset_and_subset {α : Type u_1} {m₁ m₂ : Multiset α} (h₁ : m₁.Nodup) (h₂ : m₂.Nodup) (h₃ : m₁ ⊆ m₂) (h₄ : m₂ ⊆ m₁) : m₁ = m₂

@[simp]

theorem Multiset.card_filter_eq_eq_count {α : Type u_1} [ha : DecidableEq α] {m : Multiset α} {x : α} : (filter (fun (x_1 : α) => x = x_1) m).card = count x m

theorem Multiset.map_eq_map_iff_loc {α : Type u_1} {β : Type u_2} {m₁ m₂ : Multiset α} {f : α → β} (hf : ∀ (x y : α), x ∈ m₁ ∨ x ∈ m₂ → y ∈ m₁ ∨ y ∈ m₂ → f x = f y → x = y) : map f m₁ = map f m₂ ↔ m₁ = m₂

@[simp]

theorem Multiset.toList_ofList_perm {α : Type u_1} {xs : List α} : (↑xs).toList.Perm xs

@[simp]

theorem Multiset.nodup_out_iff {α : Type u_1} {m : Multiset α} : (Quotient.out m).Nodup ↔ m.Nodup

theorem List.subperm_of_subperm_and_length_eq {α : Type u_1} {xs ys : List α} (h₁ : xs.Subperm ys) (h₂ : xs.length = ys.length) : ys.Subperm xs

theorem List.perm_of_nodup_and_subset_and_length_eq {α : Type u_1} {xs ys : List α} (hx : xs.Nodup) (h₁ : xs ⊆ ys) (h₂ : xs.length = ys.length) : ys.Perm xs

theorem List.subset_of_nodup_and_subset_and_length_eq {α : Type u_1} {xs ys : List α} (h₁ : xs.Nodup) (h₂ : xs ⊆ ys) (h₃ : xs.length = ys.length) : ys ⊆ xs

theorem List.mem_iff_count_ne_zero {α : Type u_1} {xs : List α} [ha : DecidableEq α] {x : α} : x ∈ xs ↔ count x xs ≠ 0

theorem List.perm_of_subset_and_nodup {α : Type u_1} {xs ys : List α} (h₁ : xs.Nodup) (h₂ : ys.Nodup) (h₃ : xs ⊆ ys) (h₄ : ys ⊆ xs) : xs.Perm ys

theorem List.length_eq_of_subset_and_nodup {α : Type u_1} {xs ys : List α} (h₁ : xs.Nodup) (h₂ : ys.Nodup) (h₃ : xs ⊆ ys) (h₄ : ys ⊆ xs) : xs.length = ys.length

theorem List.map_perm_map_iff_loc {α : Type u_1} {β : Type u_2} {xs ys : List α} {f : α → β} (hf : ∀ (x y : α), x ∈ xs ∨ x ∈ ys → y ∈ xs ∨ y ∈ ys → f x = f y → x = y) : (map f xs).Perm (map f ys) ↔ xs.Perm ys

theorem List.nodup_of_nodup_and_subperm {α : Type u_1} {xs ys : List α} (h₁ : ys.Nodup) (h₂ : xs.Subperm ys) : xs.Nodup

theorem List.nodup_filterMap_iff {α : Type u_1} {β : Type u_2} {xs : List α} [ha : DecidableEq α] {f : α → Option β} : (filterMap f xs).Nodup ↔ ∀ x ∈ xs, ∀ (y : β), f x = some y → count x xs ≤ 1 ∧ ∀ x' ∈ xs, f x' = some y → x = x'

theorem List.filterMap_perm_filterMap_iff_filter_map_perm {α : Type u_1} {β : Type u_2} {xs ys : List α} {f : α → Option β} : (filterMap f xs).Perm (filterMap f ys) ↔ (filter Option.isSome (map f xs)).Perm (filter Option.isSome (map f ys))

theorem List.count_filter_pos {α : Type u_1} {xs : List α} [ha : DecidableEq α] {f : α → Bool} {x : α} (h : f x = true) : count x (filter f xs) = count x xs

theorem List.count_filter_neg {α : Type u_1} {xs : List α} [ha : DecidableEq α] {f : α → Bool} {x : α} (h : f x = false) : count x (filter f xs) = 0

theorem List.count_filter_neg' {α : Type u_1} {xs : List α} [ha : DecidableEq α] {f : α → Bool} {x : α} (h : ¬f x = true) : count x (filter f xs) = 0

theorem List.count_filter_eq_ite {α : Type u_1} {xs : List α} [ha : DecidableEq α] {f : α → Bool} {x : α} : count x (filter f xs) = if f x = true then count x xs else 0

theorem List.filter_perm_of_perm {α : Type u_1} {xs ys : List α} {f : α → Bool} (h : xs.Perm ys) : (filter f xs).Perm (filter f ys)

theorem List.count_map_of_loc {α : Type u_1} {β : Type u_2} {xs : List α} [ha : DecidableEq α] [hb : DecidableEq β] {f : α → β} {x : α} (h : ∀ y ∈ xs, f x = f y → x = y) : count (f x) (map f xs) = count x xs

theorem List.count_map_eq_sum {α : Type u_1} {β : Type u_2} {xs : List α} [ha : DecidableEq α] [hb : DecidableEq β] {f : α → β} {y : β} : count y (map f xs) = ∑ x ∈ xs.toFinset, if f x = y then count x xs else 0

@[simp]

theorem List.cons_erase_perm_iff_mem {α : Type u_1} {xs : List α} [ha : DecidableEq α] {x : α} : (x :: xs.erase x).Perm xs ↔ x ∈ xs

@[simp]

theorem List.perm_cons_erase_iff_mem {α : Type u_1} {xs : List α} [ha : DecidableEq α] {x : α} : xs.Perm (x :: xs.erase x) ↔ x ∈ xs

theorem List.le_max? {α : Type u_1} {xs : List α} [ha : LinearOrder α] {x m : α} (h₁ : x ∈ xs) (h₂ : xs.max? = some m) : x ≤ m

theorem List.nodup_erase {α : Type u_1} {xs : List α} [ha : DecidableEq α] {x : α} (h : xs.Nodup) : (xs.erase x).Nodup

theorem List.pairwise_erase {α : Type u_1} {xs : List α} [ha : DecidableEq α] {r : α → α → Prop} {x : α} (h : Pairwise r xs) : Pairwise r (xs.erase x)

theorem List.Perm.mapWith {α : Type u_1} {β : Type u_2} {xs ys : List α} {f : (x : α) → x ∈ xs → β} (h : xs.Perm ys) : (xs.mapWith f).Perm (ys.mapWith fun (x : α) (h₁ : x ∈ ys) => f x ⋯)

@[simp]

theorem Finset.nodup_out_val {α : Type u_1} {s : Finset α} : (Quotient.out s.val).Nodup

@[simp]

theorem Finset.nodup_val {α : Type u_1} {s : Finset α} : s.val.Nodup

@[simp]

theorem Finset.mem_out_val {α : Type u_1} {s : Finset α} {x : α} : x ∈ Quotient.out s.val ↔ x ∈ s

theorem Finset.card_insert_erase_eq {α : Type u_1} {s : Finset α} {x y : α} [ha : DecidableEq α] (h₁ : x ∈ s) (h₂ : y ∉ s) : (insert y (s.erase x)).card = s.card

def Finset.map' {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : α → β) : Finset β

Equations

• s.map' f = s.biUnion fun (x : α) => {f x}

@[simp]

theorem Finset.mem_map'' {α : Type u_1} {β : Type u_2} {s : Finset α} [hb : DecidableEq β] {f : α → β} {y : β} : y ∈ s.map' f ↔ ∃ x ∈ s, f x = y

theorem Finset.sum_range_list_get! {xs : List ℝ} {f : ℝ → ℝ} : ∑ i ∈ range xs.length, f xs[i]! = (List.map f xs).sum

theorem Finset.prod_range_list_get! {xs : List ℝ} {f : ℝ → ℝ} : ∏ i ∈ range xs.length, f xs[i]! = (List.map f xs).prod

theorem Finset.le_sum_range {a : ℕ → ℝ} {N n : ℕ} (h : n < N) : |a n| ≤ ∑ i ∈ range N, |a i|

theorem Finset.one_le_prod_of_forall_one_le {ι : Type u_4} {s : Finset ι} {f : ι → ℝ} (h : ∀ i ∈ s, 1 ≤ f i) : 1 ≤ ∏ i ∈ s, f i

theorem Finset.sum_geom_eq {b : ℝ} {n : ℕ} (hb : b ≠ 1) : ∑ k ∈ range n, b ^ k = (1 - b ^ n) / (1 - b)

theorem Finset.sum_add_geom_eq' {b : ℝ} {n : ℕ} (hb : b ≠ 1) : ∑ k ∈ range n, ↑k * b ^ k = (b * ∑ k ∈ range n, b ^ k - ↑n * b ^ n) / (1 - b)

theorem Finset.sum_add_geom_eq {b : ℝ} {n : ℕ} (hb : b ≠ 1) : ∑ k ∈ range n, ↑k * b ^ k = (b ^ n * (↑n * b - ↑n - b) + b) / (1 - b) ^ 2

theorem Finset.card_filter_range_le_of_le {p : ℕ → Prop} {i j : ℕ} [hp : DecidablePred p] (h : i ≤ j) : (filter p (range i)).card ≤ (filter p (range j)).card

theorem Finset.Ico_add_right {n m k : ℕ} (h : n ≤ m) : Ico n (m + k) = Ico n m ∪ Ico m (m + k)

theorem Finset.card_filter_range_add {p : ℕ → Prop} {n k : ℕ} [hp : DecidablePred p] : {i ∈ range (n + k) | p i}.card = {i ∈ range n | p i}.card + {i ∈ Ico n (n + k) | p i}.card

theorem Finset.card_eq_one_iff_exiu {α : Type u_1} {s : Finset α} : s.card = 1 ↔ ∃! x : α, x ∈ s

theorem Finset.forall_iff_of_fintype {α : Type u_1} [ha : Fintype α] {p : α → Prop} : (∀ (x : α), p x) ↔ ∀ x ∈ Fintype.elems, p x

@[instance_reducible]

instance Finset.instDecidableForallOfFintypeOfDecidablePred_projects {α : Type u_1} [ha : Fintype α] {p : α → Prop} [hp : DecidablePred p] : Decidable (∀ (x : α), p x)

Equations

• Finset.instDecidableForallOfFintypeOfDecidablePred_projects = decidable_of_iff' (∀ x ∈ Fintype.elems, p x) ⋯