-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem dropLast_eq_eraseIdx {xs : List α} {i : Nat} (last_idx : i + 1 = xs.length) :
    xs.dropLast = List.eraseIdx xs i

Proof state:
case succ.e_tail
α : Type u_1
n : Nat
ih : ∀ {xs : List α}, n + 1 = xs.length → xs.dropLast = xs.eraseIdx n
xs✝ : List α
x : α
xs : List α
last_idx : n + 1 = xs.length
⊢ xs.dropLast = xs.eraseIdx n

case succ.x_1
α : Type u_1
n : Nat
ih : ∀ {xs : List α}, n + 1 = xs.length → xs.dropLast = xs.eraseIdx n
xs✝ : List α
x : α
xs : List α
last_idx : n + 1 = xs.length
⊢ xs = [] → False

Tactic:
exact ih last_idx

Result:
case succ.x_1
α : Type u_1
n : Nat
ih : ∀ {xs : List α}, n + 1 = xs.length → xs.dropLast = xs.eraseIdx n
xs✝ : List α
x : α
xs : List α
last_idx : n + 1 = xs.length
⊢ xs = [] → False

Proof state:
case succ.x_1
α : Type u_1
n : Nat
ih : ∀ {xs : List α}, n + 1 = xs.length → xs.dropLast = xs.eraseIdx n
xs✝ : List α
x : α
xs : List α
last_idx : n + 1 = xs.length
⊢ xs = [] → False

Tactic:
exact fun _ => nomatch xs

Result:
no goals

Proof state:
α : Type u_1
xs : List α
i : Nat
last_idx : i + 1 = xs.length
⊢ xs.dropLast = xs.eraseIdx i

Tactic:
induction i generalizing xs with
| zero =>
  let [x] := xs
  rfl
| succ n ih =>
  let x::xs := xs
  simp at last_idx
  rw [dropLast, eraseIdx]
  congr
  exact ih last_idx
  exact fun _ => nomatch xs

Result:
no goals

Proof state:
case zero
α : Type u_1
xs : List α
last_idx : 0 + 1 = xs.length
⊢ xs.dropLast = xs.eraseIdx 0

Tactic:
let [x] := xs

Result:
case zero
α : Type u_1
xs : List α
x : α
last_idx : 0 + 1 = [x].length
⊢ [x].dropLast = [x].eraseIdx 0

Proof state:
case zero
α : Type u_1
xs : List α
x : α
last_idx : 0 + 1 = [x].length
⊢ [x].dropLast = [x].eraseIdx 0

Tactic:
rfl

Result:
no goals

Proof state:
case succ
α : Type u_1
n : Nat
ih : ∀ {xs : List α}, n + 1 = xs.length → xs.dropLast = xs.eraseIdx n
xs : List α
last_idx : n + 1 + 1 = xs.length
⊢ xs.dropLast = xs.eraseIdx (n + 1)

Tactic:
let x::xs := xs

Result:
case succ
α : Type u_1
n : Nat
ih : ∀ {xs : List α}, n + 1 = xs.length → xs.dropLast = xs.eraseIdx n
xs✝ : List α
x : α
xs : List α
last_idx : n + 1 + 1 = (x :: xs).length
⊢ (x :: xs).dropLast = (x :: xs).eraseIdx (n + 1)

Proof state:
case succ
α : Type u_1
n : Nat
ih : ∀ {xs : List α}, n + 1 = xs.length → xs.dropLast = xs.eraseIdx n
xs✝ : List α
x : α
xs : List α
last_idx : n + 1 = xs.length
⊢ x :: xs.dropLast = x :: xs.eraseIdx n

case succ.x_1
α : Type u_1
n : Nat
ih : ∀ {xs : List α}, n + 1 = xs.length → xs.dropLast = xs.eraseIdx n
xs✝ : List α
x : α
xs : List α
last_idx : n + 1 = xs.length
⊢ xs = [] → False

Tactic:
congr

Result:
case succ.e_tail
α : Type u_1
n : Nat
ih : ∀ {xs : List α}, n + 1 = xs.length → xs.dropLast = xs.eraseIdx n
xs✝ : List α
x : α
xs : List α
last_idx : n + 1 = xs.length
⊢ xs.dropLast = xs.eraseIdx n

case succ.x_1
α : Type u_1
n : Nat
ih : ∀ {xs : List α}, n + 1 = xs.length → xs.dropLast = xs.eraseIdx n
xs✝ : List α
x : α
xs : List α
last_idx : n + 1 = xs.length
⊢ xs = [] → False

Proof state:
case succ
α : Type u_1
n : Nat
ih : ∀ {xs : List α}, n + 1 = xs.length → xs.dropLast = xs.eraseIdx n
xs✝ : List α
x : α
xs : List α
last_idx : n + 1 + 1 = (x :: xs).length
⊢ (x :: xs).dropLast = (x :: xs).eraseIdx (n + 1)

Tactic:
simp at last_idx

Result:
case succ
α : Type u_1
n : Nat
ih : ∀ {xs : List α}, n + 1 = xs.length → xs.dropLast = xs.eraseIdx n
xs✝ : List α
x : α
xs : List α
last_idx : n + 1 = xs.length
⊢ (x :: xs).dropLast = (x :: xs).eraseIdx (n + 1)

Proof state:
case succ
α : Type u_1
n : Nat
ih : ∀ {xs : List α}, n + 1 = xs.length → xs.dropLast = xs.eraseIdx n
xs✝ : List α
x : α
xs : List α
last_idx : n + 1 = xs.length
⊢ (x :: xs).dropLast = (x :: xs).eraseIdx (n + 1)

Tactic:
rw [dropLast, eraseIdx]

Result:
case succ
α : Type u_1
n : Nat
ih : ∀ {xs : List α}, n + 1 = xs.length → xs.dropLast = xs.eraseIdx n
xs✝ : List α
x : α
xs : List α
last_idx : n + 1 = xs.length
⊢ x :: xs.dropLast = x :: xs.eraseIdx n

case succ.x_1
α : Type u_1
n : Nat
ih : ∀ {xs : List α}, n + 1 = xs.length → xs.dropLast = xs.eraseIdx n
xs✝ : List α
x : α
xs : List α
last_idx : n + 1 = xs.length
⊢ xs = [] → False