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

case neg
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : ¬ComplexShape.Rel c i j
⊢ d C i j ≫ d C j k = 0
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
⊢ d C i j ≫ d C j k = 0
by_cases hij : c.Rel i j
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : ComplexShape.Rel c i j
hjk : ComplexShape.Rel c j k
⊢ d C i j ≫ d C j k = 0

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