ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
rij rij' : ComplexShape.Rel c i j
⊢ d C i j ≫ eqToHom (_ : X C j = X C j) = d C i j
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j j' : ι
rij : ComplexShape.Rel c i j
rij' : ComplexShape.Rel c i j'
⊢ d C i j' ≫ eqToHom (_ : X C j' = X C j) = d C i j
obtain rfl := c.next_eq rij rij'
no goals
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
rij rij' : ComplexShape.Rel c i j
⊢ d C i j ≫ eqToHom (_ : X C j = X C j) = d C i j
simp only [eqToHom_refl, comp_id]