ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : Hom C₁ C₂
i : ι
w : ComplexShape.Rel c i (ComplexShape.next c i)
⊢ next f i = (xNextIso C₁ w).hom ≫ HomologicalComplex.Hom.f f (ComplexShape.next c i) ≫ (xNextIso C₂ w).inv
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : Hom C₁ C₂
i j : ι
w : ComplexShape.Rel c i j
⊢ next f i = (xNextIso C₁ w).hom ≫ HomologicalComplex.Hom.f f j ≫ (xNextIso C₂ w).inv
obtain rfl := c.next_eq' w
no goals
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : Hom C₁ C₂
i : ι
w : ComplexShape.Rel c i (ComplexShape.next c i)
⊢ next f i = (xNextIso C₁ w).hom ≫ HomologicalComplex.Hom.f f (ComplexShape.next c i) ≫ (xNextIso C₂ w).inv
simp only [xNextIso, eqToIso_refl, Iso.refl_hom, Iso.refl_inv, comp_id, id_comp]