dsimp [Functor.comp, mapF]
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ Prefunctor.obj mapF.toPrefunctor (F ⋙ G) = Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ Functor.mk
      { obj := List.map fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X),
        map :=
          fun {X Y} ↦
            DVect2.map (fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X))
              (fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X))
              fun {a b} f ↦ Prefunctor.map G.toPrefunctor (Prefunctor.map F.toPrefunctor f) } =
    Functor.mk
      { obj := fun X ↦ List.map G.toPrefunctor.obj (List.map F.toPrefunctor.obj X),
        map :=
          fun {X Y} f ↦
            DVect2.map G.toPrefunctor.obj G.toPrefunctor.obj (fun {a b} ↦ Prefunctor.map G.toPrefunctor)
              (DVect2.map F.toPrefunctor.obj F.toPrefunctor.obj (fun {a b} ↦ Prefunctor.map F.toPrefunctor) f) }