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
E : Type u₅
inst✝ : Category E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
K : D ⥤ E
⊢ whiskerRight (associator F G H).hom K ≫ (associator F (G ⋙ H) K).hom ≫ whiskerLeft F (associator G H K).hom =
    (associator (F ⋙ G) H K).hom ≫ (associator F G (H ⋙ K)).hom
aesop_cat