-- Mathlib/Data/List/Nodup.lean
theorem Nodup.erase_getElem [DecidableEq α] {l : List α} (hl : l.Nodup)
    (i : Nat) (h : i < l.length) : l.erase l[i] = l.eraseIdx ↑i

Proof state:
case cons.succ
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
IH : l.Nodup → ∀ (i : ℕ) (h : i < l.length), l.erase l[i] = l.eraseIdx i
hl : (a :: l).Nodup
i : ℕ
h : i + 1 < (a :: l).length
⊢ (a :: l).erase (a :: l)[i + 1] = (a :: l).eraseIdx (i + 1)

Tactic:
rw [nodup_cons] at hl

Result:
case cons.succ
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
IH : l.Nodup → ∀ (i : ℕ) (h : i < l.length), l.erase l[i] = l.eraseIdx i
hl : a ∉ l ∧ l.Nodup
i : ℕ
h : i + 1 < (a :: l).length
⊢ (a :: l).erase (a :: l)[i + 1] = (a :: l).eraseIdx (i + 1)

Proof state:
case cons.succ
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
IH : l.Nodup → ∀ (i : ℕ) (h : i < l.length), l.erase l[i] = l.eraseIdx i
hl : a ∉ l ∧ l.Nodup
i : ℕ
h : i + 1 < (a :: l).length
⊢ ¬(a == (a :: l)[i + 1]) = true

Tactic:
rw [beq_iff_eq]

Result:
case cons.succ
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
IH : l.Nodup → ∀ (i : ℕ) (h : i < l.length), l.erase l[i] = l.eraseIdx i
hl : a ∉ l ∧ l.Nodup
i : ℕ
h : i + 1 < (a :: l).length
⊢ ¬a = (a :: l)[i + 1]

Proof state:
case cons.zero
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
IH : l.Nodup → ∀ (i : ℕ) (h : i < l.length), l.erase l[i] = l.eraseIdx i
hl : (a :: l).Nodup
h : 0 < (a :: l).length
⊢ (a :: l).erase (a :: l)[0] = (a :: l).eraseIdx 0

Tactic:
simp

Result:
no goals

Proof state:
case nil
α : Type u
inst✝ : DecidableEq α
hl : [].Nodup
i : ℕ
h : i < [].length
⊢ [].erase [][i] = [].eraseIdx i

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
IH : l.Nodup → ∀ (i : ℕ) (h : i < l.length), l.erase l[i] = l.eraseIdx i
hl : a ∉ l ∧ l.Nodup
i : ℕ
h : i + 1 < (a :: l).length
⊢ (a :: l).erase (a :: l)[i + 1] = (a :: l).eraseIdx (i + 1)

Tactic:
rw [erase_cons_tail]

Result:
case cons.succ
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
IH : l.Nodup → ∀ (i : ℕ) (h : i < l.length), l.erase l[i] = l.eraseIdx i
hl : a ∉ l ∧ l.Nodup
i : ℕ
h : i + 1 < (a :: l).length
⊢ a :: l.erase (a :: l)[i + 1] = (a :: l).eraseIdx (i + 1)

case cons.succ
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
IH : l.Nodup → ∀ (i : ℕ) (h : i < l.length), l.erase l[i] = l.eraseIdx i
hl : a ∉ l ∧ l.Nodup
i : ℕ
h : i + 1 < (a :: l).length
⊢ ¬(a == (a :: l)[i + 1]) = true

Proof state:
case cons.succ
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
IH : l.Nodup → ∀ (i : ℕ) (h : i < l.length), l.erase l[i] = l.eraseIdx i
hl : a ∉ l ∧ l.Nodup
i : ℕ
h : i + 1 < (a :: l).length
⊢ a :: l.erase (a :: l)[i + 1] = (a :: l).eraseIdx (i + 1)

Tactic:
simp [IH hl.2]

Result:
no goals

Proof state:
case cons.succ
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
IH : l.Nodup → ∀ (i : ℕ) (h : i < l.length), l.erase l[i] = l.eraseIdx i
hl : a ∉ l ∧ l.Nodup
i : ℕ
h : i + 1 < (a :: l).length
⊢ ¬a = (a :: l)[i + 1]

Tactic:
simp only [getElem_cons_succ]

Result:
case cons.succ
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
IH : l.Nodup → ∀ (i : ℕ) (h : i < l.length), l.erase l[i] = l.eraseIdx i
hl : a ∉ l ∧ l.Nodup
i : ℕ
h : i + 1 < (a :: l).length
⊢ ¬a = l[i]

Proof state:
case cons.succ
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
IH : l.Nodup → ∀ (i : ℕ) (h : i < l.length), l.erase l[i] = l.eraseIdx i
hl : a ∉ l ∧ l.Nodup
i : ℕ
h : i + 1 < (a :: l).length
⊢ ¬a = l[i]

Tactic:
simp only [length_cons, Nat.succ_eq_add_one, Nat.add_lt_add_iff_right] at h

Result:
case cons.succ
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
IH : l.Nodup → ∀ (i : ℕ) (h : i < l.length), l.erase l[i] = l.eraseIdx i
hl : a ∉ l ∧ l.Nodup
i : ℕ
h✝ : i + 1 < (a :: l).length
h : i < l.length
⊢ ¬a = l[i]