mathlib

13393e3c - chore(data/list/*): various renamings to use dot notation (#2481)

chore(data/list/*): various renamings to use dot notation (#2481) * use dot notation * add a version of `list.perm.prod_eq` that only assumes that elements of the list pairwise commute instead of commutativity of the monoid. ## List of renamed symbols ### `data/list/basic` * `append_sublist_append_of_sublist_right` : `sublist.append_right`; * `reverse_sublist` : `sublist.reverse`; * `append_sublist_append` : `sublist.append`; * `subset_of_sublist`: `sublist.subset`; * `sublist_antisymm` : `sublist.antisymm`; * `filter_map_sublist_filter_map` : `sublist.filter_map` * `map_sublist_map` : `sublist.map` * `erasep_sublist_erasep`: `sublist.erasep` * `erase_sublist_erase` : `sublist.erase`; * `diff_sublist_of_sublist` : `sublist.diff_right`; ### `data/list/perm` * `perm.skip` : `perm.cons`; * `perm_comm` (new); * `perm_subset` : `perm.subset`; * `mem_of_perm` : `perm.mem_iff`; * `perm_app_left` : `perm.append_right` (note `right` vs `left`) * `perm_app_right` : `perm.append_left` (note `right` vs `left`) * `perm_app` : `perm.append`; * `perm_app_cons` : `perm.append_cons`; * `perm_cons_app` : `perm_append_singleton`; * `perm_app_comm` : `perm_append_comm`; * `perm_length` : `perm.length_eq`; * `eq_nil_of_perm_nil` : `perm.eq_nil` and `perm.nil_eq` with different choices of lhs/rhs; * `eq_singleton_of_perm_inv` : `perm.eq_singleton` and `perm.singleton_eq` with different choices of lhs/rhs; * `perm_singleton` and `singleton_perm`: `iff` versions of `perm.eq_singleton` and `perm.singleton_eq`; * `eq_singleton_of_perm` : `singleton_perm_singleton`; * `perm_cons_app_cons` : `perm_cons_append_cons`; * `perm_repeat` : `repeat_perm`; new `perm_repeat` differs from it in the choice of lhs/rhs; * `perm_erase` : `perm_cons_erase`; * `perm_filter_map` : `perm.filter_map`; * `perm_map` : `perm.map`; * `perm_pmap` : `perm.pmap`; * `perm_filter` : `perm.filter`; * `subperm_of_sublist` : `sublist.subperm`; * `subperm_of_perm` : `perm.subperm`; * `subperm.refl` : now has `@[refl]` attribute; * `subperm.trans` : now has `@[trans]` attribute; * `length_le_of_subperm` : `subperm.length_le`; * `subset_of_subperm` : `subperm.subset`; * `exists_perm_append_of_sublist` : `sublist.exists_perm_append`; * `perm_countp` : `perm.countp_eq`; * `countp_le_of_subperm` : `subperm.countp_le`; * `perm_count` : `perm.count_eq`; * `count_le_of_subperm` : `subperm.count_le`; * `foldl_eq_of_perm` : `perm.foldl_eq`, added a primed version with slightly weaker assumptions; * `foldr_eq_of_perm` : `perm.foldr_eq`; * `rec_heq_of_perm` : `perm.eec_heq`; * `fold_op_eq_of_perm` : `perm.fold_op_eq`; * `prod_eq_of_perm`: `perm.prod_eq` and `perm.prod_eq'`; * `perm_cons_inv` : `perm.cons_inv`; * `perm_cons` : now is a `@[simp]` lemma; * `perm_app_right_iff` : `perm_append_right_iff`; * `subperm_app_left` : `subperm_append_left`; * `subperm_app_right` : `subperm_append_right`; * `perm_ext_sublist_nodup` : `nodup.sublist_ext`; * `erase_perm_erase` : `perm.erase`; * `subperm_cons_erase` (new); * `erase_subperm_erase` : `subperm.erase`; * `perm_diff_left` : `perm.diff_right` (note `left` vs `right`); * `perm_diff_right` : `perm.diff_left` (note `left` vs `right`); * `perm.diff`, `subperm.diff_right`, `erase_cons_subperm_cons_erase` (new); * `perm_bag_inter_left` : `perm.bag_inter_right` (note `left` vs `right`); * `perm_bag_inter_right` : `perm.bag_inter_left` (note `left` vs `right`); * `perm.bag_inter` (new); * `perm_erase_dup_of_perm` : `perm.erase_dup`; * `perm_union_left` : `perm.union_right` (note `left` vs `right`); * `perm_union_right` : `perm.union_left` (note `left` vs `right`); * `perm_union` : `perm.union`; * `perm_inter_left` : `perm.inter_right` (note `left` vs `right`); * `perm_inter_right` : `perm.inter_left` (note `left` vs `right`); * `perm_inter` : `perm.inter`; * `perm_nodup` : `perm.nodup_iff`; * `perm_bind_left` : `perm.bind_right` (note `left` vs `right`); * `perm_bind_right` : `perm.bind_left` (note `left` vs `right`); * `perm_product_left` : `perm.product_right` (note `left` vs `right`); * `perm_product_right` : `peerm.product_left` (note `left` vs `right`); * `perm_product` : `perm.product`; * `perm_erasep` : `perm.erasep`; ### `data/list/sigma` * `nodupkeys.pairwise_ne` (new); * `perm_kreplace` : `perm.kreplace`; * `perm_kerase` : `perm.kerase`; * `perm_kinsert` : `perm.kinsert`; * `erase_dupkeys_cons` : now take `x : sigma β` instead of `{x : α}` and `{y : β x}`; * `perm_kunion_left` : `perm.kunion_right` (note `left` vs `right`); * `perm_kunion_right` : `perm.kunion_left` (note `left` vs `right`); * `perm_kunion` : `perm.kunion`; *