C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) 0 = 0
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ HomologicalComplex.Hom.f (Hσ q) 0 = 0
unfold Hσ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ hσ' q 0 1 (_ : ComplexShape.Rel c 1 0) ≫ HomologicalComplex.d K[X] 1 0 = 0
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) 0 = 0
rw [nullHomotopicMap'_f_of_not_rel_left (c_mk 1 0 rfl) cs_down_0_not_rel_left]
case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ hσ' Nat.zero 0 1 (_ : ComplexShape.Rel c 1 0) ≫ HomologicalComplex.d K[X] 1 0 = 0

case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ hσ' (Nat.succ q) 0 1 (_ : ComplexShape.Rel c 1 0) ≫ HomologicalComplex.d K[X] 1 0 = 0
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ hσ' q 0 1 (_ : ComplexShape.Rel c 1 0) ≫ HomologicalComplex.d K[X] 1 0 = 0
rcases q with (_|q)
case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ (((-1) ^ 0 • σ X { val := 0, isLt := (_ : 0 < Nat.succ 0) }) ≫ eqToHom (_ : X.obj [0 + 1].op = X.obj [1].op)) ≫
      HomologicalComplex.d K[X] 1 0 =
    0
case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ hσ' Nat.zero 0 1 (_ : ComplexShape.Rel c 1 0) ≫ HomologicalComplex.d K[X] 1 0 = 0
rw [hσ'_eq (show 0 = 0 + 0 by rfl) (c_mk 1 0 rfl)]
case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ σ X 0 ≫ HomologicalComplex.d K[X] 1 0 = 0
case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ (((-1) ^ 0 • σ X { val := 0, isLt := (_ : 0 < Nat.succ 0) }) ≫ eqToHom (_ : X.obj [0 + 1].op = X.obj [1].op)) ≫
      HomologicalComplex.d K[X] 1 0 =
    0
simp only [pow_zero, Fin.mk_zero, one_zsmul, eqToHom_refl, Category.comp_id]
case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ σ X 0 ≫ AlternatingFaceMapComplex.objD X 0 = 0
case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ σ X 0 ≫ HomologicalComplex.d K[X] 1 0 = 0
erw [ChainComplex.of_d]
case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ σ X 0 ≫ δ X 0 = σ X 0 ≫ δ X 1
case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ σ X 0 ≫ AlternatingFaceMapComplex.objD X 0 = 0
rw [AlternatingFaceMapComplex.objD, Fin.sum_univ_two, Fin.val_zero, Fin.val_one, pow_zero,
  pow_one, one_smul, neg_smul, one_smul, comp_add, comp_neg, add_neg_eq_zero]
no goals
case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ σ X 0 ≫ δ X 0 = σ X 0 ≫ δ X 1
erw [δ_comp_σ_self, δ_comp_σ_succ]
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ 0 = 0 + 0
rfl
no goals
case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ hσ' (Nat.succ q) 0 1 (_ : ComplexShape.Rel c 1 0) ≫ HomologicalComplex.d K[X] 1 0 = 0
rw [hσ'_eq_zero (Nat.succ_pos q) (c_mk 1 0 rfl), zero_comp]