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
F : A ⥤ B
G : B ⥤ C
x✝ : A
⊢ 𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)) ≫
      𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)) =
    Prefunctor.map G.toPrefunctor (𝟙 (Prefunctor.obj F.toPrefunctor x✝))
no goals