case nil
α : Type u
β : Type v
f✝ : ℕ → α → β
n✝ : ℕ
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n [] = List.oldMapIdx (fun i a => f (i + n) a) []

case cons
α : Type u
β : Type v
f✝ : ℕ → α → β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (f : ℕ → α → β) (n : ℕ), List.oldMapIdxCore f n tl = List.oldMapIdx (fun i a => f (i + n) a) tl
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n (hd :: tl) = List.oldMapIdx (fun i a => f (i + n) a) (hd :: tl)
α : Type u
β : Type v
l : List α
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n l = List.oldMapIdx (fun i a => f (i + n) a) l
induction' l with hd tl hl generalizing f n
no goals
case nil
α : Type u
β : Type v
f✝ : ℕ → α → β
n✝ : ℕ
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n [] = List.oldMapIdx (fun i a => f (i + n) a) []
rfl
case cons
α : Type u
β : Type v
f✝ : ℕ → α → β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (f : ℕ → α → β) (n : ℕ), List.oldMapIdxCore f n tl = List.oldMapIdx (fun i a => f (i + n) a) tl
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n (hd :: tl) = List.oldMapIdxCore (fun i a => f (i + n) a) 0 (hd :: tl)
case cons
α : Type u
β : Type v
f✝ : ℕ → α → β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (f : ℕ → α → β) (n : ℕ), List.oldMapIdxCore f n tl = List.oldMapIdx (fun i a => f (i + n) a) tl
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n (hd :: tl) = List.oldMapIdx (fun i a => f (i + n) a) (hd :: tl)
rw [List.oldMapIdx]
no goals
case cons
α : Type u
β : Type v
f✝ : ℕ → α → β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (f : ℕ → α → β) (n : ℕ), List.oldMapIdxCore f n tl = List.oldMapIdx (fun i a => f (i + n) a) tl
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n (hd :: tl) = List.oldMapIdxCore (fun i a => f (i + n) a) 0 (hd :: tl)
simp only [List.oldMapIdxCore, hl, add_left_comm, add_comm, add_zero, zero_add]