ι : 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 : ι
f : (i j : ι) → X C i ⟶ X D j
g : D ⟶ E
j : ι
⊢ (f j (ComplexShape.prev c j) ≫ Hom.f g (ComplexShape.prev c j)) ≫ d E (ComplexShape.prev c j) j =
    (f j (ComplexShape.prev c j) ≫ d D (ComplexShape.prev c j) j) ≫ Hom.f g j
ι : 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 : ι
f : (i j : ι) → X C i ⟶ X D j
g : D ⟶ E
j : ι
⊢ (↑(prevD j) fun i j => f i j ≫ Hom.f g j) = ↑(prevD j) f ≫ Hom.f g j
dsimp [prevD]
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 : ι
f : (i j : ι) → X C i ⟶ X D j
g : D ⟶ E
j : ι
⊢ (f j (ComplexShape.prev c j) ≫ Hom.f g (ComplexShape.prev c j)) ≫ d E (ComplexShape.prev c j) j =
    (f j (ComplexShape.prev c j) ≫ d D (ComplexShape.prev c j) j) ≫ Hom.f g j
simp only [Category.assoc, g.comm]