Commit 2023-12-10 21:34 ee5a1c52

View on Github →

chore: patch std4#89 (#8566)

Estimated changes

Modified Archive/Wiedijk100Theorems/BallotProblem.lean

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/Finset/Sort.lean

Modified Mathlib/Data/Finsupp/BigOperators.lean

Modified Mathlib/Data/List/FinRange.lean

Modified Mathlib/Data/List/Perm.lean

deleted theorem List.Nodup.sublist_ext

deleted theorem List.Pairwise.perm

deleted theorem List.Perm.append

deleted theorem List.Perm.append_cons

deleted theorem List.Perm.append_left

deleted theorem List.Perm.append_right

deleted theorem List.Perm.bind_right

deleted theorem List.Perm.cons_inv

deleted theorem List.Perm.countP_congr

deleted theorem List.Perm.countP_eq

deleted theorem List.Perm.count_eq

deleted theorem List.Perm.diff

deleted theorem List.Perm.diff_left

deleted theorem List.Perm.diff_right

deleted theorem List.Perm.eq_nil

deleted theorem List.Perm.eqv

deleted theorem List.Perm.erase

deleted theorem List.Perm.filter

deleted theorem List.Perm.filterMap

deleted theorem List.Perm.foldl_eq'

deleted theorem List.Perm.inter

deleted theorem List.Perm.inter_left

deleted theorem List.Perm.inter_right

deleted theorem List.Perm.join

deleted theorem List.Perm.join_congr

deleted theorem List.Perm.length_eq

deleted theorem List.Perm.map

deleted theorem List.Perm.mem_iff

deleted theorem List.Perm.nil_eq

deleted theorem List.Perm.nodup_iff

deleted theorem List.Perm.of_eq

deleted theorem List.Perm.pairwise

deleted theorem List.Perm.pairwise_iff

deleted theorem List.Perm.pmap

deleted theorem List.Perm.rec_heq

deleted theorem List.Perm.sizeOf_eq_sizeOf

deleted theorem List.Perm.subperm

deleted theorem List.Perm.subperm_left

deleted theorem List.Perm.subperm_right

deleted theorem List.Perm.subset

deleted theorem List.Perm.swap'

deleted theorem List.Perm.union

deleted theorem List.Perm.union_left

deleted theorem List.Perm.union_right

deleted inductive List.Perm

deleted theorem List.Sublist.exists_perm_append

deleted theorem List.Sublist.subperm

deleted theorem List.Subperm.antisymm

deleted theorem List.Subperm.cons_left

deleted theorem List.Subperm.cons_right

deleted theorem List.Subperm.countP_le

deleted theorem List.Subperm.count_le

deleted theorem List.Subperm.diff_right

deleted theorem List.Subperm.erase

deleted theorem List.Subperm.exists_of_length_lt

deleted theorem List.Subperm.filter

deleted theorem List.Subperm.length_le

deleted theorem List.Subperm.perm_of_length_le

deleted theorem List.Subperm.refl

deleted theorem List.Subperm.subset

deleted theorem List.Subperm.trans

deleted def List.Subperm

deleted theorem List.concat_perm

deleted theorem List.cons_perm_iff_perm_erase

deleted theorem List.countP_eq_countP_filter_add

deleted theorem List.erase_cons_subperm_cons_erase

deleted theorem List.erase_subperm

deleted theorem List.exists_perm_sublist

deleted theorem List.filter_append_perm

deleted theorem List.nil_perm

deleted theorem List.nil_subperm

deleted theorem List.not_perm_nil_cons

deleted theorem List.perm_append_comm

deleted theorem List.perm_append_left_iff

deleted theorem List.perm_append_right_iff

deleted theorem List.perm_append_singleton

deleted theorem List.perm_comm

deleted theorem List.perm_cons

deleted theorem List.perm_cons_append_cons

deleted theorem List.perm_cons_erase

deleted theorem List.perm_ext

deleted theorem List.perm_iff_count

deleted theorem List.perm_induction_on

deleted theorem List.perm_insertNth

deleted theorem List.perm_insert_swap

deleted theorem List.perm_inv_core

deleted theorem List.perm_middle

deleted theorem List.perm_nil

deleted theorem List.perm_replicate

deleted theorem List.perm_singleton

deleted theorem List.replicate_perm

deleted theorem List.reverse_perm

deleted theorem List.singleton_perm

deleted theorem List.singleton_perm_singleton

modified theorem List.singleton_subperm_iff

deleted theorem List.subperm_append_diff_self_of_count_le

deleted theorem List.subperm_append_left

deleted theorem List.subperm_append_right

deleted theorem List.subperm_cons

deleted theorem List.subperm_cons_diff

deleted theorem List.subperm_cons_erase

deleted theorem List.subperm_ext_iff

added theorem List.subperm_singleton_iff'

deleted theorem List.subperm_singleton_iff

deleted theorem List.subset_cons_diff

Modified Mathlib/Data/List/Sigma.lean

Modified Mathlib/Data/List/Sublists.lean

Modified Mathlib/Data/Multiset/Basic.lean

Modified Mathlib/Data/Multiset/Nodup.lean

Modified Mathlib/Data/Multiset/Powerset.lean

Modified Mathlib/Data/Multiset/Sym.lean

Modified Mathlib/Data/Nat/Factors.lean

Modified Mathlib/Data/Sym/Basic.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Basic.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Type.lean

Modified Mathlib/GroupTheory/Perm/Support.lean

Modified Mathlib/NumberTheory/SmoothNumbers.lean

Modified Mathlib/Testing/SlimCheck/Functions.lean

Modified lake-manifest.json

Modified test/MkIffOfInductive.lean