α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdx f (l ++ [e]) = List.oldMapIdx f l ++ [f (length l) e]
α : Type u
β : Type v
⊢ ∀ (f : ℕ → α → β) (l : List α) (e : α), List.oldMapIdx f (l ++ [e]) = List.oldMapIdx f l ++ [f (length l) e]
intros f l e
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdxCore f 0 (l ++ [e]) = List.oldMapIdxCore f 0 l ++ [f (length l) e]
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdx f (l ++ [e]) = List.oldMapIdx f l ++ [f (length l) e]
unfold List.oldMapIdx
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdxCore f 0 l ++ List.oldMapIdxCore f (0 + length l) [e] = List.oldMapIdxCore f 0 l ++ [f (length l) e]
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdxCore f 0 (l ++ [e]) = List.oldMapIdxCore f 0 l ++ [f (length l) e]
rw [List.oldMapIdxCore_append f 0 l [e]]
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdxCore f (length l) [e] = [f (length l) e]
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdxCore f 0 l ++ List.oldMapIdxCore f (0 + length l) [e] = List.oldMapIdxCore f 0 l ++ [f (length l) e]
simp only [zero_add, append_cancel_left_eq]
no goals
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdxCore f (length l) [e] = [f (length l) e]
rfl