mathlib3

11156f5a - feat(data/list/basic): Alias for `length_le_of_sublist` (#16841)

feat(data/list/basic): Alias for `length_le_of_sublist` (#16841) Make an alias `list.sublist.length_le` of `list.length_le_of_sublist` and use it. Rename `list.eq_of_sublist_of_length_eq` and `list.eq_of_sublist_of_length_le` to use dot notation.