C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
A : Type ?u.280998
inst✝¹ : Category A
inst✝ : Abelian A
X Y : CosimplicialObject C
n : ℕ
⊢ ∑ i : Fin (n + 2), (-1) ^ ↑i • CosimplicialObject.δ X i =
    ∑ x : Fin (n + 2), (-1) ^ ↑x • (SimplicialObject.δ ((cosimplicialSimplicialEquiv C).functor.obj X.op) x).unop
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
A : Type ?u.280998
inst✝¹ : Category A
inst✝ : Abelian A
X Y : CosimplicialObject C
n : ℕ
⊢ objD X n = (AlternatingFaceMapComplex.objD ((cosimplicialSimplicialEquiv C).functor.obj X.op) n).unop
simp only [objD, AlternatingFaceMapComplex.objD, unop_sum, unop_zsmul]
no goals
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
A : Type ?u.280998
inst✝¹ : Category A
inst✝ : Abelian A
X Y : CosimplicialObject C
n : ℕ
⊢ ∑ i : Fin (n + 2), (-1) ^ ↑i • CosimplicialObject.δ X i =
    ∑ x : Fin (n + 2), (-1) ^ ↑x • (SimplicialObject.δ ((cosimplicialSimplicialEquiv C).functor.obj X.op) x).unop
rfl