case nil
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
f✝ f : ℕ → α → β
⊢ mapIdx f [] = ofFn fun i => f (↑i) (get [] i)

case cons
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
f✝ : ℕ → α → β
hd : α
tl : List α
IH : ∀ (f : ℕ → α → β), mapIdx f tl = ofFn fun i => f (↑i) (get tl i)
f : ℕ → α → β
⊢ mapIdx f (hd :: tl) = ofFn fun i => f (↑i) (get (hd :: tl) i)
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
l : List α
f : ℕ → α → β
⊢ mapIdx f l = ofFn fun i => f (↑i) (get l i)
induction' l with hd tl IH generalizing f
no goals
case nil
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
f✝ f : ℕ → α → β
⊢ mapIdx f [] = ofFn fun i => f (↑i) (get [] i)
rfl
no goals
case cons
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
f✝ : ℕ → α → β
hd : α
tl : List α
IH : ∀ (f : ℕ → α → β), mapIdx f tl = ofFn fun i => f (↑i) (get tl i)
f : ℕ → α → β
⊢ mapIdx f (hd :: tl) = ofFn fun i => f (↑i) (get (hd :: tl) i)
simp [IH]