α : Type u
β : Type v
f : ℕ → α → β
⊢ ∀ (l : List α), mapIdx f l = List.oldMapIdx f l
α : Type u
β : Type v
⊢ ∀ (f : ℕ → α → β) (l : List α), mapIdx f l = List.oldMapIdx f l
intro f
case base
α : Type u
β : Type v
f : ℕ → α → β
⊢ mapIdx f [] = List.oldMapIdx f []

case ind
α : Type u
β : Type v
f : ℕ → α → β
⊢ ∀ (l : List α) (e : α), mapIdx f l = List.oldMapIdx f l → mapIdx f (l ++ [e]) = List.oldMapIdx f (l ++ [e])
α : Type u
β : Type v
f : ℕ → α → β
⊢ ∀ (l : List α), mapIdx f l = List.oldMapIdx f l
apply list_reverse_induction
no goals
case base
α : Type u
β : Type v
f : ℕ → α → β
⊢ mapIdx f [] = List.oldMapIdx f []
rfl
case ind
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
h : mapIdx f l = List.oldMapIdx f l
⊢ mapIdx f (l ++ [e]) = List.oldMapIdx f (l ++ [e])
case ind
α : Type u
β : Type v
f : ℕ → α → β
⊢ ∀ (l : List α) (e : α), mapIdx f l = List.oldMapIdx f l → mapIdx f (l ++ [e]) = List.oldMapIdx f (l ++ [e])
intro l e h
no goals
case ind
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
h : mapIdx f l = List.oldMapIdx f l
⊢ mapIdx f (l ++ [e]) = List.oldMapIdx f (l ++ [e])
rw [List.oldMapIdx_append, mapIdx_append_one, h]