Skip to content

Commit 899ea23

Browse files
committed
chore(Data/List/Lemmas): deprecate tail_reverse_eq_reverse_dropLast (#19874)
Makes `tail_reverse_eq_reverse_dropLast` a deprecated alias to [`tail_reverse`](https://github.com/leanprover/lean4/blob/938651121f3d8819109eee75722a1de087feff71/src/Init/Data/List/Lemmas.lean#L2990-L2994), which was added to core in leanprover/lean4#5360. This duplicated lemma was found by [`tryAtEachStep`](https://github.com/dwrensha/tryAtEachStep).
1 parent 7a9aa7e commit 899ea23

File tree

1 file changed

+1
-10
lines changed

1 file changed

+1
-10
lines changed

Mathlib/Data/List/Lemmas.lean

Lines changed: 1 addition & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -31,16 +31,7 @@ lemma count_flatMap [BEq β] (l : List α) (f : α → List β) (x : β) :
3131

3232
@[deprecated (since := "2024-08-20")] alias getElem_reverse' := getElem_reverse
3333

34-
theorem tail_reverse_eq_reverse_dropLast (l : List α) :
35-
l.reverse.tail = l.dropLast.reverse := by
36-
ext i v; by_cases hi : i < l.length - 1
37-
· simp only [← drop_one]
38-
rw [getElem?_eq_getElem (by simpa), getElem?_eq_getElem (by simpa),
39-
← getElem_drop' _, getElem_reverse, getElem_reverse, getElem_dropLast]
40-
· simp [show l.length - 1 - (1 + i) = l.length - 1 - 1 - i by omega]
41-
all_goals ((try simp); omega)
42-
· rw [getElem?_eq_none, getElem?_eq_none]
43-
all_goals (simp; omega)
34+
@[deprecated (since := "2024-12-10")] alias tail_reverse_eq_reverse_dropLast := tail_reverse
4435

4536
@[deprecated (since := "2024-08-19")] alias nthLe_tail := getElem_tail
4637

0 commit comments

Comments
 (0)