C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnq : n < q
hnm : ComplexShape.Rel c m n
⊢ (if n < q then 0 else (-1) ^ (n - q) • σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) }) ≫
      eqToHom (_ : X.obj [n + 1].op = X.obj [m].op) =
    0
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnq : n < q
hnm : ComplexShape.Rel c m n
⊢ hσ' q n m hnm = 0
simp only [hσ', hσ]
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnq : n < q
hnm : ComplexShape.Rel c m n
⊢ 0 ≫ eqToHom (_ : X.obj [n + 1].op = X.obj [m].op) = 0
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnq : n < q
hnm : ComplexShape.Rel c m n
⊢ (if n < q then 0 else (-1) ^ (n - q) • σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) }) ≫
      eqToHom (_ : X.obj [n + 1].op = X.obj [m].op) =
    0
split_ifs
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnq : n < q
hnm : ComplexShape.Rel c m n
⊢ 0 ≫ eqToHom (_ : X.obj [n + 1].op = X.obj [m].op) = 0
exact zero_comp