English
Under a mild hypothesis, Nodup(l.reverse.tail) is equivalent to Nodup(l.tail).
Русский
При умеренной гипотезе Nodup(l.reverse.tail) эквивално Nodup(l.tail).
LaTeX
$$$\\operatorname{Nodup}(\\mathrm{reverse}(l).tail) \\iff \\operatorname{Nodup}(l.finite\\text{ tail})$$$
Lean4
theorem nodup_tail_reverse (l : List α) (h : l[0]? = l.getLast?) : Nodup l.reverse.tail ↔ Nodup l.tail := by
induction l with
| nil => simp
| cons a l ih =>
by_cases hl : l = []
· simp_all
· simp_all only [List.tail_reverse, List.nodup_reverse, List.dropLast_cons_of_ne_nil hl, List.tail_cons]
simp only [length_cons, Nat.zero_lt_succ, getElem?_eq_getElem, Nat.add_one_sub_one, Nat.lt_add_one,
Option.some.injEq, List.getElem_cons, show l.length ≠ 0 by aesop, ↓reduceDIte, getLast?_eq_getElem?] at h
rw [h, show l.Nodup = (l.dropLast ++ [l.getLast hl]).Nodup by simp [List.dropLast_eq_take],
List.nodup_append_comm]
simp [List.getLast_eq_getElem]
