no goals
ι : Type u_1
V : Type u
inst✝⁵ : Category V
inst✝⁴ : Preadditive V
c✝ : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c✝
f✝ g : C✝ ⟶ D✝
h k : D✝ ⟶ E
i : ι
W : Type u_3
inst✝³ : Category W
inst✝² : Preadditive W
c : ComplexShape ι
F G : V ⥤ W
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
C D : HomologicalComplex V c
f : C ⟶ D
⊢ (Functor.mapHomologicalComplex F c).map f ≫ (mapHomologicalComplex α c).app D =
    (mapHomologicalComplex α c).app C ≫ (Functor.mapHomologicalComplex G c).map f
aesop_cat