no goals
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
⊢ (associator F (𝟭 B) G).hom ≫ whiskerLeft F (leftUnitor G).hom = whiskerRight (rightUnitor F).hom G
aesop_cat