dsimp [mapF.compositor, mapF.compositorLax] at *
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
a : α
as : List α
h_ind :
  NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      as =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) as
⊢ NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      (a :: as) =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) (a :: as)
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
a : α
as : List α
h_ind :
  (NatTrans.app (Prefunctor.map mapF.toPrefunctor ψ)
          (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F₁).toPrefunctor as) ≫
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor G₂).toPrefunctor
          (NatTrans.app (Prefunctor.map mapF.toPrefunctor φ) as)) ≫
      mapF.compositorLax F₂ G₂ as =
    mapF.compositorLax F₁ G₁ as ≫ NatTrans.app (Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) as
⊢ DVect2.cons
      ((NatTrans.app ψ (Prefunctor.obj F₁.toPrefunctor a) ≫ Prefunctor.map G₂.toPrefunctor (NatTrans.app φ a)) ≫
        𝟙 (Prefunctor.obj G₂.toPrefunctor (Prefunctor.obj F₂.toPrefunctor a)))
      ((NatTrans.app (Prefunctor.map mapF.toPrefunctor ψ)
            (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F₁).toPrefunctor as) ≫
          Prefunctor.map (Prefunctor.obj mapF.toPrefunctor G₂).toPrefunctor
            (NatTrans.app (Prefunctor.map mapF.toPrefunctor φ) as)) ≫
        mapF.compositorLax F₂ G₂ as) =
    DVect2.cons
      (𝟙 (Prefunctor.obj G₁.toPrefunctor (Prefunctor.obj F₁.toPrefunctor a)) ≫
        NatTrans.app ψ (Prefunctor.obj F₁.toPrefunctor a) ≫ Prefunctor.map G₂.toPrefunctor (NatTrans.app φ a))
      (mapF.compositorLax F₁ G₁ as ≫ NatTrans.app (Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) as)