ext as
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
⊢ (Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom =
    (mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)
case w.h
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
as : List α
⊢ 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