Commit 2021-12-27 16:46 46566c5b

View on Github →

split(data/list/infix): Split off data.list.basic (#11062) This moves list.prefix, list.subfix, list.infix, list.inits, list.tails and insert lemmas from data.list.basic to a new file data.list.infix.

Estimated changes

Modified src/algebra/free_monoid.lean

Modified src/data/list/basic.lean

deleted theorem list.cons_prefix_iff

deleted theorem list.drop_sublist

deleted theorem list.drop_subset

deleted theorem list.drop_suffix

deleted theorem list.eq_nil_iff_infix_nil

deleted theorem list.eq_nil_iff_prefix_nil

deleted theorem list.eq_nil_iff_suffix_nil

deleted theorem list.eq_nil_of_infix_nil

deleted theorem list.eq_nil_of_prefix_nil

deleted theorem list.eq_nil_of_suffix_nil

deleted theorem list.eq_of_infix_of_length_eq

deleted theorem list.eq_of_prefix_of_length_eq

deleted theorem list.eq_of_suffix_of_length_eq

deleted theorem list.eq_or_mem_of_mem_insert

deleted theorem list.infix.length_le

deleted theorem list.infix_append'

deleted theorem list.infix_append

deleted theorem list.infix_cons

deleted theorem list.infix_iff_prefix_suffix

deleted theorem list.infix_insert

deleted theorem list.infix_of_mem_join

deleted theorem list.infix_refl

deleted theorem list.init_prefix

deleted theorem list.init_sublist

deleted theorem list.init_subset

deleted theorem list.inits_append

deleted theorem list.inits_cons

deleted theorem list.inits_eq_tails

deleted theorem list.inits_reverse

deleted theorem list.insert.def

deleted theorem list.insert_nil

deleted theorem list.insert_of_mem

deleted theorem list.insert_of_not_mem

deleted theorem list.is_infix.filter

deleted theorem list.is_infix.trans

deleted theorem list.is_prefix.filter

deleted theorem list.is_prefix.filter_map

deleted theorem list.is_prefix.is_infix

deleted theorem list.is_prefix.reduce_option

deleted theorem list.is_prefix.trans

deleted theorem list.is_suffix.filter

deleted theorem list.is_suffix.is_infix

deleted theorem list.is_suffix.trans

deleted theorem list.length_inits

deleted theorem list.length_insert_of_mem

deleted theorem list.length_insert_of_not_mem

deleted theorem list.length_tails

deleted theorem list.map_prefix

deleted theorem list.map_reverse_inits

deleted theorem list.map_reverse_tails

deleted theorem list.mem_inits

deleted theorem list.mem_insert_iff

deleted theorem list.mem_insert_of_mem

deleted theorem list.mem_insert_self

deleted theorem list.mem_of_mem_drop

deleted theorem list.mem_of_mem_init

deleted theorem list.mem_of_mem_tail

deleted theorem list.mem_of_mem_take

deleted theorem list.mem_tails

deleted theorem list.nil_infix

deleted theorem list.nil_prefix

deleted theorem list.nil_suffix

deleted theorem list.nth_le_inits

deleted theorem list.nth_le_tails

deleted theorem list.prefix_append

deleted theorem list.prefix_append_right_inj

deleted theorem list.prefix_concat

deleted theorem list.prefix_cons_inj

deleted theorem list.prefix_iff_eq_append

deleted theorem list.prefix_iff_eq_take

deleted theorem list.prefix_of_prefix_length_le

deleted theorem list.prefix_or_prefix_of_prefix

deleted theorem list.prefix_refl

deleted theorem list.prefix_take_le_iff

deleted theorem list.reverse_prefix

deleted theorem list.reverse_suffix

deleted theorem list.sublist_insert

deleted theorem list.subset_insert

deleted theorem list.suffix_append

deleted theorem list.suffix_cons

deleted theorem list.suffix_cons_iff

deleted theorem list.suffix_iff_eq_append

deleted theorem list.suffix_iff_eq_drop

deleted theorem list.suffix_insert

deleted theorem list.suffix_of_suffix_length_le

deleted theorem list.suffix_or_suffix_of_suffix

deleted theorem list.suffix_refl

deleted theorem list.tail_sublist

deleted theorem list.tail_subset

deleted theorem list.tail_suffix

deleted theorem list.tails_append

deleted theorem list.tails_cons

deleted theorem list.tails_eq_inits

deleted theorem list.tails_reverse

deleted theorem list.take_prefix

deleted theorem list.take_sublist

deleted theorem list.take_subset

Modified src/data/list/forall2.lean

Created src/data/list/infix.lean

added theorem list.cons_prefix_iff

added theorem list.drop_sublist

added theorem list.drop_subset

added theorem list.drop_suffix

added theorem list.eq_nil_of_infix_nil

added theorem list.eq_of_infix_of_length_eq

added theorem list.eq_of_prefix_of_length_eq

added theorem list.eq_of_suffix_of_length_eq

added theorem list.eq_or_mem_of_mem_insert

added theorem list.infix.length_le

added theorem list.infix_append'

added theorem list.infix_append

added theorem list.infix_concat

added theorem list.infix_cons

added theorem list.infix_iff_prefix_suffix

added theorem list.infix_insert

added theorem list.infix_nil_iff

added theorem list.infix_of_mem_join

added theorem list.infix_refl

added theorem list.infix_rfl

added theorem list.init_prefix

added theorem list.init_sublist

added theorem list.init_subset

added theorem list.inits_append

added theorem list.inits_cons

added theorem list.inits_eq_tails

added theorem list.inits_reverse

added theorem list.insert.def

added theorem list.insert_nil

added theorem list.insert_of_mem

added theorem list.insert_of_not_mem

added theorem list.is_infix.filter

added theorem list.is_infix.trans

added theorem list.is_prefix.filter

added theorem list.is_prefix.filter_map

added theorem list.is_prefix.is_infix

added theorem list.is_prefix.map

added theorem list.is_prefix.reduce_option

added theorem list.is_prefix.trans

added theorem list.is_suffix.filter

added theorem list.is_suffix.is_infix

added theorem list.is_suffix.trans

added theorem list.length_inits

added theorem list.length_insert_of_mem

added theorem list.length_insert_of_not_mem

added theorem list.length_tails

added theorem list.map_reverse_inits

added theorem list.map_reverse_tails

added theorem list.mem_inits

added theorem list.mem_insert_iff

added theorem list.mem_insert_of_mem

added theorem list.mem_insert_self

added theorem list.mem_of_mem_drop

added theorem list.mem_of_mem_init

added theorem list.mem_of_mem_tail

added theorem list.mem_of_mem_take

added theorem list.mem_tails

added theorem list.nil_infix

added theorem list.nil_prefix

added theorem list.nil_suffix

added theorem list.nth_le_inits

added theorem list.nth_le_tails

added theorem list.prefix_append

added theorem list.prefix_append_right_inj

added theorem list.prefix_concat

added theorem list.prefix_cons_inj

added theorem list.prefix_iff_eq_append

added theorem list.prefix_iff_eq_take

added theorem list.prefix_nil_iff

added theorem list.prefix_of_prefix_length_le

added theorem list.prefix_or_prefix_of_prefix

added theorem list.prefix_refl

added theorem list.prefix_rfl

added theorem list.prefix_take_le_iff

added theorem list.reverse_prefix

added theorem list.reverse_suffix

added theorem list.sublist_insert

added theorem list.subset_insert

added theorem list.suffix_append

added theorem list.suffix_cons

added theorem list.suffix_cons_iff

added theorem list.suffix_iff_eq_append

added theorem list.suffix_iff_eq_drop

added theorem list.suffix_insert

added theorem list.suffix_nil_iff

added theorem list.suffix_of_suffix_length_le

added theorem list.suffix_or_suffix_of_suffix

added theorem list.suffix_refl

added theorem list.suffix_rfl

added theorem list.tail_sublist

added theorem list.tail_subset

added theorem list.tail_suffix

added theorem list.tails_append

added theorem list.tails_cons

added theorem list.tails_eq_inits

added theorem list.tails_reverse

added theorem list.take_prefix

added theorem list.take_sublist

added theorem list.take_subset

Modified src/data/list/lattice.lean

Modified src/data/nat/nth.lean