case pos
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C A B : HomologicalComplex V c
f : Hom A B
i j : ι
hij : ComplexShape.Rel c i j
⊢ HomologicalComplex.Hom.f f i ≫ d B i j = d A i j ≫ HomologicalComplex.Hom.f f j

case neg
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C A B : HomologicalComplex V c
f : Hom A B
i j : ι
hij : ¬ComplexShape.Rel c i j
⊢ HomologicalComplex.Hom.f f i ≫ d B i j = d A i j ≫ HomologicalComplex.Hom.f f j
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C A B : HomologicalComplex V c
f : Hom A B
i j : ι
⊢ HomologicalComplex.Hom.f f i ≫ d B i j = d A i j ≫ HomologicalComplex.Hom.f f j
by_cases hij : c.Rel i j
no goals
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C A B : HomologicalComplex V c
f : Hom A B
i j : ι
hij : ¬ComplexShape.Rel c i j
⊢ HomologicalComplex.Hom.f f i ≫ d B i j = d A i j ≫ HomologicalComplex.Hom.f f j
. rw [A.shape i j hij, B.shape i j hij, comp_zero, zero_comp]
no goals
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C A B : HomologicalComplex V c
f : Hom A B
i j : ι
hij : ComplexShape.Rel c i j
⊢ HomologicalComplex.Hom.f f i ≫ d B i j = d A i j ≫ HomologicalComplex.Hom.f f j
exact f.comm' i j hij
no goals
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C A B : HomologicalComplex V c
f : Hom A B
i j : ι
hij : ¬ComplexShape.Rel c i j
⊢ HomologicalComplex.Hom.f f i ≫ d B i j = d A i j ≫ HomologicalComplex.Hom.f f j
rw [A.shape i j hij, B.shape i j hij, comp_zero, zero_comp]