. intro as
  change List.map id as = as
  rw [List.map_id]
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a : List α),
    Prefunctor.obj
        (Prefunctor.obj mapF.toPrefunctor (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f })).toPrefunctor a =
      a

case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map
        (Prefunctor.obj mapF.toPrefunctor (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f })).toPrefunctor f)
      f
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map
        (Prefunctor.obj mapF.toPrefunctor (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f })).toPrefunctor f)
      f