[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.4444, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
i j k : ι
hi : ComplexShape.prev c j = i
hk : ComplexShape.next c j = k
K : HomologicalComplex C c
⊢ (XIsoOfEq K hi).hom ≫ ((shortComplexFunctor' C c i j k).obj K).f =
    ((shortComplexFunctor C c j).obj K).f ≫ (Iso.refl ((shortComplexFunctor C c j).obj K).X₂).hom
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.4444, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
i j k : ι
hi : ComplexShape.prev c j = i
hk : ComplexShape.next c j = k
K : HomologicalComplex C c
⊢ (Iso.refl ((shortComplexFunctor C c j).obj K).X₂).hom ≫ ((shortComplexFunctor' C c i j k).obj K).g =
    ((shortComplexFunctor C c j).obj K).g ≫ (XIsoOfEq K hk).hom
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.4444, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
i j k : ι
hi : ComplexShape.prev c j = i
hk : ComplexShape.next c j = k
⊢ ∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y),
    (shortComplexFunctor C c j).map f ≫
        ((fun K => ShortComplex.isoMk (XIsoOfEq K hi) (Iso.refl ((shortComplexFunctor C c j).obj K).X₂) (XIsoOfEq K hk))
            Y).hom =
      ((fun K => ShortComplex.isoMk (XIsoOfEq K hi) (Iso.refl ((shortComplexFunctor C c j).obj K).X₂) (XIsoOfEq K hk))
            X).hom ≫
        (shortComplexFunctor' C c i j k).map f
[PROOFSTEP]
aesop_cat
