-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem getLast_mapIdx {l : List α} {f : Nat → α → β} {h} :
    (mapIdx f l).getLast h = f (l.length - 1) (l.getLast (by simpa using h))

Proof state:
case cons
α : Type u_1
β : Type u_2
f : Nat → α → β
head✝ : α
tail✝ : List α
h : mapIdx f (head✝ :: tail✝) ≠ []
⊢ (mapIdx f (head✝ :: tail✝)).getLast h = f ((head✝ :: tail✝).length - 1) (head✝ :: tail✝)[tail✝.length]

Tactic:
simp only [mapIdx_cons]

Result:
case cons
α : Type u_1
β : Type u_2
f : Nat → α → β
head✝ : α
tail✝ : List α
h : mapIdx f (head✝ :: tail✝) ≠ []
⊢ (f 0 head✝ :: mapIdx (fun i => f (i + 1)) tail✝).getLast ⋯ =
    f ((head✝ :: tail✝).length - 1) (head✝ :: tail✝)[tail✝.length]

Proof state:
case cons
α : Type u_1
β : Type u_2
f : Nat → α → β
head✝ : α
tail✝ : List α
h : mapIdx f (head✝ :: tail✝) ≠ []
⊢ f (mapIdx (fun i => f (i + 1)) tail✝).length (head✝ :: tail✝)[(mapIdx (fun i => f (i + 1)) tail✝).length] =
    f ((head✝ :: tail✝).length - 1) (head✝ :: tail✝)[tail✝.length]

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.98299
β : Type ?u.98312
l : List α
f : Nat → α → β
h : mapIdx f l ≠ []
⊢ l ≠ []

Tactic:
simpa using h

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : Nat → α → β
head✝ : α
tail✝ : List α
h : mapIdx f (head✝ :: tail✝) ≠ []
⊢ (f 0 head✝ :: mapIdx (fun i => f (i + 1)) tail✝)[(mapIdx (fun i => f (i + 1)) tail✝).length] =
    f ((head✝ :: tail✝).length - 1) (head✝ :: tail✝)[tail✝.length]

Tactic:
simp only [← mapIdx_cons, getElem_mapIdx]

Result:
case cons
α : Type u_1
β : Type u_2
f : Nat → α → β
head✝ : α
tail✝ : List α
h : mapIdx f (head✝ :: tail✝) ≠ []
⊢ f (mapIdx (fun i => f (i + 1)) tail✝).length (head✝ :: tail✝)[(mapIdx (fun i => f (i + 1)) tail✝).length] =
    f ((head✝ :: tail✝).length - 1) (head✝ :: tail✝)[tail✝.length]

Proof state:
case cons
α : Type u_1
β : Type u_2
f : Nat → α → β
head✝ : α
tail✝ : List α
h : mapIdx f (head✝ :: tail✝) ≠ []
⊢ (mapIdx f (head✝ :: tail✝)).getLast h = f ((head✝ :: tail✝).length - 1) ((head✝ :: tail✝).getLast ⋯)

Tactic:
simp only [← getElem_cons_length _ _ _ rfl]

Result:
case cons
α : Type u_1
β : Type u_2
f : Nat → α → β
head✝ : α
tail✝ : List α
h : mapIdx f (head✝ :: tail✝) ≠ []
⊢ (mapIdx f (head✝ :: tail✝)).getLast h = f ((head✝ :: tail✝).length - 1) (head✝ :: tail✝)[tail✝.length]

Proof state:
case nil
α : Type u_1
β : Type u_2
f : Nat → α → β
h : mapIdx f [] ≠ []
⊢ (mapIdx f []).getLast h = f ([].length - 1) ([].getLast ⋯)

Tactic:
simp at h

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : Nat → α → β
head✝ : α
tail✝ : List α
h : mapIdx f (head✝ :: tail✝) ≠ []
⊢ (f 0 head✝ :: mapIdx (fun i => f (i + 1)) tail✝).getLast ⋯ =
    f ((head✝ :: tail✝).length - 1) (head✝ :: tail✝)[tail✝.length]

Tactic:
simp only [← getElem_cons_length _ _ _ rfl]

Result:
case cons
α : Type u_1
β : Type u_2
f : Nat → α → β
head✝ : α
tail✝ : List α
h : mapIdx f (head✝ :: tail✝) ≠ []
⊢ (f 0 head✝ :: mapIdx (fun i => f (i + 1)) tail✝)[(mapIdx (fun i => f (i + 1)) tail✝).length] =
    f ((head✝ :: tail✝).length - 1) (head✝ :: tail✝)[tail✝.length]

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
h : mapIdx f l ≠ []
⊢ (mapIdx f l).getLast h = f (l.length - 1) (l.getLast ⋯)

Tactic:
cases l with
| nil => simp at h
| cons _ _ =>
  simp only [← getElem_cons_length _ _ _ rfl]
  simp only [mapIdx_cons]
  simp only [← getElem_cons_length _ _ _ rfl]
  simp only [← mapIdx_cons, getElem_mapIdx]
  simp

Result:
no goals