C : Type u_1
inst✝¹ : Category C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ (HomologicalComplex.d (AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)) (n + 1) n).f =
    P.p.app [n + 1].op ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n
C : Type u_1
inst✝¹ : Category C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ (HomologicalComplex.d (AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)) (n + 1) n).f =
    P.p.app [n + 1].op ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n
dsimp
C : Type u_1
inst✝¹ : Category C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ ∑ x : Fin (n + 2), (-1) ^ ↑x • (SimplicialObject.δ (KaroubiFunctorCategoryEmbedding.obj P) x).f =
    ∑ x : Fin (n + 2), (-1) ^ ↑x • P.p.app [n + 1].op ≫ SimplicialObject.δ P.X x
C : Type u_1
inst✝¹ : Category C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ (HomologicalComplex.d (AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)) (n + 1) n).f =
    P.p.app [n + 1].op ≫ HomologicalComplex.d (AlternatingFaceMapComplex.obj P.X) (n + 1) n
simp only [AlternatingFaceMapComplex.obj_d_eq, Karoubi.sum_hom, Preadditive.comp_sum,
  Karoubi.zsmul_hom, Preadditive.comp_zsmul]
no goals
C : Type u_1
inst✝¹ : Category C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ ∑ x : Fin (n + 2), (-1) ^ ↑x • (SimplicialObject.δ (KaroubiFunctorCategoryEmbedding.obj P) x).f =
    ∑ x : Fin (n + 2), (-1) ^ ↑x • P.p.app [n + 1].op ≫ SimplicialObject.δ P.X x
rfl