Commit 2024-12-20 05:03 899ea23a
View on Github →chore(Data/List/Lemmas): deprecate tail_reverse_eq_reverse_dropLast (#19874)
Makes tail_reverse_eq_reverse_dropLast a deprecated alias to tail_reverse, which was added to core in https://github.com/leanprover/lean4/pull/5360.
This duplicated lemma was found by tryAtEachStep.