-- Mathlib/Data/List/Nodup.lean
lemma nodup_tail_reverse (l : List α) (h : l[0]? = l.getLast?) :
    Nodup l.reverse.tail ↔ Nodup l.tail

Proof state:
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.dropLast.Nodup ↔ l.tail.Nodup)
h : (a :: l)[0]? = (a :: l).getLast?
hl : ¬l = []
⊢ l.length ≠ 0

Tactic:
aesop

Result:
no goals

Proof state:
case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.dropLast.Nodup ↔ l.tail.Nodup)
hl : ¬l = []
h : a = l[l.length - 1]
⊢ (l[l.length - 1] :: l.dropLast).Nodup ↔ ([l.getLast hl] ++ l.dropLast).Nodup

Tactic:
simp [List.getLast_eq_getElem]

Result:
no goals

Proof state:
case cons
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.reverse.tail.Nodup ↔ l.tail.Nodup)
h : (a :: l)[0]? = (a :: l).getLast?
⊢ (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup

Tactic:
by_cases hl : l = []

Result:
case pos
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.reverse.tail.Nodup ↔ l.tail.Nodup)
h : (a :: l)[0]? = (a :: l).getLast?
hl : l = []
⊢ (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup

case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.reverse.tail.Nodup ↔ l.tail.Nodup)
h : (a :: l)[0]? = (a :: l).getLast?
hl : ¬l = []
⊢ (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup

Proof state:
case nil
α : Type u
h : [][0]? = [].getLast?
⊢ [].reverse.tail.Nodup ↔ [].tail.Nodup

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.dropLast.Nodup ↔ l.tail.Nodup)
hl : ¬l = []
h : a = l[l.length - 1]
⊢ l.Nodup = (l.dropLast ++ [l.getLast hl]).Nodup

Tactic:
simp [List.dropLast_eq_take]

Result:
no goals

Proof state:
case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.dropLast.Nodup ↔ l.tail.Nodup)
hl : ¬l = []
h : a = l[l.length - 1]
⊢ (a :: l.dropLast).Nodup ↔ l.Nodup

Tactic:
rw [h,
  show l.Nodup = (l.dropLast ++ [l.getLast hl]).Nodup by
    simp [List.dropLast_eq_take],
  List.nodup_append_comm]

Result:
case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.dropLast.Nodup ↔ l.tail.Nodup)
hl : ¬l = []
h : a = l[l.length - 1]
⊢ (l[l.length - 1] :: l.dropLast).Nodup ↔ ([l.getLast hl] ++ l.dropLast).Nodup

Proof state:
case pos
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.reverse.tail.Nodup ↔ l.tail.Nodup)
h : (a :: l)[0]? = (a :: l).getLast?
hl : l = []
⊢ (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup

Tactic:
aesop

Result:
no goals

Proof state:
case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.reverse.tail.Nodup ↔ l.tail.Nodup)
h : (a :: l)[0]? = (a :: l).getLast?
hl : ¬l = []
⊢ (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup

Tactic:
simp_all only [List.tail_reverse, List.nodup_reverse,
  List.dropLast_cons_of_ne_nil hl, List.tail_cons]

Result:
case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.dropLast.Nodup ↔ l.tail.Nodup)
h : (a :: l)[0]? = (a :: l).getLast?
hl : ¬l = []
⊢ (a :: l.dropLast).Nodup ↔ l.Nodup

Proof state:
case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.dropLast.Nodup ↔ l.tail.Nodup)
h : (a :: l)[0]? = (a :: l).getLast?
hl : ¬l = []
⊢ (a :: l.dropLast).Nodup ↔ l.Nodup

Tactic:
simp only [length_cons, Nat.zero_lt_succ, getElem?_eq_getElem, getElem_cons_zero,
  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

Result:
case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.dropLast.Nodup ↔ l.tail.Nodup)
hl : ¬l = []
h : a = l[l.length - 1]
⊢ (a :: l.dropLast).Nodup ↔ l.Nodup