Commit 2025-04-11 06:06 706ce8d7
View on Github →chore(Data/List/Basic): deprecate duplicate lemma erase_diff_erase_sublist_of_sublist (#23917)
Marks erase_diff_erase_sublist_of_sublist as a deprecated alias of Sublist.erase_diff_erase_sublist.
This duplication was found by tryAtEachStep.