no goals
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
A : Type ?u.282467
inst✝¹ : Category A
inst✝ : Abelian A
X Y : CosimplicialObject C
n : ℕ
⊢ objD X n ≫ objD X (n + 1) = 0
simp only [d_eq_unop_d, ← unop_comp, AlternatingFaceMapComplex.d_squared, unop_zero]