Commit 2023-01-13 09:04 64e70429

View on Github →

feat: port Mathlib.Data.List.Sigma (#1493)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/Sigma.lean

added theorem List.Nodupkeys.eq_of_fst_eq

added theorem List.Nodupkeys.eq_of_mk_mem

added theorem List.Nodupkeys.kerase

added theorem List.Nodupkeys.kunion

added theorem List.Nodupkeys.pairwise_ne

added theorem List.Nodupkeys.sublist

added def List.Nodupkeys

added theorem List.Perm.kerase

added theorem List.Perm.kinsert

added theorem List.Perm.kreplace

added theorem List.Perm.kunion

added theorem List.Perm.kunion_left

added theorem List.Perm.kunion_right

added def List.dedupkeys

added theorem List.dedupkeys_cons

added def List.dlookup

added theorem List.dlookup_cons_eq

added theorem List.dlookup_cons_ne

added theorem List.dlookup_dedupkeys

added theorem List.dlookup_eq_none

added theorem List.dlookup_is_some

added theorem List.dlookup_kerase

added theorem List.dlookup_kerase_ne

added theorem List.dlookup_kinsert

added theorem List.dlookup_kinsert_ne

added theorem List.dlookup_kunion_eq_some

added theorem List.dlookup_kunion_left

added theorem List.dlookup_kunion_right

added theorem List.dlookup_nil

added theorem List.exists_of_kerase

added theorem List.exists_of_mem_keys

added theorem List.head?_lookupAll

added def List.kerase

added theorem List.kerase_append_left

added theorem List.kerase_append_right

added theorem List.kerase_comm

added theorem List.kerase_cons_eq

added theorem List.kerase_cons_ne

added theorem List.kerase_kerase

added theorem List.kerase_keys_subset

added theorem List.kerase_nil

added theorem List.kerase_of_not_mem_keys

added theorem List.kerase_sublist

added def List.kextract

added theorem List.kextract_eq_dlookup_kerase

added def List.keys

added theorem List.keys_cons

added theorem List.keys_kerase

added theorem List.keys_kreplace

added theorem List.keys_nil

added def List.kinsert

added theorem List.kinsert_def

added theorem List.kinsert_nodupkeys

added def List.kreplace

added theorem List.kreplace_nodupkeys

added theorem List.kreplace_of_forall_not

added theorem List.kreplace_self

added def List.kunion

added theorem List.kunion_cons

added theorem List.kunion_kerase

added theorem List.kunion_nil

added def List.lookupAll

added theorem List.lookupAll_cons_eq

added theorem List.lookupAll_cons_ne

added theorem List.lookupAll_eq_dlookup

added theorem List.lookupAll_eq_nil

added theorem List.lookupAll_length_le_one

added theorem List.lookupAll_nil

added theorem List.lookupAll_nodup

added theorem List.lookupAll_sublist

added theorem List.lookup_ext

added theorem List.map_dlookup_eq_find

added theorem List.mem_dlookup

added theorem List.mem_dlookup_iff

added theorem List.mem_dlookup_kunion

added theorem List.mem_dlookup_kunion_middle

added theorem List.mem_ext

added theorem List.mem_keys

added theorem List.mem_keys_kerase_of_ne

added theorem List.mem_keys_kinsert

added theorem List.mem_keys_kunion

added theorem List.mem_keys_of_mem

added theorem List.mem_keys_of_mem_keys_kerase

added theorem List.mem_lookupAll

added theorem List.nil_kunion

added theorem List.nodup_enum_map_fst

added theorem List.nodupkeys_cons

added theorem List.nodupkeys_dedupkeys

added theorem List.nodupkeys_iff_pairwise

added theorem List.nodupkeys_join

added theorem List.nodupkeys_nil

added theorem List.nodupkeys_singleton

added theorem List.not_eq_key

added theorem List.not_mem_keys

added theorem List.not_mem_keys_kerase

added theorem List.of_mem_dlookup

added theorem List.perm_dlookup

added theorem List.perm_lookupAll

added theorem List.perm_nodupkeys

added theorem List.sizeOf_dedupkeys

added theorem List.sizeOf_kerase