simp
case w.h
A : Type u₁
inst✝⁴ : Category A
B : Type u₂
inst✝³ : Category B
C : Type u₃
inst✝² : Category C
D : Type u₄
inst✝¹ : Category D
E : Type u₅
inst✝ : Category E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
K : D ⥤ E
x✝ : A
⊢ Prefunctor.map K.toPrefunctor
        (𝟙 (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)))) ≫
      𝟙
          (Prefunctor.obj K.toPrefunctor
            (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)))) ≫
        𝟙
          (Prefunctor.obj K.toPrefunctor
            (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)))) =
    𝟙
        (Prefunctor.obj K.toPrefunctor
          (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)))) ≫
      𝟙
        (Prefunctor.obj K.toPrefunctor
          (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝))))
no goals