case nil
α✝ : Type u
β : Type v
α : Type u_1
L : List α
f✝ f : ℕ → α → β
⊢ mapIdx f ([] ++ L) = mapIdx f [] ++ mapIdx (fun i a => f (i + length []) a) L

case cons
α✝ : Type u
β : Type v
α : Type u_1
L : List α
f✝ : ℕ → α → β
a : α
J : List α
IH : ∀ (f : ℕ → α → β), mapIdx f (J ++ L) = mapIdx f J ++ mapIdx (fun i a => f (i + length J) a) L
f : ℕ → α → β
⊢ mapIdx f (a :: J ++ L) = mapIdx f (a :: J) ++ mapIdx (fun i a_1 => f (i + length (a :: J)) a_1) L
α✝ : Type u
β : Type v
α : Type u_1
K L : List α
f : ℕ → α → β
⊢ mapIdx f (K ++ L) = mapIdx f K ++ mapIdx (fun i a => f (i + length K) a) L
induction' K with a J IH generalizing f
no goals
case nil
α✝ : Type u
β : Type v
α : Type u_1
L : List α
f✝ f : ℕ → α → β
⊢ mapIdx f ([] ++ L) = mapIdx f [] ++ mapIdx (fun i a => f (i + length []) a) L
rfl
no goals
case cons
α✝ : Type u
β : Type v
α : Type u_1
L : List α
f✝ : ℕ → α → β
a : α
J : List α
IH : ∀ (f : ℕ → α → β), mapIdx f (J ++ L) = mapIdx f J ++ mapIdx (fun i a => f (i + length J) a) L
f : ℕ → α → β
⊢ mapIdx f (a :: J ++ L) = mapIdx f (a :: J) ++ mapIdx (fun i a_1 => f (i + length (a :: J)) a_1) L
simp [IH fun i ↦ f (i + 1), add_assoc]